diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 9fa1a7f7ac8..6bfce9e92e5 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1675,7 +1675,7 @@ void goto_checkt::goto_check( if(enable_pointer_check) local_bitvector_analysis = - util_make_unique(goto_function); + util_make_unique(goto_function, ns); goto_programt &goto_program=goto_function.body; diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp index f307ba0f834..84117cbe903 100644 --- a/src/analyses/local_bitvector_analysis.cpp +++ b/src/analyses/local_bitvector_analysis.cpp @@ -60,13 +60,9 @@ bool local_bitvector_analysist::merge(points_tot &a, points_tot &b) /// \return return 'true' iff we track the object with given identifier bool local_bitvector_analysist::is_tracked(const irep_idt &identifier) { - localst::locals_mapt::const_iterator it=locals.locals_map.find(identifier); - if(it==locals.locals_map.end() || - it->second.type().id()!=ID_pointer || - dirty(identifier)) - return false; - - return true; + localst::locals_sett::const_iterator it = locals.locals.find(identifier); + return it != locals.locals.end() && ns.lookup(*it).type.id() == ID_pointer && + !dirty(identifier); } void local_bitvector_analysist::assign_lhs( @@ -254,9 +250,11 @@ void local_bitvector_analysist::build() // Gather the objects we track, and // feed in sufficiently bad defaults for their value // in the entry location. - for(const auto &local : locals.locals_map) - if(is_tracked(local.first)) - loc_infos[0][pointers.number(local.first)]=flagst::mk_unknown(); + for(const auto &local : locals.locals) + { + if(is_tracked(local)) + loc_infos[0][pointers.number(local)] = flagst::mk_unknown(); + } while(!work_queue.empty()) { diff --git a/src/analyses/local_bitvector_analysis.h b/src/analyses/local_bitvector_analysis.h index 57695b14679..e675ef5d876 100644 --- a/src/analyses/local_bitvector_analysis.h +++ b/src/analyses/local_bitvector_analysis.h @@ -25,11 +25,13 @@ class local_bitvector_analysist public: typedef goto_functionst::goto_functiont goto_functiont; - explicit local_bitvector_analysist( - const goto_functiont &_goto_function): - dirty(_goto_function), - locals(_goto_function), - cfg(_goto_function.body) + local_bitvector_analysist( + const goto_functiont &_goto_function, + const namespacet &ns) + : dirty(_goto_function), + locals(_goto_function), + cfg(_goto_function.body), + ns(ns) { build(); } @@ -176,6 +178,7 @@ class local_bitvector_analysist const exprt &src); protected: + const namespacet &ns; void build(); typedef std::stack work_queuet; diff --git a/src/analyses/locals.cpp b/src/analyses/locals.cpp index 51761280280..f15419f91b4 100644 --- a/src/analyses/locals.cpp +++ b/src/analyses/locals.cpp @@ -18,20 +18,18 @@ Date: March 2013 void localst::build(const goto_functiont &goto_function) { forall_goto_program_instructions(it, goto_function.body) + { if(it->is_decl()) - { - const code_declt &code_decl=to_code_decl(it->code); - locals_map.emplace(code_decl.get_identifier(), code_decl.symbol()); - } - - for(const auto ¶m : goto_function.type.parameters()) - locals_map.emplace( - param.get_identifier(), - symbol_exprt(param.get_identifier(), param.type())); + locals.insert(it->get_decl().get_identifier()); + } + + locals.insert( + goto_function.parameter_identifiers.begin(), + goto_function.parameter_identifiers.end()); } void localst::output(std::ostream &out) const { - for(const auto &local : locals_map) - out << local.first << "\n"; + for(const auto &local : locals) + out << local << "\n"; } diff --git a/src/analyses/locals.h b/src/analyses/locals.h index 281f0aa811d..144e74ddecd 100644 --- a/src/analyses/locals.h +++ b/src/analyses/locals.h @@ -31,11 +31,11 @@ class localst // but including the function parameters. bool is_local(const irep_idt &identifier) const { - return locals_map.find(identifier)!=locals_map.end(); + return locals.find(identifier) != locals.end(); } - typedef std::map locals_mapt; - locals_mapt locals_map; + typedef std::unordered_set locals_sett; + locals_sett locals; protected: void build(const goto_functiont &goto_function); diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 632dd4356c7..4b5ceffe300 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -299,7 +299,7 @@ int goto_instrument_parse_optionst::doit() forall_goto_functions(it, goto_model.goto_functions) { - local_bitvector_analysist local_bitvector_analysis(it->second); + local_bitvector_analysist local_bitvector_analysis(it->second, ns); std::cout << ">>>>\n"; std::cout << ">>>> " << it->first << '\n'; std::cout << ">>>>\n";