CBMC
|
List all unreachable instructions. More...
#include "unreachable_instructions.h"
#include <util/json_irep.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>
#include <filesystem>
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 irep_idt &function_identifier, const goto_programt &goto_program, const dead_mapt &dead_map, std::ostream &os) |
static void | add_to_xml (const irep_idt &function_identifier, const goto_programt &goto_program, const dead_mapt &dead_map, xmlt &dest) |
static std::optional< std::string > | file_name_string_opt (const source_locationt &source_location) |
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) |
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 std::optional< std::string > | line_string_opt (const source_locationt &source_location) |
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 27 of file unreachable_instructions.cpp.
|
static |
Definition at line 116 of file unreachable_instructions.cpp.
|
static |
Definition at line 82 of file unreachable_instructions.cpp.
|
static |
Definition at line 48 of file unreachable_instructions.cpp.
|
static |
Definition at line 57 of file unreachable_instructions.cpp.
std::unordered_set<irep_idt> compute_called_functions_from_ai | ( | const goto_modelt & | goto_model, |
const ai_baset & | ai | ||
) |
Definition at line 419 of file unreachable_instructions.cpp.
|
static |
Definition at line 105 of file unreachable_instructions.cpp.
|
static |
Definition at line 265 of file unreachable_instructions.cpp.
|
static |
Definition at line 255 of file unreachable_instructions.cpp.
|
static |
Definition at line 299 of file unreachable_instructions.cpp.
|
static |
Definition at line 67 of file unreachable_instructions.cpp.
void reachable_functions | ( | const goto_modelt & | goto_model, |
const bool | json, | ||
std::ostream & | os | ||
) |
Definition at line 405 of file unreachable_instructions.cpp.
bool static_reachable_functions | ( | const goto_modelt & | goto_model, |
const ai_baset & | ai, | ||
const optionst & | options, | ||
std::ostream & | out | ||
) |
Definition at line 453 of file unreachable_instructions.cpp.
bool static_unreachable_functions | ( | const goto_modelt & | goto_model, |
const ai_baset & | ai, | ||
const optionst & | options, | ||
std::ostream & | out | ||
) |
Definition at line 439 of file unreachable_instructions.cpp.
bool static_unreachable_instructions | ( | const goto_modelt & | goto_model, |
const ai_baset & | ai, | ||
const optionst & | options, | ||
std::ostream & | out | ||
) |
Definition at line 206 of file unreachable_instructions.cpp.
void unreachable_functions | ( | const goto_modelt & | goto_model, |
const bool | json, | ||
std::ostream & | os | ||
) |
Definition at line 391 of file unreachable_instructions.cpp.
void unreachable_instructions | ( | const goto_modelt & | goto_model, |
const bool | json, | ||
std::ostream & | os | ||
) |
Definition at line 163 of file unreachable_instructions.cpp.
|
static |
Definition at line 29 of file unreachable_instructions.cpp.
|
static |
Definition at line 282 of file unreachable_instructions.cpp.