Merge pull request #6712 from tautschnig/feature/hide-decl

Hide declarations steps from trace when an initialisation follows

Author: tautschnig

regression/cbmc-cover/location-multiline-statement/multi-file.desc

@@ -3,7 +3,7 @@ multi-file.c
 --cover location
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.coverage.2\] file multi-file.c line 10 function main block 2 \(lines [\w\- /\.\\:]*dereference.h:main:2; multi-file.c:main:10,13,14,16\): SATISFIED
+^\[main.coverage.2\] file multi-file.c line 13 function main block 2 \(lines [\w\- /\.\\:]*dereference.h:main:2; multi-file.c:main:10,13,14,16\): SATISFIED
 --
 ^warning: ignoring
 --

regression/cbmc-cover/location-multiline-statement/test.desc

@@ -3,7 +3,7 @@ example.c
 --cover location
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.coverage.2\] file example.c line 10 function main block 2 \(lines example.c:main:10,13,14\): SATISFIED$
+^\[main.coverage.2\] file example.c line 13 function main block 2 \(lines example.c:main:10,13,14\): SATISFIED$
 --
 ^warning: ignoring
 --

regression/cbmc-cover/location15/test.desc

@@ -4,7 +4,7 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.coverage.1\] file main.c line 10 function main block 1.*: SATISFIED$
-^\[main.coverage.2\] file main.c line 10 function main block 2.*: SATISFIED$
+^\[main.coverage.2\] file main.c line 11 function main block 2.*: SATISFIED$
 ^\[main.coverage.3\] file main.c line 13 function main block 3.*: FAILED$
 ^\[main.coverage.4\] file main.c line 16 function main block 4.*: SATISFIED$
 ^\[foo.coverage.1\] file main.c line 5 function foo block 1.*: FAILED$

regression/cbmc/trace-values/trace-values.c

@@ -11,15 +11,14 @@ struct S
 int main()
 {
   static int static_var;
-  int local_var;
+  int local_var = 3;
   int *p=&my_nested[0].array[1];
   int *q=&my_nested[1].f;
   int *null=0;
   int *junk;
 
   global_var=1;
   static_var=2;
-  local_var=3;
   *p=4;
   *q=5;
   *null=6;

regression/cbmc/trace-values/trace-values.desc

@@ -3,7 +3,6 @@ trace-values.c
 --trace
 ^EXIT=10$
 ^SIGNAL=0$
-^  local_var=0 .*$
 ^  global_var=1 .*$
 ^  static_var=2 .*$
 ^  local_var=3 .*$
@@ -16,6 +15,7 @@ trace-values.c
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
+^  local_var=[^3]+ .*$
 --
 Note the assignment to "null" is not included because an assignment direct to
 a certainly-null pointer goes to symex::invalid_object, not null$object, and is

regression/cbmc/z3/trace-char.desc

@@ -3,7 +3,6 @@ trace-char.c
 --trace --smt2 --z3
 ^EXIT=10$
 ^SIGNAL=0$
-arr=\{ arr
 arr=\{ '0', '1', '2', '3', '4', '5', '6', '7' \}
 --
 arr=(assignment removed)

regression/cbmc/z3/trace.desc

@@ -3,7 +3,6 @@ trace.c
 --trace --smt2 --z3
 ^EXIT=10$
 ^SIGNAL=0$
-arr=\{ arr
 arr=\{ 0, 1, 2, 3, 4, 5, 6, 17 \}
 --
 arr=(assignment removed)

src/goto-instrument/unwindset.cpp

@@ -126,6 +126,9 @@ void unwindsett::parse_unwindset_one_loop(
               loop_nr_label) != instruction.labels.end())
           {
             location = instruction.source_location();
+            // the label may be attached to the DECL part of an initializing
+            // declaration, which we may have marked as hidden
+            location->remove(ID_hide);
           }
           if(
             location.has_value() && instruction.is_backwards_goto() &&

src/goto-programs/goto_convert.cpp

@@ -626,12 +626,12 @@ void goto_convertt::convert_frontend_decl(
   }
   else
   {
-    // this is expected to go away
-    exprt initializer;
+    exprt initializer = code.op1();
 
     codet tmp=code;
-    initializer=code.op1();
     tmp.operands().resize(1);
+    // hide this declaration-without-initializer step in the goto trace
+    tmp.add_source_location().set_hide();
 
     // Break up into decl and assignment.
     // Decl must be visible before initializer.
@@ -642,7 +642,7 @@ void goto_convertt::convert_frontend_decl(
     if(initializer.is_not_nil())
     {
       code_assignt assign(code.op0(), initializer);
-      assign.add_source_location() = tmp.source_location();
+      assign.add_source_location() = initializer.find_source_location();
 
       convert_assign(assign, dest, mode);
     }