Skip to content
Merged
Show file tree
Hide file tree
Changes from 4 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/analyses/call_graph.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -165,7 +165,7 @@ class function_indicest
call_grapht::directed_grapht &graph;

public:
std::unordered_map<irep_idt, node_indext, irep_id_hash> function_indices;
std::unordered_map<irep_idt, node_indext> function_indices;

explicit function_indicest(call_grapht::directed_grapht &graph):
graph(graph)
Expand Down
5 changes: 2 additions & 3 deletions src/analyses/call_graph.h
Original file line number Diff line number Diff line change
Expand Up @@ -115,7 +115,7 @@ class call_grapht
friend class call_grapht;

/// Maps function names onto node indices
std::unordered_map<irep_idt, node_indext, irep_id_hash> nodes_by_name;
std::unordered_map<irep_idt, node_indext> nodes_by_name;

public:
/// Find the graph node by function name
Expand All @@ -124,8 +124,7 @@ class call_grapht
optionalt<node_indext> get_node_index(const irep_idt &function) const;

/// Type of the node name -> node index map.
typedef
std::unordered_map<irep_idt, node_indext, irep_id_hash> nodes_by_namet;
typedef std::unordered_map<irep_idt, node_indext> nodes_by_namet;

/// Get the node name -> node index map
/// \return node-by-name map
Expand Down
7 changes: 3 additions & 4 deletions src/analyses/dirty.h
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,6 @@ class dirtyt

public:
bool initialized;
typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
typedef goto_functionst::goto_functiont goto_functiont;

/// \post dirtyt objects that are created through this constructor are not
Expand Down Expand Up @@ -72,7 +71,7 @@ class dirtyt
return operator()(expr.get_identifier());
}

const id_sett &get_dirty_ids() const
const std::unordered_set<irep_idt> &get_dirty_ids() const
{
die_if_uninitialized();
return dirty;
Expand All @@ -97,7 +96,7 @@ class dirtyt
void build(const goto_functiont &goto_function);

// variables whose address is taken
id_sett dirty;
std::unordered_set<irep_idt> dirty;

void find_dirty(const exprt &expr);
void find_dirty_address_of(const exprt &expr);
Expand Down Expand Up @@ -131,7 +130,7 @@ class incremental_dirtyt

private:
dirtyt dirty;
std::unordered_set<irep_idt, irep_id_hash> dirty_processed_functions;
std::unordered_set<irep_idt> dirty_processed_functions;
};

#endif // CPROVER_ANALYSES_DIRTY_H
6 changes: 2 additions & 4 deletions src/analyses/invariant_propagation.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -40,8 +40,7 @@ void invariant_propagationt::add_objects(
goto_program.get_decl_identifiers(locals);

// cache the list for the locals to speed things up
typedef std::unordered_map<irep_idt, object_listt, irep_id_hash>
object_cachet;
typedef std::unordered_map<irep_idt, object_listt> object_cachet;
object_cachet object_cache;

forall_goto_program_instructions(i_it, goto_program)
Expand Down Expand Up @@ -133,8 +132,7 @@ void invariant_propagationt::add_objects(
const goto_programt &goto_program=f_it->second.body;

// cache the list for the locals to speed things up
typedef std::unordered_map<irep_idt, object_listt, irep_id_hash>
object_cachet;
typedef std::unordered_map<irep_idt, object_listt> object_cachet;
object_cachet object_cache;

forall_goto_program_instructions(i_it, goto_program)
Expand Down
7 changes: 3 additions & 4 deletions src/analyses/reaching_definitions.h
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ class sparse_bitvector_analysist
protected:
typedef typename std::map<V, std::size_t> inner_mapt;
std::vector<typename inner_mapt::const_iterator> values;
std::unordered_map<irep_idt, inner_mapt, irep_id_hash> value_map;
std::unordered_map<irep_idt, inner_mapt> value_map;
};

struct reaching_definitiont
Expand Down Expand Up @@ -191,15 +191,14 @@ class rd_range_domaint:public ai_domain_baset
#ifdef USE_DSTRING
typedef std::map<irep_idt, values_innert> valuest;
#else
typedef std::unordered_map<irep_idt, values_innert, irep_id_hash> valuest;
typedef std::unordered_map<irep_idt, values_innert> valuest;
#endif
valuest values;

#ifdef USE_DSTRING
typedef std::map<irep_idt, ranges_at_loct> export_cachet;
#else
typedef std::unordered_map<irep_idt, ranges_at_loct, irep_id_hash>
export_cachet;
typedef std::unordered_map<irep_idt, ranges_at_loct> export_cachet;
#endif
mutable export_cachet export_cache;

Expand Down
3 changes: 1 addition & 2 deletions src/ansi-c/ansi_c_scope.h
Original file line number Diff line number Diff line change
Expand Up @@ -41,8 +41,7 @@ class ansi_c_scopet
public:
// This maps "scope names" (tag-X, label-X, X) to
// ansi_c_identifiert.
typedef std::unordered_map<irep_idt, ansi_c_identifiert, irep_id_hash>
name_mapt;
typedef std::unordered_map<irep_idt, ansi_c_identifiert> name_mapt;
name_mapt name_map;

std::string prefix;
Expand Down
4 changes: 2 additions & 2 deletions src/ansi-c/c_typecheck_base.h
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,7 @@ class c_typecheck_baset:
const irep_idt mode;
symbolt current_symbol;

typedef std::unordered_map<irep_idt, typet, irep_id_hash> id_type_mapt;
typedef std::unordered_map<irep_idt, typet> id_type_mapt;
id_type_mapt parameter_map;

// overload to use language specific syntax
Expand Down Expand Up @@ -270,7 +270,7 @@ class c_typecheck_baset:
src.id()==ID_real;
}

