cprover
|
List all unreachable instructions. More...
#include <iosfwd>
Go to the source code of this file.
Functions | |
void | unreachable_instructions (const goto_modelt &, const bool json, std::ostream &os) |
void | unreachable_functions (const goto_modelt &, const bool json, std::ostream &os) |
void | reachable_functions (const goto_modelt &, const bool json, std::ostream &os) |
bool | static_unreachable_instructions (const goto_modelt &, const ai_baset &, const optionst &, std::ostream &) |
bool | static_unreachable_functions (const goto_modelt &, const ai_baset &, const optionst &, std::ostream &) |
bool | static_reachable_functions (const goto_modelt &, const ai_baset &, const optionst &, std::ostream &) |
List all unreachable instructions.
Definition in file unreachable_instructions.h.
void reachable_functions | ( | const goto_modelt & | , |
const bool | json, | ||
std::ostream & | os | ||
) |
Definition at line 392 of file unreachable_instructions.cpp.
References compute_called_functions(), json(), list_functions(), and optionst::set_option().
Referenced by janalyzer_parse_optionst::perform_analysis(), and goto_analyzer_parse_optionst::perform_analysis().
bool static_reachable_functions | ( | const goto_modelt & | , |
const ai_baset & | , | ||
const optionst & | , | ||
std::ostream & | |||
) |
Definition at line 442 of file unreachable_instructions.cpp.
References compute_called_functions_from_ai(), and list_functions().
Referenced by janalyzer_parse_optionst::perform_analysis(), and goto_analyzer_parse_optionst::perform_analysis().
bool static_unreachable_functions | ( | const goto_modelt & | , |
const ai_baset & | , | ||
const optionst & | , | ||
std::ostream & | |||
) |
Definition at line 428 of file unreachable_instructions.cpp.
References compute_called_functions_from_ai(), and list_functions().
Referenced by janalyzer_parse_optionst::perform_analysis(), and goto_analyzer_parse_optionst::perform_analysis().
bool static_unreachable_instructions | ( | const goto_modelt & | , |
const ai_baset & | , | ||
const optionst & | , | ||
std::ostream & | |||
) |
Definition at line 204 of file unreachable_instructions.cpp.
References add_to_json(), add_to_xml(), jsont::array, build_dead_map_from_ai(), forall_goto_functions, optionst::get_bool_option(), goto_modelt::goto_functions, goto_program, INVARIANT, output_dead_plain(), and goto_modelt::symbol_table.
Referenced by janalyzer_parse_optionst::perform_analysis(), and goto_analyzer_parse_optionst::perform_analysis().
void unreachable_functions | ( | const goto_modelt & | , |
const bool | json, | ||
std::ostream & | os | ||
) |
Definition at line 376 of file unreachable_instructions.cpp.
References compute_called_functions(), json(), list_functions(), and optionst::set_option().
Referenced by janalyzer_parse_optionst::perform_analysis(), and goto_analyzer_parse_optionst::perform_analysis().
void unreachable_instructions | ( | const goto_modelt & | , |
const bool | json, | ||
std::ostream & | os | ||
) |
Definition at line 162 of file unreachable_instructions.cpp.
References add_to_json(), all_unreachable(), jsont::array, symbolt::base_name, compute_called_functions(), forall_goto_functions, goto_modelt::goto_functions, goto_program, json(), namespacet::lookup(), output_dead_plain(), goto_modelt::symbol_table, and unreachable_instructions().