Skip to content

Commit 7601bb1

Browse files
tautschnigtautschnig
authored
Merge pull request #8040 from tautschnig/cleanup/dstring
Cleanup USE_STD_STRING/USE_DSTRING configuration option
2 parents c8aae0d + c26d38c commit 7601bb1

37 files changed

+99
-74
lines changed

Diff for: ‎jbmc/src/java_bytecode/character_refine_preprocess.h

+1
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ Date: March 2017
2323
#include <util/mp_arith.h>
2424
#include <util/std_code_base.h>
2525

26+
#include <list>
2627
#include <unordered_map>
2728

2829
class code_function_callt;

Diff for: ‎jbmc/src/java_bytecode/java_bytecode_parse_tree.h

+4-3
Original file line numberDiff line numberDiff line change
@@ -10,14 +10,15 @@ Author: Daniel Kroening, [email protected]
1010
#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H
1111
#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H
1212

13-
#include <set>
14-
#include <map>
15-
1613
#include <util/std_types.h>
1714

1815
#include "bytecode_info.h"
1916
#include "java_types.h"
2017

18+
#include <list>
19+
#include <map>
20+
#include <set>
21+
2122
struct java_bytecode_parse_treet
2223
{
2324
// Disallow copy construction and copy assignment, but allow move construction

Diff for: ‎jbmc/src/java_bytecode/java_class_loader_base.h

+2
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,8 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include "jar_pool.h"
1515

16+
#include <list>
17+
1618
class message_handlert;
1719
struct java_bytecode_parse_treet;
1820

Diff for: ‎src/crangler/c_wrangler.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ Author: Daniel Kroening, [email protected]
2323

2424
#include <fstream> // IWYU pragma: keep
2525
#include <iostream>
26+
#include <list>
2627
#include <map>
2728
#include <regex>
2829
#include <sstream>

Diff for: ‎src/goto-cc/compile.h

+1
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ Date: June 2006
1818
#include <util/std_types.h>
1919
#include <util/symbol.h>
2020

21+
#include <list>
2122
#include <map>
2223

2324
class cmdlinet;

Diff for: ‎src/goto-cc/ld_mode.h

+2
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,8 @@ Date: June 2006
1717
#include "gcc_message_handler.h"
1818
#include "goto_cc_mode.h"
1919

20+
#include <list>
21+
2022
class ld_modet : public goto_cc_modet
2123
{
2224
public:

Diff for: ‎src/goto-cc/linker_script_merge.h

+3-2
Original file line numberDiff line numberDiff line change
@@ -5,11 +5,12 @@
55
#ifndef CPROVER_GOTO_CC_LINKER_SCRIPT_MERGE_H
66
#define CPROVER_GOTO_CC_LINKER_SCRIPT_MERGE_H
77

8+
#include <util/message.h>
9+
810
#include <functional>
11+
#include <list>
912
#include <map>
1013

11-
#include <util/message.h>
12-
1314
class cmdlinet;
1415
class exprt; // IWYU pragma: keep
1516
class goto_modelt;

Diff for: ‎src/goto-harness/recursive_initialization.h

+5-4
Original file line numberDiff line numberDiff line change
@@ -9,15 +9,16 @@ Author: Diffblue Ltd.
99
#ifndef CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H
1010
#define CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H
1111

12-
#include <map>
13-
#include <set>
14-
#include <unordered_set>
15-
1612
#include <util/cprover_prefix.h>
1713
#include <util/prefix.h>
1814
#include <util/std_expr.h>
1915
#include <util/symbol.h>
2016

17+
#include <list>
18+
#include <map>
19+
#include <set>
20+
#include <unordered_set>
21+
2122
class code_blockt;
2223
class goto_modelt;
2324

Diff for: ‎src/goto-programs/goto_program.h

+5-4
Original file line numberDiff line numberDiff line change
@@ -12,16 +12,17 @@ Author: Daniel Kroening, [email protected]
1212
#ifndef CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
1313
#define CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
1414

15+
#include <util/invariant.h>
16+
#include <util/source_location.h>
17+
1518
#include "goto_instruction_code.h"
1619

1720
#include <iosfwd>
18-
#include <set>
1921
#include <limits>
22+
#include <list>
23+
#include <set>
2024
#include <string>
2125

22-
#include <util/invariant.h>
23-
#include <util/source_location.h>
24-
2526
class code_gotot;
2627
class namespacet;
2728
enum class validation_modet;

Diff for: ‎src/goto-programs/graphml_witness.cpp

+3
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,9 @@ Author: Daniel Kroening
2020
#include <util/prefix.h>
2121
#include <util/ssa_expr.h>
2222
#include <util/string_constant.h>
23+
#ifndef USE_DSTRING
24+
# include <util/string_container.h>
25+
#endif
2326
#include <util/symbol.h>
2427

2528
#include <ansi-c/expr2c.h>

Diff for: ‎src/goto-symex/symex_main.cpp

+6-6
Original file line numberDiff line numberDiff line change
@@ -9,24 +9,24 @@ Author: Daniel Kroening, [email protected]
99
/// \file
1010
/// Symbolic Execution
1111

12-
#include "goto_symex.h"
13-
14-
#include <memory>
15-
16-
#include <pointer-analysis/value_set_dereference.h>
17-
1812
#include <util/exception_utils.h>
1913
#include <util/expr_iterator.h>
2014
#include <util/expr_util.h>
2115
#include <util/format.h>
2216
#include <util/format_expr.h>
2317
#include <util/invariant.h>
18+
#include <util/magic.h>
2419
#include <util/mathematical_expr.h>
2520
#include <util/replace_symbol.h>
2621
#include <util/std_expr.h>
2722

23+
#include <pointer-analysis/value_set_dereference.h>
24+
25+
#include "goto_symex.h"
2826
#include "path_storage.h"
2927

28+
#include <memory>
29+
3030
symex_configt::symex_configt(const optionst &options)
3131
: max_depth(options.get_unsigned_int_option("depth")),
3232
doing_path_exploration(options.is_set("paths")),

Diff for: ‎src/goto-synthesizer/expr_enumerator.h

+1
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: Qinheping Hu
1111

1212
#include <util/expr.h>
1313

14+
#include <list>
1415
#include <map>
1516
#include <set>
1617

Diff for: ‎src/libcprover-cpp/verification_result.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -114,7 +114,7 @@ std::vector<std::string> verification_resultt::get_property_ids() const
114114
std::vector<std::string> result;
115115
for(const auto &props : _impl->get_properties())
116116
{
117-
result.push_back(as_string(props.first));
117+
result.push_back(id2string(props.first));
118118
}
119119
return result;
120120
}

Diff for: ‎src/solvers/flattening/bv_utils.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
88

99
#include "bv_utils.h"
1010

11+
#include <list>
1112
#include <utility>
1213

1314
bvt bv_utilst::build_constant(const mp_integer &n, std::size_t width)

Diff for: ‎src/solvers/smt2_incremental/response_or_error.h

-5
Original file line numberDiff line numberDiff line change
@@ -20,11 +20,6 @@ class response_or_errort final
2020
{
2121
}
2222

23-
explicit response_or_errort(std::string message)
24-
: smt_or_messages{std::vector<std::string>{std::move(message)}}
25-
{
26-
}
27-
2823
explicit response_or_errort(std::vector<std::string> messages)
2924
: smt_or_messages{std::move(messages)}
3025
{

Diff for: ‎src/solvers/smt2_incremental/smt_response_validation.cpp

+17-17
Original file line numberDiff line numberDiff line change
@@ -139,14 +139,14 @@ valid_smt_error_response(const irept &parse_tree)
139139
// unexpected in the parse tree is now considered to be an invalid response.
140140
if(parse_tree.get_sub().size() == 1)
141141
{
142-
return {response_or_errort<smt_responset>{
143-
"Error response is missing the error message."}};
142+
return {response_or_errort<smt_responset>{std::vector<std::string>{
143+
{"Error response is missing the error message."}}}};
144144
}
145145
if(parse_tree.get_sub().size() > 2)
146146
{
147-
return {response_or_errort<smt_responset>{
148-
"Error response has multiple error messages - \"" +
149-
print_parse_tree(parse_tree) + "\"."}};
147+
return {response_or_errort<smt_responset>{std::vector<std::string>{
148+
{"Error response has multiple error messages - \"" +
149+
print_parse_tree(parse_tree) + "\"."}}}};
150150
}
151151
return validation_propagating<smt_error_responset, smt_responset>(
152152
validate_string_literal(parse_tree.get_sub()[1]));
@@ -250,10 +250,10 @@ static std::optional<response_or_errort<smt_termt>> try_select_validation(
250250
return {};
251251
if(parse_tree.get_sub().size() != 3)
252252
{
253-
return response_or_errort<smt_termt>{
254-
"\"select\" is expected to have 2 arguments, but " +
255-
std::to_string(parse_tree.get_sub().size()) +
256-
" arguments were found - \"" + print_parse_tree(parse_tree) + "\"."};
253+
return response_or_errort<smt_termt>{std::vector<std::string>{
254+
{"\"select\" is expected to have 2 arguments, but " +
255+
std::to_string(parse_tree.get_sub().size()) +
256+
" arguments were found - \"" + print_parse_tree(parse_tree) + "\"."}}};
257257
}
258258
const auto array = validate_term(parse_tree.get_sub()[1], identifier_table);
259259
const auto index = validate_term(parse_tree.get_sub()[2], identifier_table);
@@ -281,8 +281,8 @@ static response_or_errort<smt_termt> validate_term(
281281
{
282282
return *select_validation;
283283
}
284-
return response_or_errort<smt_termt>{"Unrecognised SMT term - \"" +
285-
print_parse_tree(parse_tree) + "\"."};
284+
return response_or_errort<smt_termt>{std::vector<std::string>{
285+
{"Unrecognised SMT term - \"" + print_parse_tree(parse_tree) + "\"."}}};
286286
}
287287

288288
static response_or_errort<smt_get_value_responset::valuation_pairt>
@@ -305,10 +305,10 @@ validate_valuation_pair(
305305
if(valid_descriptor.get_sort() != valid_value.get_sort())
306306
{
307307
return resultt{
308-
"Mismatched descriptor and value sorts in - " +
309-
print_parse_tree(pair_parse_tree) + "\nDescriptor has sort " +
310-
smt_to_smt2_string(valid_descriptor.get_sort()) + "\nValue has sort " +
311-
smt_to_smt2_string(valid_value.get_sort())};
308+
{"Mismatched descriptor and value sorts in - " +
309+
print_parse_tree(pair_parse_tree) + "\nDescriptor has sort " +
310+
smt_to_smt2_string(valid_descriptor.get_sort()) + "\nValue has sort " +
311+
smt_to_smt2_string(valid_value.get_sort())}};
312312
}
313313
// see https://github.com/diffblue/cbmc/issues/7464 for why we explicitly name
314314
// the valuation_pairt type here:
@@ -378,6 +378,6 @@ response_or_errort<smt_responset> validate_smt_response(
378378
{
379379
return *get_value_response;
380380
}
381-
return response_or_errort<smt_responset>{"Invalid SMT response \"" +
382-
id2string(parse_tree.id()) + "\""};
381+
return response_or_errort<smt_responset>{std::vector<std::string>{
382+
{"Invalid SMT response \"" + id2string(parse_tree.id()) + "\""}}};
383383
}

Diff for: ‎src/solvers/strings/string_constraint_instantiation.cpp

+4-2
Original file line numberDiff line numberDiff line change
@@ -10,15 +10,17 @@ Author: Jesse Sigal, [email protected]
1010
/// Defines related function for string constraints.
1111

1212
#include "string_constraint_instantiation.h"
13-
#include <algorithm>
14-
#include <unordered_set>
1513

1614
#include <util/arith_tools.h>
1715
#include <util/expr_iterator.h>
1816
#include <util/format_expr.h>
1917

2018
#include "string_constraint.h"
2119

20+
#include <algorithm>
21+
#include <list>
22+
#include <unordered_set>
23+
2224
/// Look for symbol \p qvar in the expression \p index and return true if found
2325
/// \return True, iff \p qvar appears in \p index.
2426
static bool contains(const exprt &index, const symbol_exprt &qvar)

Diff for: ‎src/statement-list/statement_list_parse_tree.h

+2
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,8 @@ Author: Matthias Weiss, [email protected]
1515
#include <util/std_code_base.h>
1616
#include <util/std_expr.h>
1717

18+
#include <list>
19+
1820
/// Intermediate representation of a parsed Statement List file before
1921
/// converting it into a goto program. Contains all data structures that are
2022
/// necessary for describing Statement List functions and function blocks.

Diff for: ‎src/util/irep_ids.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ enum class idt:unsigned
4545
#else
4646

4747
#define IREP_ID_ONE(the_id) const std::string ID_##the_id(#the_id);
48-
#define IREP_ID_TWO(the_id, str) const std::string ID_##the_id(#the_id);
48+
# define IREP_ID_TWO(the_id, str) const std::string ID_##the_id(# str);
4949

5050
#endif
5151

Diff for: ‎src/util/irep_serialization.cpp

+8-3
Original file line numberDiff line numberDiff line change
@@ -13,11 +13,12 @@ Date: May 2007
1313

1414
#include "irep_serialization.h"
1515

16+
#include "exception_utils.h"
17+
#include "string_container.h"
18+
1619
#include <climits>
1720
#include <iostream>
1821

19-
#include "exception_utils.h"
20-
2122
void irep_serializationt::write_irep(
2223
std::ostream &out,
2324
const irept &irep)
@@ -211,7 +212,11 @@ void irep_serializationt::write_string_ref(
211212
std::ostream &out,
212213
const irep_idt &s)
213214
{
214-
size_t id=irep_id_hash()(s);
215+
#ifdef USE_DSTRING
216+
size_t id = s.get_no();
217+
#else
218+
size_t id = get_string_container()[s];
219+
#endif
215220
if(id>=ireps_container.string_map.size())
216221
ireps_container.string_map.resize(id+1, false);
217222

Diff for: ‎src/util/json.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -274,7 +274,7 @@ class json_stringt:public jsont
274274
{
275275
}
276276

277-
#ifndef USE_STD_STRING
277+
#ifdef USE_DSTRING
278278
explicit json_stringt(const irep_idt &_value)
279279
: jsont(kindt::J_STRING, id2string(_value))
280280
{

Diff for: ‎src/util/symbol_table_base.h

+1
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@
88

99
#include "symbol.h" // IWYU pragma: keep
1010

11+
#include <list>
1112
#include <map>
1213
#include <unordered_map>
1314

Diff for: ‎unit/analyses/variable-sensitivity/abstract_environment/to_predicate.cpp

+3-3
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ SCENARIO(
5252

5353
auto type = signedbv_typet(32);
5454
auto val2 = make_constant(from_integer(2, type), env, ns);
55-
auto x_name = symbol_exprt(dstringt("x"), type);
55+
auto x_name = symbol_exprt("x", type);
5656

5757
env.assign(x_name, val2, ns);
5858

@@ -65,10 +65,10 @@ SCENARIO(
6565

6666
auto type = signedbv_typet(32);
6767
auto val2 = make_constant(from_integer(2, type), env, ns);
68-
auto x_name = symbol_exprt(dstringt("x"), type);
68+
auto x_name = symbol_exprt("x", type);
6969

7070
auto val3 = make_constant(from_integer(3, type), env, ns);
71-
auto y_name = symbol_exprt(dstringt("y"), type);
71+
auto y_name = symbol_exprt("y", type);
7272

7373
env.assign(x_name, val2, ns);
7474
env.assign(y_name, val3, ns);

Diff for: ‎unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ SCENARIO(
2525
const typet type = signedbv_typet(32);
2626
const exprt val2 = from_integer(2, type);
2727

28-
const exprt x_name = symbol_exprt(dstringt("x"), type);
28+
const exprt x_name = symbol_exprt("x", type);
2929

3030
auto config = vsd_configt::constant_domain();
3131
config.context_tracking.data_dependency_context = false;

Diff for: ‎unit/analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -24,9 +24,9 @@ SCENARIO(
2424
{
2525
const auto int_type = signedbv_typet(32);
2626
const auto ptr_type = pointer_typet(int_type, 32);
27-
const auto val2_symbol = symbol_exprt(dstringt("val2"), int_type);
27+
const auto val2_symbol = symbol_exprt("val2", int_type);
2828

29-
const auto x_name = symbol_exprt(dstringt("x"), int_type);
29+
const auto x_name = symbol_exprt("x", int_type);
3030

3131
auto config = vsd_configt::constant_domain();
3232
config.context_tracking.data_dependency_context = false;

0 commit comments

Comments
 (0)