cprover
|
List all unreachable instructions. More...
#include "unreachable_instructions.h"
#include <util/file_util.h>
#include <util/json_expr.h>
#include <util/options.h>
#include <util/xml.h>
#include <goto-programs/compute_called_functions.h>
#include <analyses/ai.h>
#include <analyses/cfg_dominators.h>
Go to the source code of this file.
Typedefs | |
typedef std::map< unsigned, goto_programt::const_targett > | dead_mapt |
Functions | |
static void | unreachable_instructions (const goto_programt &goto_program, dead_mapt &dest) |
static void | all_unreachable (const goto_programt &goto_program, dead_mapt &dest) |
static void | build_dead_map_from_ai (const goto_programt &goto_program, const ai_baset &ai, dead_mapt &dest) |
static void | output_dead_plain (const namespacet &ns, const goto_programt &goto_program, const dead_mapt &dead_map, std::ostream &os) |
static void | add_to_xml (const goto_programt &goto_program, const dead_mapt &dead_map, xmlt &dest) |
static void | add_to_json (const namespacet &ns, const goto_programt &goto_program, const dead_mapt &dead_map, json_arrayt &dest) |
void | unreachable_instructions (const goto_modelt &goto_model, const bool json, std::ostream &os) |
bool | static_unreachable_instructions (const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out) |
static void | json_output_function (const irep_idt &function, const source_locationt &first_location, const source_locationt &last_location, json_arrayt &dest) |
static void | xml_output_function (const irep_idt &function, const source_locationt &first_location, const source_locationt &last_location, xmlt &dest) |
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 | unreachable_functions (const goto_modelt &goto_model, const bool json, std::ostream &os) |
void | reachable_functions (const goto_modelt &goto_model, const bool json, std::ostream &os) |
std::unordered_set< irep_idt > | compute_called_functions_from_ai (const goto_modelt &goto_model, const ai_baset &ai) |
bool | static_unreachable_functions (const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out) |
bool | static_reachable_functions (const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out) |
List all unreachable instructions.
Definition in file unreachable_instructions.cpp.
typedef std::map<unsigned, goto_programt::const_targett> dead_mapt |
Definition at line 26 of file unreachable_instructions.cpp.
|
static |
Definition at line 114 of file unreachable_instructions.cpp.
References concat_dir_file(), DATA_INVARIANT, irept::find(), goto_program, id2string(), goto_programt::instructions, json(), jsont::make_array(), jsont::make_object(), goto_programt::output_instruction(), PRECONDITION, json_arrayt::push_back(), and size_type().
Referenced by static_unreachable_instructions(), and unreachable_instructions().
|
static |
Definition at line 86 of file unreachable_instructions.cpp.
References DATA_INVARIANT, goto_program, id2string(), goto_programt::instructions, xmlt::new_element(), PRECONDITION, xmlt::set_attribute(), and to_string().
Referenced by static_unreachable_instructions().
|
static |
Definition at line 47 of file unreachable_instructions.cpp.
References forall_goto_program_instructions, and goto_program.
Referenced by unreachable_instructions().
|
static |
Definition at line 56 of file unreachable_instructions.cpp.
References ai_baset::abstract_state_before(), forall_goto_program_instructions, and goto_program.
Referenced by static_unreachable_instructions().
std::unordered_set<irep_idt> compute_called_functions_from_ai | ( | const goto_modelt & | goto_model, |
const ai_baset & | ai | ||
) |
Definition at line 408 of file unreachable_instructions.cpp.
References ai_baset::abstract_state_before(), forall_goto_functions, goto_modelt::goto_functions, and goto_programt::instructions.
Referenced by static_reachable_functions(), and static_unreachable_functions().
|
static |
Definition at line 253 of file unreachable_instructions.cpp.
References concat_dir_file(), source_locationt::get_file(), source_locationt::get_line(), source_locationt::get_working_directory(), id2string(), jsont::make_object(), and json_arrayt::push_back().
Referenced by list_functions().
|
static |
Definition at line 289 of file unreachable_instructions.cpp.
References jsont::array, symbolt::base_name, concat_dir_file(), dstringt::empty(), forall_goto_functions, optionst::get_bool_option(), source_locationt::get_file(), source_locationt::get_line(), source_locationt::get_working_directory(), goto_modelt::goto_functions, goto_program, id2string(), goto_programt::instructions, json_output_function(), symbolt::location, namespacet::lookup(), goto_modelt::symbol_table, and xml_output_function().
Referenced by reachable_functions(), static_reachable_functions(), static_unreachable_functions(), and unreachable_functions().
|
static |
Definition at line 66 of file unreachable_instructions.cpp.
References goto_program, goto_programt::instructions, and goto_programt::output_instruction().
Referenced by static_unreachable_instructions(), and unreachable_instructions().
void reachable_functions | ( | const goto_modelt & | goto_model, |
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 & | goto_model, |
const ai_baset & | ai, | ||
const optionst & | options, | ||
std::ostream & | out | ||
) |
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 & | goto_model, |
const ai_baset & | ai, | ||
const optionst & | options, | ||
std::ostream & | out | ||
) |
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 & | goto_model, |
const ai_baset & | ai, | ||
const optionst & | options, | ||
std::ostream & | out | ||
) |
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 & | goto_model, |
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().
|
static |
Definition at line 28 of file unreachable_instructions.cpp.
References cfg_dominators_templatet< P, T, post_dom >::cfg, cfg_baset< T, P, I >::entry_map, and goto_program.
Referenced by janalyzer_parse_optionst::perform_analysis(), goto_analyzer_parse_optionst::perform_analysis(), and unreachable_instructions().
void unreachable_instructions | ( | const goto_modelt & | goto_model, |
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().
|
static |
Definition at line 272 of file unreachable_instructions.cpp.
References concat_dir_file(), source_locationt::get_file(), source_locationt::get_line(), source_locationt::get_working_directory(), id2string(), xmlt::new_element(), and xmlt::set_attribute().
Referenced by list_functions().