Go to the documentation of this file.
26 typedef std::map<unsigned, goto_programt::const_targett>
dead_mapt;
33 dominators(goto_program);
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));
73 os <<
"\n*** " << function_identifier <<
" ***\n";
75 for(dead_mapt::const_iterator it=dead_map.begin();
90 for(dead_mapt::const_iterator it=dead_map.begin();
98 it->second->source_location.as_string());
105 const irep_idt &function_identifier,
115 "The last instruction in a goto-program must be END_FUNCTION");
121 id2string(end_function->source_location.get_working_directory()),
122 id2string(end_function->source_location.get_file())))}};
126 for(dead_mapt::const_iterator it=dead_map.begin();
130 std::ostringstream oss;
132 std::string s=oss.str();
135 assert(n!=std::string::npos);
137 n=s.find_first_not_of(
' ');
138 assert(n!=std::string::npos);
166 if(!f_it->second.body_available())
177 called.find(decl.
base_name) != called.end() ||
185 if(!dead_map.empty())
190 add_to_json(ns, f_it->first, goto_program, dead_map, json_result);
195 os << json_result <<
'\n';
205 xmlt xml_result(
"unreachable-instructions");
211 if(!f_it->second.body_available())
218 if(!dead_map.empty())
222 add_to_json(ns, f_it->first, f_it->second.body, dead_map, json_result);
226 add_to_xml(f_it->first, f_it->second.body, dead_map, xml_result);
237 out << json_result <<
'\n';
239 out << xml_result <<
'\n';
283 const std::unordered_set<irep_idt> &called,
289 xmlt xml_result(unreachable ?
290 "unreachable-functions" :
291 "reachable-functions");
302 unreachable == (called.find(decl.
base_name) != called.end() ||
311 if(f_it->second.body_available())
324 last_location = end_function->source_location;
363 << last_location.
get_line() <<
"\n";
368 os << json_result <<
'\n';
370 os << xml_result <<
'\n';
405 std::unordered_set<irep_idt> called;
409 if(!f_it->second.body_available())
415 called.insert(f_it->first);
427 std::unordered_set<irep_idt> called =
441 std::unordered_set<irep_idt> called =
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
static void add_to_json(const namespacet &ns, const irep_idt &function_identifier, const goto_programt &goto_program, const dead_mapt &dead_map, json_arrayt &dest)
bool static_unreachable_instructions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
std::map< unsigned, goto_programt::const_targett > dead_mapt
typet type
Type of symbol.
const irept & find(const irep_namet &name) const
virtual cstate_ptrt abstract_state_before(locationt l) const
Get a copy of the abstract state before the given instruction, without needing to know what kind of d...
irep_idt base_name
Base (non-scoped) name.
static void all_unreachable(const goto_programt &goto_program, dead_mapt &dest)
void set_option(const std::string &option, const bool value)
static void xml_output_function(const irep_idt &function, const source_locationt &first_location, const source_locationt &last_location, xmlt &dest)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
static void add_to_xml(const irep_idt &function_identifier, const goto_programt &goto_program, const dead_mapt &dead_map, xmlt &dest)
const irep_idt & get_line() const
Compute dominators for CFG of goto_function.
std::unordered_set< irep_idt > compute_called_functions(const goto_functionst &goto_functions)
computes the functions that are (potentially) called
static void list_functions(const goto_modelt &goto_model, const std::unordered_set< irep_idt > &called, const optionst &options, std::ostream &os, bool unreachable)
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static void build_dead_map_from_ai(const goto_programt &goto_program, const ai_baset &ai, dead_mapt &dest)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
void unreachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const std::string & id2string(const irep_idt &d)
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
std::string concat_dir_file(const std::string &directory, const std::string &file_name)
#define PRECONDITION(CONDITION)
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
List all unreachable instructions.
json_arrayt & make_array()
static void unreachable_instructions(const goto_programt &goto_program, dead_mapt &dest)
std::unordered_set< irep_idt > compute_called_functions_from_ai(const goto_modelt &goto_model, const ai_baset &ai)
instructionst instructions
The list of instructions in the goto program.
static void output_dead_plain(const namespacet &ns, const irep_idt &function_identifier, const goto_programt &goto_program, const dead_mapt &dead_map, std::ostream &os)
goto_functionst goto_functions
GOTO functions.
bool static_reachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
void set_attribute(const std::string &attribute, unsigned value)
source_locationt location
Source code location of definition of symbol.
bool get_bool_option(const std::string &option) const
This is the basic interface of the abstract interpreter with default implementations of the core func...
A generic container class for the GOTO intermediate representation of one function.
static void json_output_function(const irep_idt &function, const source_locationt &first_location, const source_locationt &last_location, json_arrayt &dest)
const irep_idt & get_file() const
#define forall_goto_functions(it, functions)
instructionst::const_iterator const_targett
bool static_unreachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
unsignedbv_typet size_type()
const irep_idt & get_working_directory() const
symbol_tablet symbol_table
Symbol table.
jsont & push_back(const jsont &json)
#define forall_goto_program_instructions(it, program)
xmlt & new_element(const std::string &key)