diff --git a/regression/cbmc/pointer-function-parameters-2/test.desc b/regression/cbmc/pointer-function-parameters-2/test.desc index 1db7d3c4f37..c67211d7387 100644 --- a/regression/cbmc/pointer-function-parameters-2/test.desc +++ b/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 diff --git a/regression/cbmc/pointer-function-parameters/test.desc b/regression/cbmc/pointer-function-parameters/test.desc index ee8efd932ad..b9aa6240dea 100644 --- a/regression/cbmc/pointer-function-parameters/test.desc +++ b/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 diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp index f7e806ac322..6139c4dcdab 100644 --- a/src/goto-symex/build_goto_trace.cpp +++ b/src/goto-symex/build_goto_trace.cpp @@ -308,17 +308,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); } }