Don't try to create CPROVER_memory references when processing a Java source program.

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>
@@ -410,6 +411,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

@@ -51,6 +51,7 @@ class goto_symext
     new_symbol_table(_new_symbol_table),
     ns(_ns),
     target(_target),
+    mode(),
     atomic_section_counter(0),
     guard_identifier("goto_symex::\\guard")
   {
@@ -95,9 +96,11 @@ class goto_symext
   optionst options;
   symbol_tablet &new_symbol_table;
 
+  irep_idt mode;
+
 protected:
   const namespacet &ns;
-  symex_targett ⌖  
+  symex_targett ⌖
   unsigned atomic_section_counter;
 
   friend class symex_dereference_statet;

src/goto-symex/symex_dereference.cpp

@@ -295,7 +295,8 @@ 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(

src/pointer-analysis/value_set_dereference.cpp

@@ -463,6 +463,12 @@ 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[...].
 
+    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);
 

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(