26 typedef std::map<unsigned, goto_programt::const_targett>
dead_mapt;
35 for(cfg_dominatorst::cfgt::entry_mapt::const_iterator
41 if(n.dominators.empty())
42 dest.insert(std::make_pair(it->first->location_number,
52 if(!it->is_end_function())
53 dest.insert(std::make_pair(it->location_number, it));
63 dest.insert(std::make_pair(it->location_number, it));
76 assert(end_function->is_end_function());
78 os <<
"\n*** " << end_function->function <<
" ***\n";
80 for(dead_mapt::const_iterator it=dead_map.begin();
97 "The last instruction in a goto-program must be END_FUNCTION");
102 for(dead_mapt::const_iterator it=dead_map.begin();
110 it->second->source_location.as_string());
128 "The last instruction in a goto-program must be END_FUNCTION");
130 entry[
"function"] =
json_stringt(end_function->function);
133 id2string(end_function->source_location.get_working_directory()),
134 id2string(end_function->source_location.get_file())));
138 for(dead_mapt::const_iterator it=dead_map.begin();
142 std::ostringstream oss;
144 std::string s=oss.str();
147 assert(n!=std::string::npos);
149 n=s.find_first_not_of(
' ');
150 assert(n!=std::string::npos);
158 i_entry[
"sourceLocation"]=
json(l);
176 if(!f_it->second.body_available())
186 if(called.find(decl.
base_name)!=called.end() ||
187 f_it->second.is_inlined())
192 if(!dead_map.empty())
202 os << json_result <<
'\n';
213 xmlt xml_result(
"unreachable-instructions");
219 if(!f_it->second.body_available())
226 if(!dead_map.empty())
230 add_to_json(ns, f_it->second.body, dead_map, json_result);
234 add_to_xml(ns, f_it->second.body, dead_map, xml_result);
239 "Other output formats handled");
246 out << json_result <<
'\n';
248 out << xml_result <<
'\n';
293 const std::unordered_set<irep_idt> &called,
299 xmlt xml_result(unreachable ?
300 "unreachable-functions" :
301 "reachable-functions");
312 (called.find(decl.
base_name)!=called.end() ||
313 f_it->second.is_inlined()))
319 if(f_it->second.body_available())
332 last_location = end_function->source_location;
354 << last_location.
get_line() <<
"\n";
373 os << json_result <<
'\n';
375 os << xml_result <<
'\n';
414 std::unordered_set<irep_idt> called;
418 if(!f_it->second.body_available())
424 called.insert(f_it->first);
437 std::unordered_set<irep_idt> called =
452 std::unordered_set<irep_idt> called =
std::string concat_dir_file(const std::string &directory, const std::string &file_name)
const irep_idt & get_working_directory() const
static void build_dead_map_from_ai(const goto_programt &goto_program, const ai_baset &ai, dead_mapt &dest)
const std::string & id2string(const irep_idt &d)
std::unordered_set< irep_idt > compute_called_functions_from_ai(const goto_modelt &goto_model, const ai_baset &ai)
static void xml_output_function(const irep_idt &function, const source_locationt &first_location, const source_locationt &last_location, xmlt &dest)
static void json_output_function(const irep_idt &function, const source_locationt &first_location, const source_locationt &last_location, json_arrayt &dest)
std::unordered_set< irep_idt > compute_called_functions(const goto_functionst &goto_functions)
computes the functions that are (potentially) called
bool static_reachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out)
bool static_unreachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out)
unsignedbv_typet size_type()
symbol_tablet symbol_table
Symbol table.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
virtual bool is_bottom() const =0
static void add_to_json(const namespacet &ns, const goto_programt &goto_program, const dead_mapt &dead_map, json_arrayt &dest)
json_arrayt & make_array()
#define INVARIANT(CONDITION, REASON)
static void output_dead_plain(const namespacet &ns, const goto_programt &goto_program, const dead_mapt &dead_map, std::ostream &os)
static void list_functions(const goto_modelt &goto_model, const std::unordered_set< irep_idt > &called, const optionst &options, std::ostream &os, bool unreachable)
jsont & push_back(const jsont &json)
const irep_idt & get_line() const
cfg_base_nodet< nodet, goto_programt::const_targett > nodet
instructionst instructions
The list of instructions in the goto program.
bool get_bool_option(const std::string &option) const
void set_attribute(const std::string &attribute, unsigned value)
instructionst::const_iterator const_targett
#define PRECONDITION(CONDITION)
xmlt & new_element(const std::string &name)
A generic container class for the GOTO intermediate representation of one function.
List all unreachable instructions.
source_locationt location
Source code location of definition of symbol.
const irep_idt & get_file() const
bool static_unreachable_instructions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out)
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const
Output a single instruction.
irep_idt base_name
Base (non-scoped) name.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
static void unreachable_instructions(const goto_programt &goto_program, dead_mapt &dest)
void unreachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
static void all_unreachable(const goto_programt &goto_program, dead_mapt &dest)
goto_programt & goto_program
virtual const ai_domain_baset & abstract_state_before(goto_programt::const_targett t) const =0
Returns the abstract state before the given instruction.
json_objectt & make_object()
std::map< unsigned, goto_programt::const_targett > dead_mapt
goto_programt coverage_criteriont message_handlert & message_handler
void set_option(const std::string &option, const bool value)
#define DATA_INVARIANT(CONDITION, REASON)
Compute dominators for CFG of goto_function.
#define forall_goto_functions(it, functions)
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
#define forall_goto_program_instructions(it, program)
const irept & find(const irep_namet &name) const
goto_functionst goto_functions
GOTO functions.
json_objectt json(const source_locationt &location)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
static void add_to_xml(const namespacet &ns, const goto_programt &goto_program, const dead_mapt &dead_map, xmlt &dest)