Skip to content

Commit d25dcfa

Browse files
author
Daniel Kroening
committed
Merge branch 'tautschnig-c++11-cleanup'
2 parents 467664d + 2db625a commit d25dcfa

File tree

283 files changed

+536
-2352
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

283 files changed

+536
-2352
lines changed

‎src/aa-path-symex/locs.h

-8
Original file line numberDiff line numberDiff line change
@@ -104,12 +104,4 @@ class target_to_loc_mapt
104104
mapt map;
105105
};
106106

107-
#define forall_locs(it, locs) \
108-
for(locst::loc_vectort::const_iterator it=(locs).loc_vector.begin(); \
109-
it!=(locs).loc_vector.end(); it++)
110-
111-
#define Forall_locs(it, locs) \
112-
for(exprt::operandst::iterator it=(expr).loc_vector.begin(); \
113-
it!=(locs).loc_vector.end(); it++)
114-
115107
#endif // CPROVER_AA_PATH_SYMEX_LOCS_H

‎src/aa-path-symex/path_symex.cpp

+2-3
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@ Author: Daniel Kroening, [email protected]
1010
#include <util/arith_tools.h>
1111
#include <util/simplify_expr.h>
1212
#include <util/byte_operators.h>
13-
#include <util/i2string.h>
1413
#include <util/pointer_offset_size.h>
1514
#include <util/expr_util.h>
1615
#include <util/base_type.h>
@@ -319,7 +318,7 @@ void path_symext::symex_malloc(
319318

320319
symbolt size_symbol;
321320

322-
size_symbol.base_name="dynamic_object_size"+i2string(dynamic_count);
321+
size_symbol.base_name="dynamic_object_size"+std::to_string(dynamic_count);
323322
size_symbol.name="symex::"+id2string(size_symbol.base_name);
324323
size_symbol.is_lvalue=true;
325324
size_symbol.type=tmp_size.type();
@@ -338,7 +337,7 @@ void path_symext::symex_malloc(
338337
// value
339338
symbolt value_symbol;
340339

341-
value_symbol.base_name="dynamic_object"+i2string(state.var_map.dynamic_count);
340+
value_symbol.base_name="dynamic_object"+std::to_string(state.var_map.dynamic_count);
342341
value_symbol.name="symex_dynamic::"+id2string(value_symbol.base_name);
343342
value_symbol.is_lvalue=true;
344343
value_symbol.type=object_type;

‎src/aa-path-symex/path_symex_state.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
1111
#include <util/arith_tools.h>
1212
#include <util/expr_util.h>
1313
#include <util/decision_procedure.h>
14-
#include <util/i2string.h>
1514

1615
#include <ansi-c/c_types.h>
1716

@@ -328,7 +327,7 @@ exprt path_symex_statet::instantiate_rec(
328327

329328
if(statement==ID_nondet)
330329
{
331-
irep_idt id="symex::nondet"+i2string(var_map.nondet_count);
330+
irep_idt id="symex::nondet"+std::to_string(var_map.nondet_count);
332331
var_map.nondet_count++;
333332
return symbol_exprt(id, src.type());
334333
}

‎src/aa-path-symex/var_map.cpp

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

99
#include <util/symbol.h>
1010
#include <util/std_expr.h>
11-
#include <util/i2string.h>
1211
#include <util/prefix.h>
1312

1413
#include "var_map.h"
@@ -115,5 +114,5 @@ Function: var_mapt::var_infot::ssa_identifier
115114
irep_idt var_mapt::var_infot::ssa_identifier() const
116115
{
117116
return id2string(full_identifier)+
118-
"#"+i2string(ssa_counter);
117+
"#"+std::to_string(ssa_counter);
119118
}

‎src/analyses/ai.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -275,7 +275,7 @@ class ait:public ai_baset
275275
}
276276

277277
protected:
278-
typedef hash_map_cont<locationt, domainT, const_target_hash> state_mapt;
278+
typedef std::unordered_map<locationt, domainT, const_target_hash> state_mapt;
279279
state_mapt state_map;
280280

281281
// this one creates states, if need be

‎src/analyses/dirty.h

+3-1
Original file line numberDiff line numberDiff line change
@@ -11,13 +11,15 @@ Date: March 2013
1111
#ifndef CPROVER_ANALYSES_DIRTY_H
1212
#define CPROVER_ANALYSES_DIRTY_H
1313

14+
#include <unordered_set>
15+
1416
#include <util/std_expr.h>
1517
#include <goto-programs/goto_functions.h>
1618

1719
class dirtyt
1820
{
1921
public:
20-
typedef hash_set_cont<irep_idt, irep_id_hash> id_sett;
22+
typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
2123
typedef goto_functionst::goto_functiont goto_functiont;
2224

2325
explicit dirtyt(const goto_functiont &goto_function)

‎src/analyses/flow_insensitive_analysis.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -309,7 +309,7 @@ bool flow_insensitive_analysis_baset::visit(
309309

310310
// {
311311
// static unsigned state_cntr=0;
312-
// std::string s("pastate"); s += i2string(state_cntr);
312+
// std::string s("pastate"); s += std::to_string(state_cntr);
313313
// std::ofstream f(s.c_str());
314314
// goto_program.output_instruction(ns, "", f, l);
315315
// f << std::endl;

‎src/analyses/flow_insensitive_analysis.h

+2-1
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
1313
#include <queue>
1414
#include <map>
1515
#include <iosfwd>
16+
#include <unordered_set>
1617

1718
#include <goto-programs/goto_functions.h>
1819

@@ -44,7 +45,7 @@ class flow_insensitive_abstract_domain_baset
4445
{
4546
}
4647

47-
typedef hash_set_cont<exprt, irep_hash> expr_sett;
48+
typedef std::unordered_set<exprt, irep_hash> expr_sett;
4849

4950
virtual void get_reference_set(
5051
const namespacet &ns,

‎src/analyses/goto_rw.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,7 @@ class rw_range_sett
8484
#ifdef USE_DSTRING
8585
typedef std::map<irep_idt, range_domain_baset*> objectst;
8686
#else
87-
typedef hash_map_cont<irep_idt, range_domain_baset*, string_hash> objectst;
87+
typedef std::unordered_map<irep_idt, range_domain_baset*, string_hash> objectst;
8888
#endif
8989

9090
virtual ~rw_range_sett();

‎src/analyses/interval_domain.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -11,9 +11,9 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include <util/ieee_float.h>
1313
#include <util/mp_arith.h>
14-
#include <util/interval_template.h>
1514

1615
#include "ai.h"
16+
#include "interval_template.h"
1717

1818
typedef interval_template<mp_integer> integer_intervalt;
1919
typedef interval_template<ieee_floatt> ieee_float_intervalt;

‎src/util/interval_template.h renamed to ‎src/analyses/interval_template.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,9 @@ Author: Daniel Kroening, [email protected]
1010
#define CPROVER_UTIL_INTERVAL_TEMPLATE_H
1111

1212
#include <algorithm>
13-
#include <ostream>
13+
#include <iosfwd>
1414

15-
#include "threeval.h"
15+
#include <util/threeval.h>
1616

1717
template<class T> class interval_template
1818
{

‎src/analyses/invariant_propagation.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -78,7 +78,7 @@ void invariant_propagationt::add_objects(
7878
goto_program.get_decl_identifiers(locals);
7979

8080
// cache the list for the locals to speed things up
81-
typedef hash_map_cont<irep_idt, object_listt, irep_id_hash> object_cachet;
81+
typedef std::unordered_map<irep_idt, object_listt, irep_id_hash> object_cachet;
8282
object_cachet object_cache;
8383

8484
for(goto_programt::instructionst::const_iterator
@@ -226,7 +226,7 @@ void invariant_propagationt::add_objects(
226226
const goto_programt &goto_program=f_it->second.body;
227227

228228
// cache the list for the locals to speed things up
229-
typedef hash_map_cont<irep_idt, object_listt, irep_id_hash> object_cachet;
229+
typedef std::unordered_map<irep_idt, object_listt, irep_id_hash> object_cachet;
230230
object_cachet object_cache;
231231

232232
for(goto_programt::instructionst::const_iterator

‎src/analyses/invariant_set.h

+2-1
Original file line numberDiff line numberDiff line change
@@ -14,10 +14,11 @@ Author: Daniel Kroening, [email protected]
1414
#include <util/union_find.h>
1515
#include <util/threeval.h>
1616
#include <util/mp_arith.h>
17-
#include <util/interval_template.h>
1817

1918
#include <pointer-analysis/value_sets.h>
2019

20+
#include "interval_template.h"
21+
2122
class inv_object_storet
2223
{
2324
public:

‎src/analyses/reaching_definitions.h

+3-3
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ class sparse_bitvector_analysist
4747
protected:
4848
typedef typename std::map<V, std::size_t> inner_mapt;
4949
std::vector<typename inner_mapt::const_iterator> values;
50-
hash_map_cont<irep_idt, inner_mapt, irep_id_hash> value_map;
50+
std::unordered_map<irep_idt, inner_mapt, irep_id_hash> value_map;
5151
};
5252

5353
struct reaching_definitiont
@@ -151,14 +151,14 @@ class rd_range_domaint:public ai_domain_baset
151151
#ifdef USE_DSTRING
152152
typedef std::map<irep_idt, values_innert> valuest;
153153
#else
154-
typedef hash_map_cont<irep_idt, values_innert, irep_id_hash> valuest;
154+
typedef std::unordered_map<irep_idt, values_innert, irep_id_hash> valuest;
155155
#endif
156156
valuest values;
157157

158158
#ifdef USE_DSTRING
159159
typedef std::map<irep_idt, ranges_at_loct> export_cachet;
160160
#else
161-
typedef hash_map_cont<irep_idt, ranges_at_loct, irep_id_hash>
161+
typedef std::unordered_map<irep_idt, ranges_at_loct, irep_id_hash>
162162
export_cachet;
163163
#endif
164164
mutable export_cachet export_cache;

‎src/analyses/static_analysis.h

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

1616
#include <map>
1717
#include <iosfwd>
18+
#include <unordered_set>
1819

1920
#include <goto-programs/goto_functions.h>
2021

@@ -60,7 +61,7 @@ class domain_baset
6061
{
6162
}
6263

63-
typedef hash_set_cont<exprt, irep_hash> expr_sett;
64+
typedef std::unordered_set<exprt, irep_hash> expr_sett;
6465

6566
// will go away
6667
virtual void get_reference_set(

‎src/ansi-c/Makefile

+1-1
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ SRC = c_typecast.cpp ansi_c_y.tab.cpp ansi_c_lex.yy.cpp ansi_c_parser.cpp \
1414
literals/convert_float_literal.cpp \
1515
literals/convert_character_literal.cpp \
1616
literals/convert_integer_literal.cpp \
17-
literals/convert_string_literal.cpp
17+
literals/convert_string_literal.cpp c_misc.cpp
1818

1919
INCLUDES= -I ..
2020

‎src/ansi-c/ansi_c_entry_point.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,6 @@ Author: Daniel Kroening, [email protected]
1717
#include <util/config.h>
1818
#include <util/cprover_prefix.h>
1919
#include <util/prefix.h>
20-
#include <util/i2string.h>
2120

2221
#include <ansi-c/c_types.h>
2322
#include <ansi-c/string_constant.h>
@@ -52,7 +51,7 @@ exprt::operandst build_function_environment(
5251
for(const auto & p : parameters)
5352
{
5453
irep_idt base_name=p.get_base_name().empty()?
55-
("argument#"+i2string(i)):p.get_base_name();
54+
("argument#"+to_string(i)):p.get_base_name();
5655
irep_idt identifier=id2string(goto_functionst::entry_point())+
5756
"::"+id2string(base_name);
5857

‎src/ansi-c/ansi_c_internal_additions.cpp

+2-3
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,6 @@ Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

9-
#include <util/i2string.h>
109
#include <util/config.h>
1110

1211
#include "ansi_c_internal_additions.h"
@@ -94,7 +93,7 @@ static std::string architecture_string(int value, const char *s)
9493
{
9594
return std::string("const int __CPROVER_architecture_")+
9695
std::string(s)+
97-
"="+i2string(value)+";\n";
96+
"="+std::to_string(value)+";\n";
9897
}
9998

10099
/*******************************************************************\
@@ -193,7 +192,7 @@ void ansi_c_internal_additions(std::string &code)
193192
"double __CPROVER_inf(void);\n"
194193
"float __CPROVER_inff(void);\n"
195194
"long double __CPROVER_infl(void);\n"
196-
"int __CPROVER_thread_local __CPROVER_rounding_mode="+i2string(config.ansi_c.rounding_mode)+";\n"
195+
"int __CPROVER_thread_local __CPROVER_rounding_mode="+std::to_string(config.ansi_c.rounding_mode)+";\n"
197196

198197
// absolute value
199198
"int __CPROVER_abs(int x);\n"

‎src/ansi-c/ansi_c_parser.h

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

1414
#include <util/parser.h>
1515
#include <util/expr.h>
16-
#include <util/hash_cont.h>
1716
#include <util/string_hash.h>
18-
#include <util/i2string.h>
1917
#include <util/mp_arith.h>
2018
#include <util/config.h>
2119

‎src/ansi-c/ansi_c_scope.h

+1-2
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@ Author: Daniel Kroening, [email protected]
99
#ifndef CPROVER_ANSI_C_ANSI_C_SCOPE_H
1010
#define CPROVER_ANSI_C_ANSI_C_SCOPE_H
1111

12-
#include <util/hash_cont.h>
1312
#include <util/irep.h>
1413

1514
typedef enum { ANSI_C_UNKNOWN, ANSI_C_SYMBOL, ANSI_C_TYPEDEF,
@@ -31,7 +30,7 @@ class ansi_c_scopet
3130
public:
3231
// This maps "scope names" (tag-X, label-X, X) to
3332
// ansi_c_identifiert.
34-
typedef hash_map_cont<irep_idt, ansi_c_identifiert, irep_id_hash> name_mapt;
33+
typedef std::unordered_map<irep_idt, ansi_c_identifiert, irep_id_hash> name_mapt;
3534
name_mapt name_map;
3635

3736
std::string prefix;

‎src/util/c_misc.cpp renamed to ‎src/ansi-c/c_misc.cpp

+4-2
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ Function: MetaChar
2828
2929
\*******************************************************************/
3030

31-
void MetaChar(std::string &out, char c, bool inString)
31+
static void MetaChar(std::string &out, char c, bool inString)
3232
{
3333
switch(c)
3434
{
@@ -101,6 +101,7 @@ void MetaChar(std::string &out, char c, bool inString)
101101
}
102102
}
103103

104+
#if 0
104105
/*******************************************************************\
105106

106107
Function: MetaChar
@@ -113,12 +114,13 @@ Function: MetaChar
113114

114115
\*******************************************************************/
115116

116-
std::string MetaChar(char c)
117+
static std::string MetaChar(char c)
117118
{
118119
std::string result;
119120
MetaChar(result, c, false);
120121
return result;
121122
}
123+
#endif
122124

123125
/*******************************************************************\
124126

‎src/util/c_misc.h renamed to ‎src/ansi-c/c_misc.h

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

1212
#include <string>
1313

14-
std::string MetaChar(char c);
1514
std::string MetaString(const std::string &in);
1615

1716
#endif // CPROVER_UTIL_C_MISC_H

‎src/ansi-c/c_preprocess.cpp

+5-6
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,6 @@ Author: Daniel Kroening, [email protected]
2222
#include <fstream>
2323

2424
#include <util/config.h>
25-
#include <util/i2string.h>
2625
#include <util/message.h>
2726
#include <util/tempfile.h>
2827
#include <util/unicode.h>
@@ -773,7 +772,7 @@ bool c_preprocess_gcc_clang(
773772

774773
command +=" -E -undef -D__CPROVER__";
775774

776-
command+=" -D__WORDSIZE="+i2string(config.ansi_c.pointer_width);
775+
command+=" -D__WORDSIZE="+std::to_string(config.ansi_c.pointer_width);
777776

778777
command+=" -D__DBL_MIN_EXP__=\"(-1021)\"";
779778
command+=" -D__FLT_MIN__=1.17549435e-38F";
@@ -1091,9 +1090,9 @@ bool c_preprocess_arm(
10911090

10921091
command="armcc -E -D__CPROVER__";
10931092

1094-
// command+=" -D__sizeof_int="+i2string(config.ansi_c.int_width/8);
1095-
// command+=" -D__sizeof_long="+i2string(config.ansi_c.long_int_width/8);
1096-
// command+=" -D__sizeof_ptr="+i2string(config.ansi_c.pointer_width/8);
1093+
// command+=" -D__sizeof_int="+std::to_string(config.ansi_c.int_width/8);
1094+
// command+=" -D__sizeof_long="+std::to_string(config.ansi_c.long_int_width/8);
1095+
// command+=" -D__sizeof_ptr="+std::to_string(config.ansi_c.pointer_width/8);
10971096
//command+=" -D__EDG_VERSION__=308";
10981097
//command+=" -D__EDG__";
10991098
// command+=" -D__CC_ARM=1";
@@ -1108,7 +1107,7 @@ bool c_preprocess_arm(
11081107

11091108
if(config.ansi_c.os!=configt::ansi_ct::ost::OS_WIN)
11101109
{
1111-
command+=" -D__WORDSIZE="+i2string(config.ansi_c.pointer_width);
1110+
command+=" -D__WORDSIZE="+std::to_string(config.ansi_c.pointer_width);
11121111

11131112
if(config.ansi_c.int_width==16)
11141113
command+=GCC_DEFINES_16;

0 commit comments

Comments
 (0)