Hide declarations steps from trace when an initialisation follows

If the front-end generated a declaration with an initialiser, then goto
conversion can mark the declaration statement (but not the
initialisation!) as hidden. This will avoid showing meaningless values
in a goto trace.

Author: tautschnig

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

@@ -16,6 +16,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

src/goto-programs/goto_convert.cpp

@@ -627,11 +627,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 +643,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.source_location();
 
       convert_assign(assign, dest, mode);
     }