@@ -93,6 +93,8 @@ void constant_propagator_domaint::transform(
9393 {
9494 exprt g;
9595
96+ // Comparing iterators is safe as the target must be within the same list
97+ // of instructions because this is a GOTO.
9698 if (from->get_target ()==to)
9799 g=simplify_expr (from->guard , ns);
98100 else
@@ -121,15 +123,14 @@ void constant_propagator_domaint::transform(
121123 const code_function_callt &function_call=to_code_function_call (from->code );
122124 const exprt &function=function_call.function ();
123125
124- const locationt& next=std::next (from);
125-
126126 if (function.id ()==ID_symbol)
127127 {
128128 // called function identifier
129129 const symbol_exprt &symbol_expr=to_symbol_expr (function);
130130 const irep_idt id=symbol_expr.get_identifier ();
131131
132- if (to==next)
132+ // Functions with no body
133+ if (from->function == to->function )
133134 {
134135 if (id==CPROVER_PREFIX " set_must" ||
135136 id==CPROVER_PREFIX " get_must" ||
@@ -177,7 +178,9 @@ void constant_propagator_domaint::transform(
177178 else
178179 {
179180 // unresolved call
180- INVARIANT (to==next, " Unresolved call can only be approximated if a skip" );
181+ INVARIANT (
182+ from->function == to->function ,
183+ " Unresolved call can only be approximated if a skip" );
181184
182185 if (have_dirty)
183186 values.set_dirty_to_top (cp->dirty , ns);
0 commit comments