From 81dd624fbdfc721adcad8ad2df7121bebbf074b7 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 31 Aug 2016 09:24:54 +0100 Subject: [PATCH 1/2] Don't try to create CPROVER_memory references when processing a Java source program. --- src/cbmc/bmc.cpp | 7 +++++++ src/goto-symex/goto_symex.h | 5 ++++- src/goto-symex/symex_dereference.cpp | 3 ++- src/pointer-analysis/value_set_dereference.cpp | 6 ++++++ src/pointer-analysis/value_set_dereference.h | 7 +++++-- 5 files changed, 24 insertions(+), 4 deletions(-) diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 4072452112f..94d04b995cf 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -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(); diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 15f05453921..84fca76ad34 100644 --- a/src/goto-symex/goto_symex.h +++ b/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; diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index 007c74576a6..52e0eec28f7 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/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( diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 6aeb3980a0b..34c428d6f4b 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -454,6 +454,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); diff --git a/src/pointer-analysis/value_set_dereference.h b/src/pointer-analysis/value_set_dereference.h index 5f7f8b45612..ed8054be028 100644 --- a/src/pointer-analysis/value_set_dereference.h +++ b/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( From 9100eb4bdeb489185b7c7af00fd46ec2c0865f34 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 20 Oct 2016 12:26:54 +0100 Subject: [PATCH 2/2] Fix initialisation order --- src/goto-symex/goto_symex.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 84fca76ad34..aede6b453ec 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -49,9 +49,9 @@ class goto_symext remaining_vccs(0), constant_propagation(true), new_symbol_table(_new_symbol_table), + mode(), ns(_ns), target(_target), - mode(), atomic_section_counter(0), guard_identifier("goto_symex::\\guard") {