From d01248afacb96bf3bb4715070b4a7a1c49c01b28 Mon Sep 17 00:00:00 2001
From: Remi Delmas <delmasrd@amazon.com>
Date: Mon, 14 Aug 2023 17:53:37 +0000
Subject: [PATCH] CONTRACTS: add missing source locations

---
 .../dynamic-frames/dfcc_instrument_loop.cpp   | 20 +++++++++----------
 .../dynamic-frames/dfcc_spec_functions.cpp    |  5 +++--
 2 files changed, 13 insertions(+), 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
index f2d864b7c69..f0fab83d6bb 100644
--- 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
index 9c4e666f1b0..266e447ef43 100644
--- 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(