cprover
|
List all unreachable instructions. More...
#include "unreachable_instructions.h"
#include <sstream>
#include <util/json.h>
#include <util/json_expr.h>
#include <util/file_util.h>
#include <analyses/cfg_dominators.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/compute_called_functions.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 | output_dead_plain (const namespacet &ns, const goto_programt &goto_program, const dead_mapt &dead_map, std::ostream &os) |
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) |
static void | json_output_function (const irep_idt &function, const source_locationt &first_location, const source_locationt &last_location, json_arrayt &dest) |
static void | list_functions (const goto_modelt &goto_model, const bool json, 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) |
List all unreachable instructions.
Definition in file unreachable_instructions.cpp.
typedef std::map<unsigned, goto_programt::const_targett> dead_mapt |
Definition at line 27 of file unreachable_instructions.cpp.
|
static |
Definition at line 77 of file unreachable_instructions.cpp.
References concat_dir_file(), irept::find(), id2string(), goto_program_templatet< codeT, guardT >::instructions, json(), jsont::make_array(), jsont::make_object(), goto_programt::output_instruction(), json_arrayt::push_back(), and size_type().
Referenced by unreachable_instructions().
|
static |
Definition at line 48 of file unreachable_instructions.cpp.
References forall_goto_program_instructions.
Referenced by unreachable_instructions().
|
static |
Definition at line 167 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 186 of file unreachable_instructions.cpp.
References jsont::array, symbolt::base_name, compute_called_functions(), concat_dir_file(), forall_goto_functions, source_locationt::get_file(), source_locationt::get_line(), source_locationt::get_working_directory(), goto_modelt::goto_functions, id2string(), goto_program_templatet< codeT, guardT >::instructions, json(), json_output_function(), symbolt::location, namespacet::lookup(), and goto_modelt::symbol_table.
Referenced by reachable_functions(), and unreachable_functions().
|
static |
Definition at line 57 of file unreachable_instructions.cpp.
References goto_program_templatet< codeT, guardT >::instructions, and goto_programt::output_instruction().
Referenced by unreachable_instructions().
void reachable_functions | ( | const goto_modelt & | goto_model, |
const bool | json, | ||
std::ostream & | os | ||
) |
Definition at line 258 of file unreachable_instructions.cpp.
References json(), and list_functions().
Referenced by goto_analyzer_parse_optionst::doit().
void unreachable_functions | ( | const goto_modelt & | goto_model, |
const bool | json, | ||
std::ostream & | os | ||
) |
Definition at line 250 of file unreachable_instructions.cpp.
References json(), and list_functions().
Referenced by goto_analyzer_parse_optionst::doit().
|
static |
Definition at line 29 of file unreachable_instructions.cpp.
References cfg_dominators_templatet< P, T, post_dom >::cfg, and cfg_baset< T, P, I >::entry_map.
Referenced by goto_analyzer_parse_optionst::doit(), and unreachable_instructions().
void unreachable_instructions | ( | const goto_modelt & | goto_model, |
const bool | json, | ||
std::ostream & | os | ||
) |
Definition at line 124 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, json(), namespacet::lookup(), output_dead_plain(), goto_modelt::symbol_table, and unreachable_instructions().