dynamic memory fixes

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

Author: kroening

src/cbmc/show_vcc.cpp

@@ -71,6 +71,13 @@ void bmct::show_vcc(std::ostream &out)
           std::string string_value;
           languages.from_expr(p_it->cond_expr, string_value);
           out << "{-" << count << "} " << string_value << std::endl;
+
+          #if 0
+          languages.from_expr(p_it->guard_expr, string_value);
+          out << "GUARD: " << string_value << std::endl;
+          out << std::endl;
+          #endif
+          
           count++;
         }
 

src/goto-programs/dynamic_memory.cpp

@@ -16,7 +16,7 @@ Author: Daniel Kroening, [email protected]
 
 /*******************************************************************\
 
-Function: valid_object
+Function: deallocated
 
   Inputs:
 
@@ -26,15 +26,15 @@ Function: valid_object
 
 \*******************************************************************/
 
-exprt valid_object(const namespacet &ns, const exprt &pointer)
+exprt deallocated(const namespacet &ns, const exprt &pointer)
 {
   // we check __CPROVER_deallocated!
   const symbolt &deallocated_symbol=ns.lookup(CPROVER_PREFIX "deallocated");
 
   exprt same_object_expr(ID_same_object, bool_typet());
   same_object_expr.copy_to_operands(pointer, symbol_expr(deallocated_symbol));
 
-  return not_exprt(same_object_expr);
+  return same_object_expr;
 }
 
 /*******************************************************************\

src/goto-programs/dynamic_memory.h

@@ -11,7 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <namespace.h>
 
-exprt valid_object(const namespacet &ns, const exprt &pointer);
+exprt deallocated(const namespacet &ns, const exprt &pointer);
 exprt dynamic_size(const namespacet &ns, const exprt &pointer);
 exprt pointer_object_has_type(const namespacet &ns, const exprt &pointer, const typet &type);
 exprt dynamic_object(const exprt &pointer);

src/goto-symex/builtin_functions.cpp

@@ -114,40 +114,61 @@ void basic_symext::symex_malloc(
         }
       }
     }
-
+    
     if(object_type.is_nil())
       object_type=array_typet(uchar_type(), tmp_size);
-      
-    // must use renamed size in the above,
-    // or it can change!
+
+    // we introduce a fresh symbol for the size
+    // to prevent any issues of the size getting ever changed
+    
+    if(object_type.id()==ID_array &&
+       !to_array_type(object_type).size().is_constant())
+    {
+      exprt &size=to_array_type(object_type).size();
+    
+      symbolt size_symbol;
+
+      size_symbol.base_name="dynamic_object_size"+i2string(dynamic_counter);
+      size_symbol.name="symex_dynamic::"+id2string(size_symbol.base_name);
+      size_symbol.lvalue=true;
+      size_symbol.type=tmp_size.type();
+      size_symbol.mode=ID_C;
+
+      new_context.add(size_symbol);
+
+      guardt guard;
+      symex_assign_rec(state, symbol_expr(size_symbol), nil_exprt(), size, guard, VISIBLE);
+
+      size=symbol_expr(size_symbol);
+    }
   }
 
   // value
-  symbolt symbol;
+  symbolt value_symbol;
 
-  symbol.base_name="dynamic_object"+i2string(dynamic_counter);
-  symbol.name="symex_dynamic::"+id2string(symbol.base_name);
-  symbol.lvalue=true;
-  symbol.type=object_type;
-  symbol.type.set("#dynamic", true);
-  symbol.mode=ID_C;
+  value_symbol.base_name="dynamic_object"+i2string(dynamic_counter);
+  value_symbol.name="symex_dynamic::"+id2string(value_symbol.base_name);
+  value_symbol.lvalue=true;
+  value_symbol.type=object_type;
+  value_symbol.type.set("#dynamic", true);
+  value_symbol.mode=ID_C;
 
-  new_context.add(symbol);
+  new_context.add(value_symbol);
 
   address_of_exprt rhs;
 
   if(object_type.id()==ID_array)
   {
-    rhs.type()=pointer_typet(symbol.type.subtype());
-    index_exprt index_expr(symbol.type.subtype());
-    index_expr.array()=symbol_expr(symbol);
+    rhs.type()=pointer_typet(value_symbol.type.subtype());
+    index_exprt index_expr(value_symbol.type.subtype());
+    index_expr.array()=symbol_expr(value_symbol);
     index_expr.index()=gen_zero(index_type());
     rhs.op0()=index_expr;
   }
   else
   {
-    rhs.op0()=symbol_expr(symbol);
-    rhs.type()=pointer_typet(symbol.type);
+    rhs.op0()=symbol_expr(value_symbol);
+    rhs.type()=pointer_typet(value_symbol.type);
   }
 
   if(rhs.type()!=lhs.type())

src/goto-symex/goto_symex_state.cpp

@@ -474,8 +474,8 @@ void goto_symex_statet::rename_address(
   const namespacet &ns,
   levelt level)
 {
-  // do full renaming for type
-  rename(expr.type(), ns, level);
+  // only do L1!
+  rename(expr.type(), ns, L1);
 
   if(expr.id()==ID_symbol)
   {