use ssa_exprt

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@6381 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

regression/cbmc/Malloc18/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/Malloc21/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$

src/analyses/goto_check.cpp

@@ -1540,6 +1540,8 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
           goto_programt::targett t=new_code.add_instruction(ASSIGN);
           exprt address_of_expr=address_of_exprt(variable);
           exprt lhs=ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
+          if(!base_type_eq(lhs.type(), address_of_expr.type(), ns))
+            address_of_expr.make_typecast(lhs.type());
           exprt rhs=if_exprt(
             side_effect_expr_nondett(bool_typet()), address_of_expr, lhs, lhs.type());
           t->source_location=i.source_location;

src/cbmc/counterexample_beautification.cpp

@@ -45,7 +45,7 @@ void counterexample_beautificationt::get_minimization_list(
     {
       if(!prop_conv.l_get(it->guard_literal).is_false())
       {
-        const typet &type=it->original_lhs_object.type();
+        const typet &type=it->ssa_lhs.type();
 
         if(type!=bool_typet())
         {

src/goto-programs/goto_trace.cpp

@@ -112,8 +112,8 @@ void goto_trace_stept::output(
 
   if(pc->is_other() || pc->is_assign())
   {
-    irep_idt identifier=lhs_object.get_identifier();
-    out << "  " << identifier
+    irep_idt identifier=lhs_object.get_object_name();
+    out << "  " << from_expr(ns, identifier, lhs_object.get_original_expr())
         << " = " << from_expr(ns, identifier, lhs_object_value)
         << "\n";
   }
@@ -221,11 +221,11 @@ Function: trace_value
 void trace_value(
   std::ostream &out,
   const namespacet &ns,
-  const symbol_exprt &lhs_object,
+  const ssa_exprt &lhs_object,
   const exprt &full_lhs,
   const exprt &value)
 {
-  const irep_idt &identifier=lhs_object.get_identifier();
+  const irep_idt &identifier=lhs_object.get_object_name();
   std::string value_string;
 
   if(value.is_nil())

src/goto-programs/goto_trace.h

@@ -21,7 +21,7 @@ Date: July 2005
 #include <iosfwd>
 #include <vector>
 
-#include <util/std_expr.h>
+#include <util/ssa_expr.h>
 
 #include <goto-programs/goto_program.h>
 
@@ -80,7 +80,7 @@ class goto_trace_stept
   std::string comment;
 
   // the object being assigned
-  symbol_exprt lhs_object;
+  ssa_exprt lhs_object;
 
   // the full, original lhs expression
   exprt full_lhs;
@@ -173,7 +173,7 @@ void show_goto_trace(
 void trace_value(
   std::ostream &out,
   const namespacet &ns,
-  const symbol_exprt &lhs_object,
+  const ssa_exprt &lhs_object,
   const exprt &full_lhs,
   const exprt &value);
 

src/goto-symex/auto_objects.cpp

@@ -101,7 +101,7 @@ void goto_symext::initialize_auto_object(
         address_of_expr);
 
       code_assignt assignment(expr, rhs);
-      symex_assign(state, assignment); /* TODO: needs clean */
+      symex_assign_rec(state, assignment);
     }
   }
 }
@@ -122,21 +122,25 @@ void goto_symext::trigger_auto_object(
   const exprt &expr,
   statet &state)
 {
-  if(expr.id()==ID_symbol)
+  if(expr.id()==ID_symbol &&
+     expr.get_bool(ID_C_SSA_symbol))
   {
-    const symbol_exprt &symbol_expr=to_symbol_expr(expr);
-    const irep_idt &identifier=symbol_expr.get_identifier();
+    const ssa_exprt &ssa_expr=to_ssa_expr(expr);
+    const irep_idt &obj_identifier=ssa_expr.get_object_name();
 
-    const symbolt &symbol=
-      ns.lookup(state.get_original_name(identifier));
-
-    if(has_prefix(id2string(symbol.base_name), "auto_object"))
+    if(obj_identifier!="goto_symex::\\guard")
     {
-      // done already?
-      if(state.level2.current_names.find(identifier)==
-         state.level2.current_names.end())
+      const symbolt &symbol=
+        ns.lookup(obj_identifier);
+
+      if(has_prefix(id2string(symbol.base_name), "auto_object"))
       {
-        initialize_auto_object(expr, state);
+        // done already?
+        if(state.level2.current_names.find(ssa_expr.get_identifier())==
+           state.level2.current_names.end())
+        {
+          initialize_auto_object(expr, state);
+        }
       }
     }
   }

src/goto-symex/build_goto_trace.cpp

@@ -226,7 +226,10 @@ void build_goto_trace(
     goto_trace_step.thread_nr=SSA_step.source.thread_nr;
     goto_trace_step.pc=SSA_step.source.pc;
     goto_trace_step.comment=SSA_step.comment;
-    goto_trace_step.lhs_object=SSA_step.original_lhs_object;
+    if(SSA_step.ssa_lhs.is_not_nil())
+      goto_trace_step.lhs_object=ssa_exprt(SSA_step.ssa_lhs.get_original_expr());
+    else
+      goto_trace_step.lhs_object.make_nil();
     goto_trace_step.type=SSA_step.type;
     goto_trace_step.hidden=SSA_step.hidden;
     goto_trace_step.format_string=SSA_step.format_string;

src/goto-symex/goto_symex.h

@@ -153,6 +153,7 @@ class goto_symext
   virtual void symex_atomic_begin(statet &state);
   virtual void symex_atomic_end(statet &state);  
   virtual void symex_decl(statet &state);
+  virtual void symex_decl(statet &state, const symbol_exprt &expr);
   virtual void symex_dead(statet &state);
 
   virtual void symex_other(
@@ -239,12 +240,13 @@ class goto_symext
   virtual void do_simplify(exprt &expr);
 
   //virtual void symex_block(statet &state, const codet &code);
+  void symex_assign_rec(statet &state, const code_assignt &code);
   virtual void symex_assign(statet &state, const code_assignt &code);
 
   typedef symex_targett::assignment_typet assignment_typet;
 
   void symex_assign_rec(statet &state, const exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type);
-  void symex_assign_symbol(statet &state, const symbol_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type);
+  void symex_assign_symbol(statet &state, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type);
   void symex_assign_typecast(statet &state, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type);
   void symex_assign_array(statet &state, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type);
   void symex_assign_struct_member(statet &state, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type);