27typedef std::map<unsigned, goto_programt::const_targett>
dead_mapt;
34 dominators(goto_program);
36 for(cfg_dominatorst::cfgt::entry_mapt::const_iterator
41 const cfg_dominatorst::cfgt::nodet &
n=dominators.
cfg[it->second];
42 if(
n.dominators.empty())
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);
89 x.set_attribute(
"name",
id2string(function_identifier));
91 for(dead_mapt::const_iterator it=dead_map.begin();
95 xmlt &
inst =
x.new_element(
"instruction");
96 inst.set_attribute(
"location_number",
97 std::to_string(it->second->location_number));
99 "source_location", it->second->source_location().as_string());
104static std::optional<std::string>
107 if(source_location.
get_file().empty())
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();
144 std::string::size_type
n=s.find(
'\n');
147 n=s.find_first_not_of(
' ');
176 if(!
gf_entry.second.body_available())
193 if(!dead_map.empty())
219 if(!
gf_entry.second.body_available())
226 if(!dead_map.empty())
254static std::optional<std::string>
294 x.set_attribute(
"first_line", *
line_opt);
301 const std::unordered_set<irep_idt> &
called,
308 "unreachable-functions" :
309 "reachable-functions");
327 if(
gf_entry.second.body_available())
423 std::unordered_set<irep_idt>
called;
427 if(!
gf_entry.second.body_available())
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 void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
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...
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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)
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_file() const
const irep_idt & get_line() const
source_locationt location
Source code location of definition of symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt irep_idt base_name
Name of module the symbol belongs to.
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.
static void all_unreachable(const goto_programt &goto_program, dead_mapt &dest)
bool static_unreachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
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)
std::unordered_set< irep_idt > compute_called_functions_from_ai(const goto_modelt &goto_model, const ai_baset &ai)
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)
static std::optional< std::string > line_string_opt(const source_locationt &source_location)
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.