From 16c619b4d7a9566e60565f7eeb92df4532701708 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 26 Apr 2024 12:25:02 +0000 Subject: [PATCH] Make DFCC is_dead_object_update less restrictive GOTO programs are free to use different ways to assign to `__CPROVER_dead_object`. Any such assignment that does not match the expected pattern can then safely be ignored. --- .../dynamic-frames/dfcc_instrument.cpp | 22 ++++++++++--------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp index 1f885938aca..34e3f44a2b7 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp @@ -757,19 +757,21 @@ dfcc_instrumentt::is_dead_object_update(const exprt &lhs, const exprt &rhs) { if( lhs.id() == ID_symbol && - to_symbol_expr(lhs).get_identifier() == CPROVER_PREFIX "dead_object") + to_symbol_expr(lhs).get_identifier() == CPROVER_PREFIX "dead_object" && + rhs.id() == ID_if) { - // error out if rhs is different from `if_exprt(nondet, ptr, dead_object)` - PRECONDITION(rhs.id() == ID_if); + // only handle `if_exprt(nondet, ptr, dead_object)` auto &if_expr = to_if_expr(rhs); - PRECONDITION(can_cast_expr(if_expr.cond())); - PRECONDITION(if_expr.false_case() == lhs); - return if_expr.true_case(); - } - else - { - return {}; + if( + if_expr.cond().id() == ID_side_effect && + to_side_effect_expr(if_expr.cond()).get_statement() == ID_nondet && + if_expr.false_case() == lhs) + { + return if_expr.true_case(); + } } + + return {}; } void dfcc_instrumentt::instrument_assign(