diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index 8132097565c..fb7596719d8 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -19,6 +19,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../pointer-analysis/add_failed_symbols$(OBJEXT) \ ../pointer-analysis/rewrite_index$(OBJEXT) \ ../pointer-analysis/goto_program_dereference$(OBJEXT) \ + ../pointer-analysis/dynamic_object_name$(OBJEXT) \ ../goto-instrument/full_slicer$(OBJEXT) \ ../goto-instrument/nondet_static$(OBJEXT) \ ../goto-instrument/cover$(OBJEXT) \ diff --git a/src/cegis/Makefile b/src/cegis/Makefile index f1a38ce4915..d11950cc14d 100644 --- a/src/cegis/Makefile +++ b/src/cegis/Makefile @@ -100,6 +100,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../pointer-analysis/add_failed_symbols$(OBJEXT) \ ../pointer-analysis/rewrite_index$(OBJEXT) \ ../pointer-analysis/goto_program_dereference$(OBJEXT) \ + ../pointer-analysis/dynamic_object_name$(OBJEXT) \ ../goto-instrument/full_slicer$(OBJEXT) \ ../analyses/analyses$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ diff --git a/src/pointer-analysis/Makefile b/src/pointer-analysis/Makefile index 95df6698b23..28d6bebb9d8 100644 --- a/src/pointer-analysis/Makefile +++ b/src/pointer-analysis/Makefile @@ -5,7 +5,9 @@ SRC = value_set.cpp goto_program_dereference.cpp value_set_analysis.cpp \ value_set_analysis_fivr.cpp value_set_fivr.cpp value_set_domain_fivr.cpp \ value_set_analysis_fivrns.cpp value_set_fivrns.cpp \ value_set_domain_fivrns.cpp value_set_dereference.cpp \ - dereference_callback.cpp + dereference_callback.cpp \ + dynamic_object_name.cpp \ + # No more source files INCLUDES= -I .. diff --git a/src/pointer-analysis/dynamic_object_name.cpp b/src/pointer-analysis/dynamic_object_name.cpp new file mode 100644 index 00000000000..0446a15eb4d --- /dev/null +++ b/src/pointer-analysis/dynamic_object_name.cpp @@ -0,0 +1,18 @@ +/*******************************************************************\ + +Module: Dynamic object name + +Author: Marius-Constantin Melemciuc + +Date: April 2017 + +@ Copyright Diffblue, Ltd. + +\*******************************************************************/ + +#include "dynamic_object_name.h" + +// We use std::string concatenation regularly with this string +// NOLINTNEXTLINE(runtime/string) +const std::string prefix_dynamic_object="value_set::dynamic_object"; + diff --git a/src/pointer-analysis/dynamic_object_name.h b/src/pointer-analysis/dynamic_object_name.h index aaeefaad5e8..ade83d59e02 100644 --- a/src/pointer-analysis/dynamic_object_name.h +++ b/src/pointer-analysis/dynamic_object_name.h @@ -17,6 +17,8 @@ Date: April 2017 #include +extern const std::string prefix_dynamic_object; + /*******************************************************************\ Function: get_dynamic_object_name @@ -38,7 +40,7 @@ inline std::string get_dynamic_object_name( const dynamic_object_exprt &dynamic_object) { std::string name= - "value_set::dynamic_object"+ + prefix_dynamic_object+ std::to_string(dynamic_object.get_instance()); if(dynamic_object.get_recency()== diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 75c644f28c1..b83ed38fbf9 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -51,7 +51,7 @@ bool value_sett::field_sensitive( const namespacet &ns) { // we always track fields on these - if(has_prefix(id2string(id), "value_set::dynamic_object") || + if(has_prefix(id2string(id), prefix_dynamic_object) || id=="value_set::return_value" || id=="value_set::memory") return true; @@ -152,7 +152,7 @@ void value_sett::output( const entryt &e=v_it->second; - if(has_prefix(id2string(e.identifier), "value_set::dynamic_object")) + if(has_prefix(id2string(e.identifier), prefix_dynamic_object)) { display_name=id2string(e.identifier)+e.suffix; identifier=""; diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index 976f68ab490..0fd9eaa6565 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -64,7 +64,7 @@ void value_set_fit::output( const entryt &e=v_it->second; - if(has_prefix(id2string(e.identifier), "value_set::dynamic_object")) + if(has_prefix(id2string(e.identifier), prefix_dynamic_object)) { display_name=id2string(e.identifier)+e.suffix; identifier=""; @@ -316,7 +316,7 @@ bool value_set_fit::make_union(const value_set_fit::valuest &new_values) { // we always track these if(has_prefix(id2string(it->second.identifier), - "value_set::dynamic_object") || + prefix_dynamic_object) || has_prefix(id2string(it->second.identifier), "value_set::return_value")) { @@ -1434,7 +1434,7 @@ void value_set_fit::assign_rec( const irep_idt &identifier=lhs.get(ID_identifier); if(has_prefix(id2string(identifier), - "value_set::dynamic_object") || + prefix_dynamic_object) || has_prefix(id2string(identifier), "value_set::return_value") || values.find(id2string(identifier)+suffix)!=values.end()) diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp index 7b65acd9f06..5becc34b8c2 100644 --- a/src/pointer-analysis/value_set_fivr.cpp +++ b/src/pointer-analysis/value_set_fivr.cpp @@ -1562,7 +1562,7 @@ void value_set_fivrt::assign_rec( const irep_idt &identifier=lhs.get(ID_identifier); if(has_prefix(id2string(identifier), - "value_set::dynamic_object") || + prefix_dynamic_object) || has_prefix(id2string(identifier), "value_set::return_value") || values.find(id2string(identifier)+suffix)!=values.end()) diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp index a50e1a0edbc..7d0c2f198d2 100644 --- a/src/pointer-analysis/value_set_fivrns.cpp +++ b/src/pointer-analysis/value_set_fivrns.cpp @@ -1202,7 +1202,7 @@ void value_set_fivrnst::assign_rec( const irep_idt &identifier=lhs.get(ID_identifier); if(has_prefix(id2string(identifier), - "value_set::dynamic_object") || + prefix_dynamic_object) || has_prefix(id2string(identifier), "value_set::return_value") || values.find(id2string(identifier)+suffix)!=values.end())