Skip to content

Commit 12ef9e7

Browse files
authored
Merge pull request #6673 from tautschnig/cleanup/remove-deprecated-string-abstraction-api
Remove deprecated string abstraction methods
2 parents a3e1411 + 3f9f055 commit 12ef9e7

File tree

2 files changed

+32
-53
lines changed

2 files changed

+32
-53
lines changed

src/goto-programs/string_abstraction.cpp

Lines changed: 24 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -67,29 +67,19 @@ static inline bool is_ptr_argument(const typet &type)
6767
return type.id()==ID_pointer;
6868
}
6969

70-
void string_abstraction(
71-
symbol_tablet &symbol_table,
72-
message_handlert &message_handler,
73-
goto_functionst &dest)
74-
{
75-
string_abstractiont string_abstraction(symbol_table, message_handler);
76-
string_abstraction(dest);
77-
}
78-
7970
void string_abstraction(
8071
goto_modelt &goto_model,
8172
message_handlert &message_handler)
8273
{
83-
string_abstractiont{goto_model.symbol_table, message_handler}.apply(
84-
goto_model);
74+
string_abstractiont{goto_model, message_handler}.apply();
8575
}
8676

8777
string_abstractiont::string_abstractiont(
88-
symbol_tablet &_symbol_table,
78+
goto_modelt &goto_model,
8979
message_handlert &_message_handler)
9080
: sym_suffix("#str$fcn"),
91-
symbol_table(_symbol_table),
92-
ns(_symbol_table),
81+
goto_model(goto_model),
82+
ns(goto_model.symbol_table),
9383
temporary_counter(0),
9484
message_handler(_message_handler)
9585
{
@@ -101,7 +91,13 @@ string_abstractiont::string_abstractiont(
10191
s.components()[2].set_pretty_name("size");
10292

10393
symbolt &struct_symbol = get_fresh_aux_symbol(
104-
s, "tag-", "string_struct", source_locationt{}, ID_C, ns, symbol_table);
94+
s,
95+
"tag-",
96+
"string_struct",
97+
source_locationt{},
98+
ID_C,
99+
ns,
100+
goto_model.symbol_table);
105101
struct_symbol.is_type = true;
106102
struct_symbol.is_lvalue = false;
107103
struct_symbol.is_state_var = false;
@@ -129,13 +125,11 @@ typet string_abstractiont::build_type(whatt what)
129125
return type;
130126
}
131127

132-
void string_abstractiont::apply(goto_modelt &goto_model)
128+
void string_abstractiont::apply()
133129
{
134-
operator()(goto_model.goto_functions);
135-
}
130+
goto_functionst &dest = goto_model.goto_functions;
131+
symbol_tablet &symbol_table = goto_model.symbol_table;
136132

137-
void string_abstractiont::operator()(goto_functionst &dest)
138-
{
139133
// iterate over all previously known symbols as the body of the loop modifies
140134
// the symbol table and can thus invalidate iterators
141135
for(auto &sym_name : symbol_table.sorted_symbol_names())
@@ -184,7 +178,7 @@ void string_abstractiont::operator()(goto_functionst &dest)
184178
}
185179
}
186180

187-
void string_abstractiont::operator()(goto_programt &dest)
181+
void string_abstractiont::apply(goto_programt &dest)
188182
{
189183
abstract(dest);
190184

@@ -238,7 +232,7 @@ code_typet::parametert string_abstractiont::add_parameter(
238232
"#str",
239233
fct_symbol.location,
240234
fct_symbol.mode,
241-
symbol_table);
235+
goto_model.symbol_table);
242236
param_symbol.is_parameter = true;
243237
param_symbol.value.make_nil();
244238

@@ -462,7 +456,7 @@ symbol_exprt string_abstractiont::add_dummy_symbol_and_value(
462456
ref_instr->source_location();
463457
}
464458

465-
symbol_table.insert(std::move(new_symbol));
459+
goto_model.symbol_table.insert(std::move(new_symbol));
466460

467461
return sym_expr;
468462
}
@@ -767,7 +761,7 @@ const typet &string_abstractiont::build_abstraction_type_rec(const typet &type,
767761
existing_tag_symbol.location,
768762
existing_tag_symbol.mode,
769763
ns,
770-
symbol_table);
764+
goto_model.symbol_table);
771765
abstracted_type_symbol.is_type = true;
772766
abstracted_type_symbol.is_lvalue = false;
773767
abstracted_type_symbol.is_state_var = false;
@@ -988,7 +982,7 @@ exprt string_abstractiont::build_unknown(const typet &type, bool write)
988982
new_symbol.mode=ID_C;
989983
new_symbol.pretty_name=identifier;
990984

991-
symbol_table.insert(std::move(new_symbol));
985+
goto_model.symbol_table.insert(std::move(new_symbol));
992986

