Merge pull request diffblue#986 from owen-jones-diffblue/bugfix/goto-trace-contains-ssa-information-test-gen-support

Remove SSA ids from goto trace

Author: smowton

regression/cbmc/pointer-function-parameters-2/test.desc

@@ -5,8 +5,8 @@ main.c
 ^\*\* Used 4 iterations$
 ^Test suite:$
 ^a=\(\(signed int \*\*\)NULL\), tmp\$1=[^,]*, tmp\$2=[^,]*$
-^a=&tmp\$1!0, tmp\$1=\(\(signed int \*\)NULL\), tmp\$2=[^,]*$
-^a=&tmp\$1!0, tmp\$1=&tmp\$2!0, tmp\$2=([012356789][0-9]*|4[0-9]+)$
-^a=&tmp\$1!0, tmp\$1=&tmp\$2!0, tmp\$2=4$
+^a=&tmp\$1, tmp\$1=\(\(signed int \*\)NULL\), tmp\$2=[^,]*$
+^a=&tmp\$1, tmp\$1=&tmp\$2, tmp\$2=([012356789][0-9]*|4[0-9]+)$
+^a=&tmp\$1, tmp\$1=&tmp\$2, tmp\$2=4$
 --
 ^warning: ignoring

regression/cbmc/pointer-function-parameters/test.desc

@@ -5,7 +5,7 @@ main.c
 ^\*\* Used 3 iterations$
 ^Test suite:$
 ^a=\(\(signed int \*\)NULL\), tmp\$1=[^,]*$
-^a=&tmp\$1!0, tmp\$1=4$
-^a=&tmp\$1!0, tmp\$1=([012356789][0-9]*|4[0-9]+)$
+^a=&tmp\$1, tmp\$1=4$
+^a=&tmp\$1, tmp\$1=([012356789][0-9]*|4[0-9]+)$
 --
 ^warning: ignoring

src/goto-symex/build_goto_trace.cpp

@@ -308,8 +308,17 @@ void build_goto_trace(
         goto_trace_step.io_args.push_back(j);
       else
       {
-        exprt tmp=prop_conv.get(j);
-        goto_trace_step.io_args.push_back(tmp);
+        // we only expect constants here
+        exprt expr=to_constant_expr(prop_conv.get(j));
+        if(expr.has_operands() && expr.op0().id()==ID_address_of)
+        {
+          exprt *op=&(to_address_of_expr(expr.op0()).object());
+          while(op->id()==ID_member || op->id()==ID_index)
+            op=&(op->op0());
+          *op=to_ssa_expr(*op).get_original_expr();
+        }
+        // use expr in the output
+        goto_trace_step.io_args.push_back(expr);
       }
     }