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

This reverts commit 3f4c9d1, reversing
changes made to 7c415e8.

Author: Owen Jones

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, 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$
+^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$
 --
 ^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, tmp\$1=4$
-^a=&tmp\$1, tmp\$1=([012356789][0-9]*|4[0-9]+)$
+^a=&tmp\$1!0, tmp\$1=4$
+^a=&tmp\$1!0, tmp\$1=([012356789][0-9]*|4[0-9]+)$
 --
 ^warning: ignoring

src/goto-symex/build_goto_trace.cpp

@@ -306,17 +306,8 @@ void build_goto_trace(
         goto_trace_step.io_args.push_back(j);
       else
       {
-        // 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);
+        exprt tmp=prop_conv.get(j);
+        goto_trace_step.io_args.push_back(tmp);
       }
     }