Skip to content

Commit 04f9d32

Browse files
Owen Jonestautschnig
Owen Jones
authored andcommitted
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.
1 parent c561b92 commit 04f9d32

File tree

3 files changed

+7
-16
lines changed

3 files changed

+7
-16
lines changed

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

+3-3
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ main.c
55
^\*\* Used 4 iterations$
66
^Test suite:$
77
^a=\(\(signed int \*\*\)NULL\), tmp\$1=[^,]*, tmp\$2=[^,]*$
8-
^a=&tmp\$1, tmp\$1=\(\(signed int \*\)NULL\), tmp\$2=[^,]*$
9-
^a=&tmp\$1, tmp\$1=&tmp\$2, tmp\$2=([012356789][0-9]*|4[0-9]+)$
10-
^a=&tmp\$1, tmp\$1=&tmp\$2, tmp\$2=4$
8+
^a=&tmp\$1!0, tmp\$1=\(\(signed int \*\)NULL\), tmp\$2=[^,]*$
9+
^a=&tmp\$1!0, tmp\$1=&tmp\$2!0, tmp\$2=([012356789][0-9]*|4[0-9]+)$
10+
^a=&tmp\$1!0, tmp\$1=&tmp\$2!0, tmp\$2=4$
1111
--
1212
^warning: ignoring

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

+2-2
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ main.c
55
^\*\* Used 3 iterations$
66
^Test suite:$
77
^a=\(\(signed int \*\)NULL\), tmp\$1=[^,]*$
8-
^a=&tmp\$1, tmp\$1=4$
9-
^a=&tmp\$1, tmp\$1=([012356789][0-9]*|4[0-9]+)$
8+
^a=&tmp\$1!0, tmp\$1=4$
9+
^a=&tmp\$1!0, tmp\$1=([012356789][0-9]*|4[0-9]+)$
1010
--
1111
^warning: ignoring

src/goto-symex/build_goto_trace.cpp

+2-11
Original file line numberDiff line numberDiff line change
@@ -304,17 +304,8 @@ void build_goto_trace(
304304
goto_trace_step.io_args.push_back(j);
305305
else
306306
{
307-
// we only expect constants here
308-
exprt expr=to_constant_expr(prop_conv.get(j));
309-
if(expr.has_operands() && expr.op0().id()==ID_address_of)
310-
{
311-
exprt *op=&(to_address_of_expr(expr.op0()).object());
312-
while(op->id()==ID_member || op->id()==ID_index)
313-
op=&(op->op0());
314-
*op=to_ssa_expr(*op).get_original_expr();
315-
}
316-
// use expr in the output
317-
goto_trace_step.io_args.push_back(expr);
307+
exprt tmp=prop_conv.get(j);
308+
goto_trace_step.io_args.push_back(tmp);
318309
}
319310
}
320311

0 commit comments

Comments
 (0)