|
cprover
|
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>
Include dependency graph for unreachable_instructions.cpp: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.