993987
return ns.lookup(identifier).symbol_expr();
994988
}
@@ -1014,14 +1008,14 @@ bool string_abstractiont::build_symbol(const symbol_exprt &sym, exprt &dest)
10141008
std::string sym_suffix_before = sym_suffix;
10151009
sym_suffix = "#str";
10161010
identifier = id2string(symbol.name) + sym_suffix;
1017-
if(symbol_table.symbols.find(identifier) == symbol_table.symbols.end())
1011+
if(!goto_model.symbol_table.has_symbol(identifier))
10181012
build_new_symbol(symbol, identifier, abstract_type);
10191013
sym_suffix = sym_suffix_before;
10201014
}
10211015
else
10221016
{
10231017
identifier=id2string(symbol.name)+sym_suffix;
1024-
if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end())
1018+
if(!goto_model.symbol_table.has_symbol(identifier))
10251019
build_new_symbol(symbol, identifier, abstract_type);
10261020
}
10271021

@@ -1053,7 +1047,7 @@ void string_abstractiont::build_new_symbol(const symbolt &symbol,
10531047
new_symbol.is_static_lifetime=symbol.is_static_lifetime;
10541048
new_symbol.is_thread_local=symbol.is_thread_local;
10551049

1056-
symbol_table.insert(std::move(new_symbol));
1050+
goto_model.symbol_table.insert(std::move(new_symbol));
10571051

10581052
if(symbol.is_static_lifetime)
10591053
{
@@ -1074,8 +1068,7 @@ bool string_abstractiont::build_symbol_constant(
10741068
+"_"+integer2string(buf_size);
10751069
irep_idt identifier="string_abstraction::"+id2string(base);
10761070

1077-
if(symbol_table.symbols.find(identifier)==
1078-
symbol_table.symbols.end())
1071+
if(!goto_model.symbol_table.has_symbol(identifier))
10791072
{
10801073
auxiliary_symbolt new_symbol;
10811074
new_symbol.type=string_struct;
@@ -1100,7 +1093,7 @@ bool string_abstractiont::build_symbol_constant(
11001093
code_assignt(new_symbol.symbol_expr(), value)));
11011094
}
11021095

1103-
symbol_table.insert(std::move(new_symbol));
1096+
goto_model.symbol_table.insert(std::move(new_symbol));
11041097
}
11051098

11061099
dest=address_of_exprt(symbol_exprt(identifier, string_struct));

src/goto-programs/string_abstraction.h

Lines changed: 8 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@ Author: Daniel Kroening, [email protected]
1414

1515
#include <util/bitvector_types.h>
1616
#include <util/config.h>
17-
#include <util/deprecate.h>
1817
#include <util/namespace.h>
1918
#include <util/std_expr.h>
2019

@@ -34,33 +33,27 @@ class message_handlert;
3433
class string_abstractiont
3534
{
3635
public:
37-
// To be deprecated once the operator() methods have been removed, at which
38-
// point a new constructor that only takes a message_handler should be
39-
// introduced.
40-
string_abstractiont(
41-
symbol_tablet &_symbol_table,
42-
message_handlert &_message_handler);
43-
44-
DEPRECATED(SINCE(2020, 12, 14, "Use apply(goto_modelt &)"))
45-
void operator()(goto_programt &dest);
46-
DEPRECATED(SINCE(2020, 12, 14, "Use apply(goto_modelt &)"))
47-
void operator()(goto_functionst &dest);
48-
4936
/// Apply string abstraction to \p goto_model. If any abstractions are to be
5037
/// applied, the affected goto_functions and any affected symbols will be
5138
/// modified.
52-
void apply(goto_modelt &goto_model);
39+
string_abstractiont(
40+
goto_modelt &goto_model,
41+
message_handlert &_message_handler);
42+
43+
void apply();
5344

5445
protected:
5546
std::string sym_suffix;
56-
symbol_tablet &symbol_table;
47+
goto_modelt &goto_model;
5748
namespacet ns;
5849
unsigned temporary_counter;
5950
message_handlert &message_handler;
6051

6152
typedef ::std::map< typet, typet > abstraction_types_mapt;
6253
abstraction_types_mapt abstraction_types_map;
6354

55+
void apply(goto_programt &dest);
56+
6457
static bool has_string_macros(const exprt &expr);
6558

6659
void replace_string_macros(
@@ -190,11 +183,4 @@ void string_abstraction(
190183
goto_modelt &,
191184
message_handlert &);
192185

193-
DEPRECATED(
194-
SINCE(2020, 12, 14, "Use string_abstraction(goto_model, message_handler)"))
195-
void string_abstraction(
196-
symbol_tablet &,
197-
message_handlert &,
198-
goto_functionst &);
199-
200186
#endif // CPROVER_GOTO_PROGRAMS_STRING_ABSTRACTION_H

0 commit comments

Comments
 (0)