From a9d96f6617b7c72231398b82293834483cc078d8 Mon Sep 17 00:00:00 2001
From: Owen Jones <owen.jones@diffblue.com>
Date: Fri, 2 Jun 2017 13:42:23 +0100
Subject: [PATCH] Remove SSA ids from goto trace

When building the goto trace we remove the SSA ids from most variable
names, but they were still in address-of expressions in the right hand
sides of assignments.
---
 .../cbmc/pointer-function-parameters-2/test.desc    |  6 +++---
 .../cbmc/pointer-function-parameters/test.desc      |  4 ++--
 src/goto-symex/build_goto_trace.cpp                 | 13 +++++++++++--
 3 files changed, 16 insertions(+), 7 deletions(-)

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