Merge pull request #335 from smowton/disable_cprover_memory_for_java

Disable cprover memory for java

Author: Daniel Kroening

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>
@@ -431,6 +432,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.language_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),
+    language_mode(),
     ns(_ns),
     target(_target),
     atomic_section_counter(0),
@@ -95,6 +96,10 @@ class goto_symext
   optionst options;
   symbol_tablet &new_symbol_table;
 
+  /// language_mode: ID_java, ID_C or another language identifier
+  /// if we know the source language in use, irep_idt() otherwise.
+  irep_idt language_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,
+      language_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/goto_program_dereference.h

@@ -19,6 +19,10 @@ Author: Daniel Kroening, [email protected]
 class goto_program_dereferencet:protected dereference_callbackt
 {
 public:
+  // Note: this currently doesn't specify a source language
+  // for the final argument to value_set_dereferencet.
+  // This means that language-inappropriate values such as
+  // (struct A*)some_integer_value in Java, may be returned.
   goto_program_dereferencet(
     const namespacet &_ns,
     symbol_tablet &_new_symbol_table,
@@ -27,7 +31,7 @@ class goto_program_dereferencet:protected dereference_callbackt
     options(_options),
     ns(_ns),
     value_sets(_value_sets),
-    dereference(_ns, _new_symbol_table, _options, *this) { }
+    dereference(_ns, _new_symbol_table, _options, *this, ID_nil) { }
 
   void dereference_program(
     goto_programt &goto_program,

src/pointer-analysis/value_set_dereference.cpp

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

@@ -37,11 +37,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):
     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() { }
@@ -78,6 +80,9 @@ class value_set_dereferencet
   symbol_tablet &new_symbol_table;
   const optionst &options;
   dereference_callbackt &dereference_callback;
+  /// language_mode: ID_java, ID_C or another language identifier
+  /// if we know the source language in use, irep_idt() otherwise.
+  const irep_idt language_mode;
   static unsigned invalid_counter;
 
   bool dereference_type_compare(