typedef std::unordered_map<irep_idt, irep_idt, irep_id_hash> asm_label_mapt;
typedef std::unordered_map<irep_idt, irep_idt> asm_label_mapt;
asm_label_mapt asm_label_map;

void apply_asm_label(const irep_idt &asm_label, symbolt &symbol);
Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/c_typecheck_type.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -877,7 +877,7 @@ void c_typecheck_baset::typecheck_compound_body(
// scan for duplicate members

{
std::unordered_set<irep_idt, irep_id_hash> members;
std::unordered_set<irep_idt> members;

for(struct_union_typet::componentst::iterator
it=components.begin();
Expand Down
4 changes: 2 additions & 2 deletions src/ansi-c/expr2c.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1688,8 +1688,8 @@ std::string expr2ct::convert_symbol(
dest=src.op0().get_string(ID_identifier);
else
{
std::unordered_map<irep_idt, irep_idt, irep_id_hash>::const_iterator
entry=shorthands.find(id);
std::unordered_map<irep_idt, irep_idt>::const_iterator entry =
shorthands.find(id);
// we might be called from conversion of a type
if(entry==shorthands.end())
{
Expand Down
6 changes: 2 additions & 4 deletions src/ansi-c/expr2c_class.h
Original file line number Diff line number Diff line change
Expand Up @@ -64,10 +64,8 @@ class expr2ct

static std::string indent_str(unsigned indent);

std::unordered_map<irep_idt,
std::unordered_set<irep_idt, irep_id_hash>,
irep_id_hash> ns_collision;
std::unordered_map<irep_idt, irep_idt, irep_id_hash> shorthands;
std::unordered_map<irep_idt, std::unordered_set<irep_idt>> ns_collision;
std::unordered_map<irep_idt, irep_idt> shorthands;

unsigned sizeof_nesting;

Expand Down
3 changes: 1 addition & 2 deletions src/ansi-c/type2name.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,7 @@ Author: Daniel Kroening, [email protected]
#include <util/pointer_offset_size.h>
#include <util/invariant.h>

typedef std::unordered_map<irep_idt, std::pair<size_t, bool>, irep_id_hash>
symbol_numbert;
typedef std::unordered_map<irep_idt, std::pair<size_t, bool>> symbol_numbert;

static std::string type2name(
const typet &type,
Expand Down
4 changes: 2 additions & 2 deletions src/cbmc/symex_bmc.h
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ class symex_bmct: public goto_symext
unsigned max_unwind;
bool max_unwind_is_set;

typedef std::unordered_map<irep_idt, unsigned, irep_id_hash> loop_limitst;
typedef std::unordered_map<irep_idt, unsigned> loop_limitst;
loop_limitst loop_limits;

typedef std::map<unsigned, loop_limitst> thread_loop_limitst;
Expand Down Expand Up @@ -147,7 +147,7 @@ class symex_bmct: public goto_symext

virtual void no_body(const irep_idt &identifier);

std::unordered_set<irep_idt, irep_id_hash> body_warnings;
std::unordered_set<irep_idt> body_warnings;

symex_coveraget symex_coverage;
};
Expand Down
2 changes: 1 addition & 1 deletion src/cpp/cpp_scopes.h
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ class cpp_scopest
}

// mapping from function/class/scope names to their cpp_idt
typedef std::unordered_map<irep_idt, cpp_idt *, irep_id_hash> id_mapt;
typedef std::unordered_map<irep_idt, cpp_idt *> id_mapt;
id_mapt id_map;

cpp_scopet *current_scope_ptr;
Expand Down
7 changes: 3 additions & 4 deletions src/goto-diff/goto_diff.h
Original file line number Diff line number Diff line change
Expand Up @@ -51,20 +51,19 @@ class goto_difft:public messaget
ui_message_handlert::uit ui;

unsigned total_functions_count;
typedef std::set<irep_idt> irep_id_sett;
irep_id_sett new_functions, modified_functions, deleted_functions;
std::set<irep_idt> new_functions, modified_functions, deleted_functions;

void output_function_group(
const std::string &group_name,
const irep_id_sett &function_group,
const std::set<irep_idt> &function_group,
const goto_modelt &goto_model) const;
void output_function(
const irep_idt &function_name,
const goto_modelt &goto_model) const;

void convert_function_group_json(
json_arrayt &result,
const irep_id_sett &function_group,
const std::set<irep_idt> &function_group,
const goto_modelt &goto_model) const;
void convert_function_json(
json_objectt &result,
Expand Down
4 changes: 2 additions & 2 deletions src/goto-diff/goto_diff_base.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ void goto_difft::output_functions() const
/// \param goto_model: the goto model
void goto_difft::output_function_group(
const std::string &group_name,
const irep_id_sett &function_group,
const std::set<irep_idt> &function_group,
const goto_modelt &goto_model) const
{
result() << group_name << ":\n";
Expand Down Expand Up @@ -113,7 +113,7 @@ void goto_difft::output_function(
/// \param goto_model: the goto model
void goto_difft::convert_function_group_json(
json_arrayt &result,
const irep_id_sett &function_group,
const std::set<irep_idt> &function_group,
const goto_modelt &goto_model) const
{
for(const auto &function_name : function_group)
Expand Down
9 changes: 3 additions & 6 deletions src/goto-instrument/code_contracts.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -45,8 +45,7 @@ class code_contractst

unsigned temporary_counter;

typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
id_sett summarized;
std::unordered_set<irep_idt> summarized;

void code_contracts(goto_functionst::goto_functiont &goto_function);

Expand Down Expand Up @@ -389,10 +388,8 @@ void code_contractst::operator()()
goto_functions.function_map.find(CPROVER_PREFIX "initialize");
assert(i_it!=goto_functions.function_map.end());

for(id_sett::const_iterator it=summarized.begin();
it!=summarized.end();
++it)
add_contract_check(*it, i_it->second.body);
for(const auto &contract : summarized)
add_contract_check(contract, i_it->second.body);

// remove skips
remove_skip(i_it->second.body);
Expand Down
6 changes: 3 additions & 3 deletions src/goto-instrument/count_eloc.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -21,9 +21,9 @@ Date: December 2012

#include <goto-programs/cfg.h>

typedef std::unordered_set<irep_idt, irep_id_hash> linest;
typedef std::unordered_map<irep_idt, linest, irep_id_hash> filest;
typedef std::unordered_map<irep_idt, filest, irep_id_hash> working_dirst;
typedef std::unordered_set<irep_idt> linest;
typedef std::unordered_map<irep_idt, linest> filest;
typedef std::unordered_map<irep_idt, filest> working_dirst;

static void collect_eloc(
const goto_modelt &goto_model,
Expand Down
2 changes: 1 addition & 1 deletion src/goto-instrument/cover_basic_blocks.h
Original file line number Diff line number Diff line change
Expand Up @@ -125,7 +125,7 @@ class cover_basic_blocks_javat final : public cover_blocks_baset
// map block number to its location
std::vector<source_locationt> block_locations;
// map java indexes to block indexes
std::unordered_map<irep_idt, std::size_t, irep_id_hash> index_to_block;
std::unordered_map<irep_idt, std::size_t> index_to_block;

public:
explicit cover_basic_blocks_javat(const goto_programt &_goto_program);
Expand Down
26 changes: 13 additions & 13 deletions src/goto-instrument/dump_c.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@ void dump_ct::operator()(std::ostream &os)
copied_symbol_table.add(symbol_pair.second);
}

typedef std::unordered_map<irep_idt, unsigned, irep_id_hash> unique_tagst;
typedef std::unordered_map<irep_idt, unsigned> unique_tagst;
unique_tagst unique_tags;

// add tags to anonymous union/struct/enum,
Expand Down Expand Up @@ -613,7 +613,7 @@ void dump_ct::cleanup_decl(

tmp.add_instruction(END_FUNCTION);

std::unordered_set<irep_idt, irep_id_hash> typedef_names;
std::unordered_set<irep_idt> typedef_names;
for(const auto &td : typedef_map)
typedef_names.insert(td.first);

Expand All @@ -640,7 +640,7 @@ void dump_ct::cleanup_decl(
/// function declarations or struct definitions
void dump_ct::collect_typedefs(const typet &type, bool early)
{
std::unordered_set<irep_idt, irep_id_hash> deps;
std::unordered_set<irep_idt> deps;
collect_typedefs_rec(type, early, deps);
}

Expand All @@ -654,12 +654,12 @@ void dump_ct::collect_typedefs(const typet &type, bool early)
void dump_ct::collect_typedefs_rec(
const typet &type,
bool early,
std::unordered_set<irep_idt, irep_id_hash> &dependencies)
std::unordered_set<irep_idt> &dependencies)
{
if(system_symbols.is_type_internal(type, system_headers))
return;

std::unordered_set<irep_idt, irep_id_hash> local_deps;
std::unordered_set<irep_idt> local_deps;

if(type.id()==ID_code)
{
Expand Down Expand Up @@ -769,10 +769,9 @@ void dump_ct::dump_typedefs(std::ostream &os) const
// output
std::map<std::string, typedef_infot> to_insert;

typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
id_sett typedefs_done;
std::unordered_map<irep_idt, id_sett, irep_id_hash>
forward_deps, reverse_deps;
std::unordered_set<irep_idt> typedefs_done;
std::unordered_map<irep_idt, std::unordered_set<irep_idt>> forward_deps,
reverse_deps;

for(const auto &td : typedef_map)
if(!td.second.type_decl_str.empty())
Expand Down Expand Up @@ -805,8 +804,9 @@ void dump_ct::dump_typedefs(std::ostream &os) const
continue;

// reduce remaining dependencies
id_sett &r_deps=r_it->second;
for(id_sett::iterator it=r_deps.begin(); it!=r_deps.end(); ) // no ++it
std::unordered_set<irep_idt> &r_deps = r_it->second;
for(std::unordered_set<irep_idt>::iterator it = r_deps.begin();
it != r_deps.end();) // no ++it
{
auto f_it=forward_deps.find(*it);
if(f_it==forward_deps.end()) // might be done already
Expand All @@ -816,7 +816,7 @@ void dump_ct::dump_typedefs(std::ostream &os) const
}

// update dependencies
id_sett &f_deps=f_it->second;
std::unordered_set<irep_idt> &f_deps = f_it->second;
PRECONDITION(!f_deps.empty());
PRECONDITION(f_deps.find(t.typedef_name)!=f_deps.end());
f_deps.erase(t.typedef_name);
Expand Down Expand Up @@ -986,7 +986,7 @@ void dump_ct::convert_function_declaration(
code_blockt b;
std::list<irep_idt> type_decls, local_static;

std::unordered_set<irep_idt, irep_id_hash> typedef_names;
std::unordered_set<irep_idt> typedef_names;
for(const auto &td : typedef_map)
typedef_names.insert(td.first);

Expand Down
Loading