Skip to content

Commit 042ad74

Browse files
author
thk123
committed
Don't use symex_dynamic:: magic string in multiple places
1 parent b8678a4 commit 042ad74

File tree

7 files changed

+24
-16
lines changed

7 files changed

+24
-16
lines changed

src/ansi-c/expr2c.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ Author: Daniel Kroening, [email protected]
2424
#include <util/lispirep.h>
2525
#include <util/namespace.h>
2626
#include <util/pointer_offset_size.h>
27+
#include <util/pointer_predicates.h>
2728
#include <util/prefix.h>
2829
#include <util/string_constant.h>
2930
#include <util/suffix.h>
@@ -1653,7 +1654,7 @@ std::string expr2ct::convert_symbol(
16531654
dest=id2string(entry->second);
16541655

16551656
#if 0
1656-
if(has_prefix(id2string(id), "symex_dynamic::dynamic_object"))
1657+
if(has_prefix(id2string(id), SYMEX_DYNAMIC_PREFIX "dynamic_object"))
16571658
{
16581659
if(sizeof_nesting++ == 0)
16591660
dest+=" /*"+convert(src.type());

src/goto-instrument/race_check.cpp

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ Date: February 2006
1818
#include <goto-programs/remove_skip.h>
1919

2020
#include <linking/static_lifetime_init.h>
21+
#include <util/pointer_predicates.h>
2122

2223
#include "rw_set.h"
2324

@@ -123,14 +124,13 @@ static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
123124
{
124125
const irep_idt &identifier=symbol_expr.get_identifier();
125126

126-
if(identifier==CPROVER_PREFIX "alloc" ||
127-
identifier==CPROVER_PREFIX "alloc_size" ||
128-
identifier=="stdin" ||
129-
identifier=="stdout" ||
130-
identifier=="stderr" ||
131-
identifier=="sys_nerr" ||
132-
has_prefix(id2string(identifier), "symex::invalid_object") ||
133-
has_prefix(id2string(identifier), "symex_dynamic::dynamic_object"))
127+
if(
128+
identifier == CPROVER_PREFIX "alloc" ||
129+
identifier == CPROVER_PREFIX "alloc_size" || identifier == "stdin" ||
130+
identifier == "stdout" || identifier == "stderr" ||
131+
identifier == "sys_nerr" ||
132+
has_prefix(id2string(identifier), "symex::invalid_object") ||
133+
has_prefix(id2string(identifier), SYMEX_DYNAMIC_PREFIX "dynamic_object"))
134134
return false; // no race check
135135

136136
const symbolt &symbol=ns.lookup(identifier);

src/goto-symex/goto_symex_state.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
2121
#include <util/format.h>
2222
#include <util/format_expr.h>
2323
#include <util/invariant.h>
24+
#include <util/pointer_predicates.h>
2425
#include <util/prefix.h>
2526
#include <util/std_expr.h>
2627

@@ -178,7 +179,7 @@ void goto_symex_statet::assignment(
178179
|| l1_identifier == guard_identifier()
179180
|| ns.lookup(l1_identifier).is_shared()
180181
|| has_prefix(id2string(l1_identifier), "symex::invalid_object")
181-
|| has_prefix(id2string(l1_identifier), "symex_dynamic::dynamic_object"));
182+
|| has_prefix(id2string(l1_identifier), SYMEX_DYNAMIC_PREFIX "dynamic_object"));
182183
#endif
183184

184185
// do the l2 renaming

src/goto-symex/symex_builtin_functions.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
1717
#include <util/invariant_utils.h>
1818
#include <util/optional.h>
1919
#include <util/pointer_offset_size.h>
20+
#include <util/pointer_predicates.h>
2021
#include <util/prefix.h>
2122
#include <util/simplify_expr.h>
2223
#include <util/string2int.h>
@@ -135,7 +136,8 @@ void goto_symext::symex_allocate(
135136

136137
size_symbol.base_name=
137138
"dynamic_object_size"+std::to_string(dynamic_counter);
138-
size_symbol.name="symex_dynamic::"+id2string(size_symbol.base_name);
139+
size_symbol.name =
140+
SYMEX_DYNAMIC_PREFIX + id2string(size_symbol.base_name);
139141
size_symbol.type=tmp_size.type();
140142
size_symbol.mode = mode;
141143
size_symbol.type.set(ID_C_constant, true);
@@ -154,7 +156,7 @@ void goto_symext::symex_allocate(
154156
symbolt value_symbol;
155157

156158
value_symbol.base_name="dynamic_object"+std::to_string(dynamic_counter);
157-
value_symbol.name="symex_dynamic::"+id2string(value_symbol.base_name);
159+
value_symbol.name = SYMEX_DYNAMIC_PREFIX + id2string(value_symbol.base_name);
158160
value_symbol.is_lvalue=true;
159161
value_symbol.type = *object_type;
160162
value_symbol.type.set(ID_C_dynamic, true);
@@ -405,7 +407,7 @@ void goto_symext::symex_cpp_new(
405407
symbol.base_name=
406408
do_array?"dynamic_"+count_string+"_array":
407409
"dynamic_"+count_string+"_value";
408-
symbol.name="symex_dynamic::"+id2string(symbol.base_name);
410+
symbol.name = SYMEX_DYNAMIC_PREFIX + id2string(symbol.base_name);
409411
symbol.is_lvalue=true;
410412
if(code.get(ID_statement)==ID_cpp_new_array ||
411413
code.get(ID_statement)==ID_cpp_new)

src/solvers/flattening/pointer_logic.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
1616
#include <util/c_types.h>
1717
#include <util/invariant.h>
1818
#include <util/pointer_offset_size.h>
19+
#include <util/pointer_predicates.h>
1920
#include <util/prefix.h>
2021
#include <util/simplify_expr.h>
2122
#include <util/std_expr.h>
@@ -26,8 +27,9 @@ bool pointer_logict::is_dynamic_object(const exprt &expr) const
2627
return true;
2728

2829
if(expr.id()==ID_symbol)
29-
if(has_prefix(id2string(to_symbol_expr(expr).get_identifier()),
30-
"symex_dynamic::"))
30+
if(has_prefix(
31+
id2string(to_symbol_expr(expr).get_identifier()),
32+
SYMEX_DYNAMIC_PREFIX))
3133
return true;
3234

3335
return false;

src/util/pointer_predicates.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]
1212
#ifndef CPROVER_UTIL_POINTER_PREDICATES_H
1313
#define CPROVER_UTIL_POINTER_PREDICATES_H
1414

15+
#define SYMEX_DYNAMIC_PREFIX "symex_dynamic::"
16+
1517
class exprt;
1618
class namespacet;
1719
class typet;

src/util/simplify_expr_pointer.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -550,7 +550,7 @@ bool simplify_exprt::simplify_dynamic_object(exprt &expr)
550550
const irep_idt identifier=to_symbol_expr(op.op0()).get_identifier();
551551

552552
// this is for the benefit of symex
553-
expr.make_bool(has_prefix(id2string(identifier), "symex_dynamic::"));
553+
expr.make_bool(has_prefix(id2string(identifier), SYMEX_DYNAMIC_PREFIX));
554554
return false;
555555
}
556556
else if(op.op0().id()==ID_string_constant)

0 commit comments

Comments
 (0)