cprover
unreachable_instructions.cpp File Reference

List all unreachable instructions. More...

Include dependency graph for unreachable_instructions.cpp:

Go to the source code of this file.

Typedefs

typedef std::map< unsigned, goto_programt::const_targettdead_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)
 

Detailed Description

List all unreachable instructions.

Definition in file unreachable_instructions.cpp.

Typedef Documentation

◆ dead_mapt

typedef std::map<unsigned, goto_programt::const_targett> dead_mapt

Definition at line 27 of file unreachable_instructions.cpp.

Function Documentation

◆ add_to_json()

◆ all_unreachable()

static void all_unreachable ( const goto_programt goto_program,
dead_mapt dest 
)
static

Definition at line 48 of file unreachable_instructions.cpp.

References forall_goto_program_instructions.

Referenced by unreachable_instructions().

◆ json_output_function()

static void json_output_function ( const irep_idt function,
const source_locationt first_location,
const source_locationt last_location,
json_arrayt dest 
)
static

◆ list_functions()

◆ output_dead_plain()

static void output_dead_plain ( const namespacet ns,
const goto_programt goto_program,
const dead_mapt dead_map,
std::ostream &  os 
)
static

◆ reachable_functions()

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().

◆ unreachable_functions()

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().

◆ unreachable_instructions() [1/2]

static void unreachable_instructions ( const goto_programt goto_program,
dead_mapt dest 
)
static

◆ unreachable_instructions() [2/2]