Symex support for lhs-typecasts and side effects

Author: tautschnig

src/path-symex/path_symex.cpp

@@ -422,6 +422,14 @@ void path_symext::assign_rec(
       var_state.value=propagate(ssa_rhs)?ssa_rhs:nil_exprt();
     }
   }
+  else if(ssa_lhs.id()==ID_typecast)
+  {
+    // dereferencing might yield a typecast
+    const exprt &new_lhs=to_typecast_expr(ssa_lhs).op();
+    typecast_exprt new_rhs(ssa_rhs, new_lhs.type());
+
+    assign_rec(state, guard, new_lhs, new_rhs);
+  }
   else if(ssa_lhs.id()==ID_member)
   {
     #ifdef DEBUG

src/path-symex/path_symex_state_read.cpp

@@ -247,7 +247,14 @@ exprt path_symex_statet::instantiate_rec(
     {
       irep_idt id="symex::nondet"+std::to_string(var_map.nondet_count);
       var_map.nondet_count++;
-      return symbol_exprt(id, src.type());
+
+      auxiliary_symbolt nondet_symbol;
+      nondet_symbol.name=id;
+      nondet_symbol.base_name=id;
+      nondet_symbol.type=src.type();
+      var_map.new_symbols.add(nondet_symbol);
+
+      return nondet_symbol.symbol_expr();
     }
     else
       throw "instantiate_rec: unexpected side effect "+id2string(statement);

src/path-symex/var_map.h

@@ -18,12 +18,17 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/namespace.h>
 #include <util/type.h>
 #include <util/std_expr.h>
+#include <util/symbol_table.h>
 
 class var_mapt
 {
 public:
   explicit var_mapt(const namespacet &_ns):
-    ns(_ns), shared_count(0), local_count(0), nondet_count(0), dynamic_count(0)
+    ns(_ns.get_symbol_table(), new_symbols),
+    shared_count(0),
+    local_count(0),
+    nondet_count(0),
+    dynamic_count(0)
   {
   }
 
@@ -93,7 +98,8 @@ class var_mapt
 
   void init(var_infot &var_info);
 
-  const namespacet &ns;
+  const namespacet ns;
+  symbol_tablet new_symbols;
 
   void output(std::ostream &) const;