CONTRACTS: add missing source locations

remi-delmas-3000 · Aug 14, 2023 · d01248a · d01248a
1 parent 08a466d
commit d01248a
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 12 deletions.
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp
@@ -249,8 +249,8 @@ dfcc_instrument_loopt::add_prehead_instructions(
   {
     pre_loop_head_instrs.add(
       goto_programt::make_decl(entered_loop, loop_head_location));
-    pre_loop_head_instrs.add(
-      goto_programt::make_assignment(entered_loop, false_exprt{}));
+    pre_loop_head_instrs.add(goto_programt::make_assignment(
+      entered_loop, false_exprt{}, loop_head_location));
   }
 
   // initial_invariant = <loop_invariant>;
@@ -276,8 +276,8 @@ dfcc_instrument_loopt::add_prehead_instructions(
     // in_base_case = true;
     pre_loop_head_instrs.add(
       goto_programt::make_decl(in_base_case, loop_head_location));
-    pre_loop_head_instrs.add(
-      goto_programt::make_assignment(in_base_case, true_exprt{}));
+    pre_loop_head_instrs.add(goto_programt::make_assignment(
+      in_base_case, true_exprt{}, loop_head_location));
   }
 
   {
@@ -417,11 +417,11 @@ dfcc_instrument_loopt::add_step_instructions(
       loop_head_location);
     step_instrs.add(
       goto_programt::make_decl(in_loop_havoc_block, loop_head_location));
-    step_instrs.add(
-      goto_programt::make_assignment(in_loop_havoc_block, true_exprt{}));
+    step_instrs.add(goto_programt::make_assignment(
+      in_loop_havoc_block, true_exprt{}, loop_head_location));
     step_instrs.destructive_append(havoc_instrs);
-    step_instrs.add(
-      goto_programt::make_assignment(in_loop_havoc_block, false_exprt{}));
+    step_instrs.add(goto_programt::make_assignment(
+      in_loop_havoc_block, false_exprt{}, loop_head_location));
   }
 
   goto_convertt converter(symbol_table, log.get_message_handler());
@@ -490,8 +490,8 @@ void dfcc_instrument_loopt::add_body_instructions(
 
   {
     // Record that we entered the loop with `entered_loop = true`.
-    pre_loop_latch_instrs.add(
-      goto_programt::make_assignment(entered_loop, true_exprt{}));
+    pre_loop_latch_instrs.add(goto_programt::make_assignment(
+      entered_loop, true_exprt{}, loop_head_location));
   }
 
   {

diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp
@@ -205,7 +205,7 @@ void dfcc_spec_functionst::generate_havoc_instructions(
           "__havoc_target",
           location);
 
-        havoc_program.add(goto_programt::make_decl(target_expr));
+        havoc_program.add(goto_programt::make_decl(target_expr, location));
 
         call.lhs() = target_expr;
         havoc_program.add(goto_programt::make_function_call(call, location));
@@ -221,7 +221,8 @@ void dfcc_spec_functionst::generate_havoc_instructions(
             target_expr, pointer_type(target_type))},
           nondet,
           location));
-        auto label = havoc_program.add(goto_programt::make_dead(target_expr));
+        auto label =
+          havoc_program.add(goto_programt::make_dead(target_expr, location));
         goto_instruction->complete_goto(label);
       }
       else if(