From 042ad7477035c0f50705086b0176da860868f9b7 Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 30 Nov 2018 12:26:38 +0000 Subject: [PATCH] Don't use symex_dynamic:: magic string in multiple places --- src/ansi-c/expr2c.cpp | 3 ++- src/goto-instrument/race_check.cpp | 16 ++++++++-------- src/goto-symex/goto_symex_state.cpp | 3 ++- src/goto-symex/symex_builtin_functions.cpp | 8 +++++--- src/solvers/flattening/pointer_logic.cpp | 6 ++++-- src/util/pointer_predicates.h | 2 ++ src/util/simplify_expr_pointer.cpp | 2 +- 7 files changed, 24 insertions(+), 16 deletions(-) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 33e954be03..a17e17848d 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -1653,7 +1654,7 @@ std::string expr2ct::convert_symbol( dest=id2string(entry->second); #if 0 - if(has_prefix(id2string(id), "symex_dynamic::dynamic_object")) + if(has_prefix(id2string(id), SYMEX_DYNAMIC_PREFIX "dynamic_object")) { if(sizeof_nesting++ == 0) dest+=" /*"+convert(src.type()); diff --git a/src/goto-instrument/race_check.cpp b/src/goto-instrument/race_check.cpp index 56227cf82b..f6dbbb6a17 100644 --- a/src/goto-instrument/race_check.cpp +++ b/src/goto-instrument/race_check.cpp @@ -18,6 +18,7 @@ Date: February 2006 #include #include +#include #include "rw_set.h" @@ -123,14 +124,13 @@ static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr) { const irep_idt &identifier=symbol_expr.get_identifier(); - if(identifier==CPROVER_PREFIX "alloc" || - identifier==CPROVER_PREFIX "alloc_size" || - identifier=="stdin" || - identifier=="stdout" || - identifier=="stderr" || - identifier=="sys_nerr" || - has_prefix(id2string(identifier), "symex::invalid_object") || - has_prefix(id2string(identifier), "symex_dynamic::dynamic_object")) + if( + identifier == CPROVER_PREFIX "alloc" || + identifier == CPROVER_PREFIX "alloc_size" || identifier == "stdin" || + identifier == "stdout" || identifier == "stderr" || + identifier == "sys_nerr" || + has_prefix(id2string(identifier), "symex::invalid_object") || + has_prefix(id2string(identifier), SYMEX_DYNAMIC_PREFIX "dynamic_object")) return false; // no race check const symbolt &symbol=ns.lookup(identifier); diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index a043d3bec7..e4d5af7095 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -178,7 +179,7 @@ void goto_symex_statet::assignment( || l1_identifier == guard_identifier() || ns.lookup(l1_identifier).is_shared() || has_prefix(id2string(l1_identifier), "symex::invalid_object") - || has_prefix(id2string(l1_identifier), "symex_dynamic::dynamic_object")); + || has_prefix(id2string(l1_identifier), SYMEX_DYNAMIC_PREFIX "dynamic_object")); #endif // do the l2 renaming diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index a0a09d7228..55af78d76b 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -135,7 +136,8 @@ void goto_symext::symex_allocate( size_symbol.base_name= "dynamic_object_size"+std::to_string(dynamic_counter); - size_symbol.name="symex_dynamic::"+id2string(size_symbol.base_name); + size_symbol.name = + SYMEX_DYNAMIC_PREFIX + id2string(size_symbol.base_name); size_symbol.type=tmp_size.type(); size_symbol.mode = mode; size_symbol.type.set(ID_C_constant, true); @@ -154,7 +156,7 @@ void goto_symext::symex_allocate( symbolt value_symbol; value_symbol.base_name="dynamic_object"+std::to_string(dynamic_counter); - value_symbol.name="symex_dynamic::"+id2string(value_symbol.base_name); + value_symbol.name = SYMEX_DYNAMIC_PREFIX + id2string(value_symbol.base_name); value_symbol.is_lvalue=true; value_symbol.type = *object_type; value_symbol.type.set(ID_C_dynamic, true); @@ -405,7 +407,7 @@ void goto_symext::symex_cpp_new( symbol.base_name= do_array?"dynamic_"+count_string+"_array": "dynamic_"+count_string+"_value"; - symbol.name="symex_dynamic::"+id2string(symbol.base_name); + symbol.name = SYMEX_DYNAMIC_PREFIX + id2string(symbol.base_name); symbol.is_lvalue=true; if(code.get(ID_statement)==ID_cpp_new_array || code.get(ID_statement)==ID_cpp_new) diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp index 69d2f2694b..5c922e9e91 100644 --- a/src/solvers/flattening/pointer_logic.cpp +++ b/src/solvers/flattening/pointer_logic.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -26,8 +27,9 @@ bool pointer_logict::is_dynamic_object(const exprt &expr) const return true; if(expr.id()==ID_symbol) - if(has_prefix(id2string(to_symbol_expr(expr).get_identifier()), - "symex_dynamic::")) + if(has_prefix( + id2string(to_symbol_expr(expr).get_identifier()), + SYMEX_DYNAMIC_PREFIX)) return true; return false; diff --git a/src/util/pointer_predicates.h b/src/util/pointer_predicates.h index a0c88d1192..2771d52f31 100644 --- a/src/util/pointer_predicates.h +++ b/src/util/pointer_predicates.h @@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_POINTER_PREDICATES_H #define CPROVER_UTIL_POINTER_PREDICATES_H +#define SYMEX_DYNAMIC_PREFIX "symex_dynamic::" + class exprt; class namespacet; class typet; diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index 01aa92af14..2fa334ad28 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -550,7 +550,7 @@ bool simplify_exprt::simplify_dynamic_object(exprt &expr) const irep_idt identifier=to_symbol_expr(op.op0()).get_identifier(); // this is for the benefit of symex - expr.make_bool(has_prefix(id2string(identifier), "symex_dynamic::")); + expr.make_bool(has_prefix(id2string(identifier), SYMEX_DYNAMIC_PREFIX)); return false; } else if(op.op0().id()==ID_string_constant)