Skip to content

Commit 2db625a

Browse files
author
Daniel Kroening
committed
merge of PR #347 
1 parent 467664d commit 2db625a

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

Lines changed: 0 additions & 8 deletions
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

Lines changed: 2 additions & 3 deletions
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

Lines changed: 1 addition & 2 deletions
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

Lines changed: 1 addition & 2 deletions
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

Lines changed: 1 addition & 1 deletion
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

Lines changed: 3 additions & 1 deletion
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

Lines changed: 1 addition & 1 deletion
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

Lines changed: 2 additions & 1 deletion
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

Lines changed: 1 addition & 1 deletion
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

Lines changed: 1 addition & 1 deletion
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;

0 commit comments

Comments
 (0)