27 typedef std::map<unsigned, goto_programt::const_targett>
dead_mapt;
34 dominators(goto_program);
36 for(cfg_dominatorst::cfgt::entry_mapt::const_iterator
43 dest.insert(std::make_pair(it->first->location_number,
53 if(!it->is_end_function())
54 dest.insert(std::make_pair(it->location_number, it));
64 dest.insert(std::make_pair(it->location_number, it));
74 os <<
"\n*** " << function_identifier <<
" ***\n";
76 for(dead_mapt::const_iterator it=dead_map.begin();
79 it->second->output(os);
91 for(dead_mapt::const_iterator it=dead_map.begin();
99 "source_location", it->second->source_location().as_string());
104 static std::optional<std::string>
110 return std::filesystem::path(
118 const irep_idt &function_identifier,
128 "The last instruction in a goto-program must be END_FUNCTION");
136 for(dead_mapt::const_iterator it=dead_map.begin();
140 std::ostringstream oss;
142 std::string s=oss.str();
147 n=s.find_first_not_of(
' ');
176 if(!gf_entry.second.body_available())
185 called.find(decl.
name) != called.end() ||
193 if(!dead_map.empty())
198 add_to_json(ns, gf_entry.first, goto_program, dead_map, json_result);
203 os << json_result <<
'\n';
213 xmlt xml_result(
"unreachable-instructions");
219 if(!gf_entry.second.body_available())
226 if(!dead_map.empty())
231 ns, gf_entry.first, gf_entry.second.body, dead_map, json_result);
235 add_to_xml(gf_entry.first, gf_entry.second.body, dead_map, xml_result);
241 ns, gf_entry.first, gf_entry.second.body, dead_map, out);
247 out << json_result <<
'\n';
249 out << xml_result <<
'\n';
254 static std::optional<std::string>
301 const std::unordered_set<irep_idt> &called,
307 xmlt xml_result(unreachable ?
308 "unreachable-functions" :
309 "reachable-functions");
318 unreachable == (called.find(decl.
name) != called.end() ||
327 if(gf_entry.second.body_available())
340 last_location = end_function->source_location();
375 os << *file_name_opt <<
' ';
378 os <<
' ' << *line_opt;
380 os <<
' ' << *line_opt;
386 os << json_result <<
'\n';
388 os << xml_result <<
'\n';
423 std::unordered_set<irep_idt> called;
427 if(!gf_entry.second.body_available())
433 called.insert(gf_entry.first);
445 std::unordered_set<irep_idt> called =
459 std::unordered_set<irep_idt> called =
Compute dominators for CFG of goto_function.
This is the basic interface of the abstract interpreter with default implementations of the core func...
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...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
jsont & push_back(const jsont &json)
json_arrayt & make_array()
void output(std::ostream &out) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
bool get_bool_option(const std::string &option) const
void set_option(const std::string &option, const bool value)
const irep_idt & get_working_directory() const
const irep_idt & get_line() const
const irep_idt & get_file() const
irep_idt base_name
Base (non-scoped) name.
source_locationt location
Source code location of definition of symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
void set_attribute(const std::string &attribute, unsigned value)
xmlt & new_element(const std::string &key)
std::unordered_set< irep_idt > compute_called_functions(const goto_functionst &goto_functions)
computes the functions that are (potentially) called
#define forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
#define CHECK_RETURN(CONDITION)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
static void all_unreachable(const goto_programt &goto_program, dead_mapt &dest)
static std::optional< std::string > line_string_opt(const source_locationt &source_location)
bool static_unreachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
std::unordered_set< irep_idt > compute_called_functions_from_ai(const goto_modelt &goto_model, const ai_baset &ai)
static void list_functions(const goto_modelt &goto_model, const std::unordered_set< irep_idt > &called, const optionst &options, std::ostream &os, bool unreachable)
static void build_dead_map_from_ai(const goto_programt &goto_program, const ai_baset &ai, dead_mapt &dest)
static void add_to_xml(const irep_idt &function_identifier, const goto_programt &goto_program, const dead_mapt &dead_map, xmlt &dest)
static void xml_output_function(const irep_idt &function, const source_locationt &first_location, const source_locationt &last_location, xmlt &dest)
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)
static std::optional< std::string > file_name_string_opt(const source_locationt &source_location)
bool static_reachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
void unreachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
static void unreachable_instructions(const goto_programt &goto_program, dead_mapt &dest)
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
static void json_output_function(const irep_idt &function, const source_locationt &first_location, const source_locationt &last_location, json_arrayt &dest)
std::map< unsigned, goto_programt::const_targett > dead_mapt
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)
List all unreachable instructions.