27 typedef std::map<unsigned, goto_programt::const_targett>
dead_mapt;
34 dominators(goto_program);
36 for(cfg_dominatorst::cfgt::entry_mapt::const_iterator
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));
67 assert(end_function->is_end_function());
69 os <<
"\n*** " << end_function->function <<
" ***\n";
71 for(dead_mapt::const_iterator it=dead_map.begin();
89 assert(end_function->is_end_function());
94 id2string(end_function->source_location.get_working_directory()),
95 id2string(end_function->source_location.get_file())));
99 for(dead_mapt::const_iterator it=dead_map.begin();
103 std::ostringstream oss;
105 std::string s=oss.str();
108 assert(n!=std::string::npos);
110 n=s.find_first_not_of(
' ');
111 assert(n!=std::string::npos);
119 i_entry[
"sourceLocation"]=
json(l);
131 std::set<irep_idt> called;
138 if(!f_it->second.body_available())
148 if(called.find(decl.
base_name)!=called.end() ||
149 f_it->second.is_inlined())
154 if(!dead_map.empty())
159 add_to_json(ns, goto_program, dead_map, json_result);
163 if(json && !json_result.
array.empty())
164 os << json_result <<
'\n';
194 std::set<irep_idt> called;
206 (called.find(decl.
base_name)!=called.end() ||
207 f_it->second.is_inlined()))
213 if(f_it->second.body_available())
220 assert(end_function->is_end_function());
221 last_location=end_function->source_location;
236 << last_location.
get_line() <<
"\n";
246 if(json && !json_result.
array.empty())
247 os << json_result <<
'\n';
std::string concat_dir_file(const std::string &directory, const std::string &file_name)
const irep_idt & get_working_directory() const
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
const std::string & id2string(const irep_idt &d)
instructionst instructions
The list of instructions in the goto program.
static void json_output_function(const irep_idt &function, const source_locationt &first_location, const source_locationt &last_location, json_arrayt &dest)
unsignedbv_typet size_type()
symbol_tablet symbol_table
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static void list_functions(const goto_modelt &goto_model, const bool json, std::ostream &os, bool unreachable)
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()
static void output_dead_plain(const namespacet &ns, const goto_programt &goto_program, const dead_mapt &dead_map, std::ostream &os)
jsont & push_back(const jsont &json)
instructionst::const_iterator const_targett
const irep_idt & get_line() const
cfg_base_nodet< nodet, goto_programt::const_targett > nodet
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
List all unreachable instructions.
source_locationt location
Source code location of definition of symbol.
const irep_idt & get_file() const
void compute_called_functions(const goto_functionst &goto_functions, std::set< irep_idt > &functions)
computes the functions that are (potentially) called
irep_idt base_name
Base (non-scoped) name.
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)
json_objectt & make_object()
std::map< unsigned, goto_programt::const_targett > dead_mapt
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)
std::ostream & output_instruction(const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) const
See below.
#define forall_goto_program_instructions(it, program)
const irept & find(const irep_namet &name) const
goto_functionst goto_functions
json_objectt json(const source_locationt &location)