Don't reference CPROVER_memory from Java code. Fixes #197.

goto-symex's value-set analysis can reach the conclusion that an integer may be cast
to a pointer, and so generate a reference to the __CPROVER_memory symbol. This is
invalid in Java however, since the symbol is not defined and of course Java cannot
express dereferencing a non-pointer type.

This change disables generation of __CPROVER_memory references when a Java-typed
entry point is found. I couldn't provide a test case against master at this time however
because the examples in both of the above bugs now succeed against master, presumably
because value-set analysis has been improved and is harder to confuse into introducing
a pointer-to-int cast.

Author: smowton

src/cbmc/bmc.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/time_stopping.h>
 #include <util/message.h>
 #include <util/json.h>
+#include <util/cprover_prefix.h>
 
 #include <langapi/mode.h>
 #include <langapi/languages.h>
@@ -428,6 +429,12 @@ safety_checkert::resultt bmct::run(
   symex.set_message_handler(get_message_handler());
   symex.options=options;
 
+  {
+    const symbolt *init_symbol;
+    if(!ns.lookup(CPROVER_PREFIX "initialize", init_symbol))
+      symex.mode=init_symbol->mode;
+  }  
+
   status() << "Starting Bounded Model Checking" << eom;
 
   symex.last_source_location.make_nil();

src/goto-symex/goto_symex.h

@@ -49,6 +49,7 @@ class goto_symext
     remaining_vccs(0),
     constant_propagation(true),
     new_symbol_table(_new_symbol_table),
+    mode(),
     ns(_ns),
     target(_target),
     atomic_section_counter(0),
@@ -95,6 +96,8 @@ class goto_symext
   optionst options;
   symbol_tablet &new_symbol_table;
 
+  irep_idt mode;
+
 protected:
   const namespacet &ns;
   symex_targett ⌖

src/goto-symex/symex_dereference.cpp

@@ -295,8 +295,9 @@ void goto_symext::dereference_rec(
       ns,
       new_symbol_table,
       options,
-      symex_dereference_state);
-
+      symex_dereference_state,
+      mode);      
+    
     // std::cout << "**** " << from_expr(ns, "", tmp1) << std::endl;
     exprt tmp2=dereference.dereference(
       tmp1, guard, write?value_set_dereferencet::WRITE:value_set_dereferencet::READ);

src/pointer-analysis/value_set_dereference.cpp

@@ -454,7 +454,13 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
     // This is stuff like *((char *)5).
     // This is turned into an access to __CPROVER_memory[...].
 
-    const symbolt &memory_symbol=ns.lookup(CPROVER_PREFIX "memory");
+    if(language_mode==ID_java)
+    {
+      result.value=nil_exprt();
+      return result;
+    }
+    
+    const symbolt &memory_symbol=ns.lookup(CPROVER_PREFIX "memory");    
     exprt symbol_expr=symbol_exprt(memory_symbol.name, memory_symbol.type);
 
     exprt pointer_offset=unary_exprt(

src/pointer-analysis/value_set_dereference.h

@@ -39,11 +39,13 @@ class value_set_dereferencet
     const namespacet &_ns,
     symbol_tablet &_new_symbol_table,
     const optionst &_options,
-    dereference_callbackt &_dereference_callback):
+    dereference_callbackt &_dereference_callback,
+    const irep_idt _language_mode = irep_idt()):
     ns(_ns),
     new_symbol_table(_new_symbol_table),
     options(_options),
-    dereference_callback(_dereference_callback)
+    dereference_callback(_dereference_callback),
+    language_mode(_language_mode)
   { }
 
   virtual ~value_set_dereferencet() { }
@@ -80,6 +82,7 @@ class value_set_dereferencet
   symbol_tablet &new_symbol_table;
   const optionst &options;
   dereference_callbackt &dereference_callback;
+  const irep_idt language_mode;
   static unsigned invalid_counter;
 
   bool dereference_type_compare(