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();
96 "The last instruction in a goto-program must be END_FUNCTION");
101 for(dead_mapt::const_iterator it=dead_map.begin();
109 it->second->source_location.as_string());
127 "The last instruction in a goto-program must be END_FUNCTION");
129 entry[
"function"] =
json_stringt(end_function->function);
132 id2string(end_function->source_location.get_working_directory()),
133 id2string(end_function->source_location.get_file())));
137 for(dead_mapt::const_iterator it=dead_map.begin();
141 std::ostringstream oss;
143 std::string s=oss.str();
146 assert(n!=std::string::npos);
148 n=s.find_first_not_of(
' ');
149 assert(n!=std::string::npos);
157 i_entry[
"sourceLocation"]=
json(l);
175 if(!f_it->second.body_available())
185 if(called.find(decl.
base_name)!=called.end() ||
186 f_it->second.is_inlined())
191 if(!dead_map.empty())
201 os << json_result <<
'\n';
211 xmlt xml_result(
"unreachable-instructions");
217 if(!f_it->second.body_available())
224 if(!dead_map.empty())
228 add_to_json(ns, f_it->second.body, dead_map, json_result);
232 add_to_xml(f_it->second.body, dead_map, xml_result);
237 "Other output formats handled");
244 out << json_result <<
'\n';
246 out << xml_result <<
'\n';
291 const std::unordered_set<irep_idt> &called,
297 xmlt xml_result(unreachable ?
298 "unreachable-functions" :
299 "reachable-functions");
310 (called.find(decl.
base_name)!=called.end() ||
311 f_it->second.is_inlined()))
317 if(f_it->second.body_available())
330 last_location = end_function->source_location;
352 << last_location.
get_line() <<
"\n";
371 os << json_result <<
'\n';
373 os << xml_result <<
'\n';
412 std::unordered_set<irep_idt> called;
416 if(!f_it->second.body_available())
422 called.insert(f_it->first);
434 std::unordered_set<irep_idt> called =
448 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)
bool static_unreachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
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
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 std::unique_ptr< statet > abstract_state_before(locationt l) const =0
Accessing individual domains at particular locations (without needing to know what kind of domain or ...
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
bool static_reachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
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)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
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
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const
Output a single instruction.
The basic interface of an abstract interpreter.
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)
static void add_to_xml(const goto_programt &goto_program, const dead_mapt &dead_map, xmlt &dest)
goto_programt & goto_program
json_objectt & make_object()
std::map< unsigned, goto_programt::const_targett > dead_mapt
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)
bool static_unreachable_instructions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
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().