CBMC
unreachable_instructions.cpp File Reference

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_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 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_idtcompute_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)
 

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

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 
)
static

Definition at line 116 of file unreachable_instructions.cpp.

◆ add_to_xml()

static void add_to_xml ( const irep_idt function_identifier,
const goto_programt goto_program,
const dead_mapt dead_map,
xmlt dest 
)
static

Definition at line 82 of file unreachable_instructions.cpp.

◆ all_unreachable()

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

Definition at line 48 of file unreachable_instructions.cpp.

◆ build_dead_map_from_ai()

static void build_dead_map_from_ai ( const goto_programt goto_program,
const ai_baset ai,
dead_mapt dest 
)
static

Definition at line 57 of file unreachable_instructions.cpp.

◆ compute_called_functions_from_ai()

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.

◆ file_name_string_opt()

static std::optional<std::string> file_name_string_opt ( const source_locationt source_location)
static

Definition at line 105 of file unreachable_instructions.cpp.

◆ 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

Definition at line 265 of file unreachable_instructions.cpp.

◆ line_string_opt()

static std::optional<std::string> line_string_opt ( const source_locationt source_location)
static

Definition at line 255 of file unreachable_instructions.cpp.

◆ list_functions()

static void list_functions ( const goto_modelt goto_model,
const std::unordered_set< irep_idt > &  called,
const optionst options,
std::ostream &  os,
bool  unreachable 
)
static

Definition at line 299 of file unreachable_instructions.cpp.

◆ output_dead_plain()

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

Definition at line 67 of file unreachable_instructions.cpp.

◆ reachable_functions()

void reachable_functions ( const goto_modelt goto_model,
const bool  json,
std::ostream &  os 
)

Definition at line 405 of file unreachable_instructions.cpp.

◆ static_reachable_functions()

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.

◆ static_unreachable_functions()

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.

◆ static_unreachable_instructions()

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.

◆ unreachable_functions()

void unreachable_functions ( const goto_modelt goto_model,
const bool  json,
std::ostream &  os 
)

Definition at line 391 of file unreachable_instructions.cpp.

◆ unreachable_instructions() [1/2]

void unreachable_instructions ( const goto_modelt goto_model,
const bool  json,
std::ostream &  os 
)

Definition at line 163 of file unreachable_instructions.cpp.

◆ unreachable_instructions() [2/2]

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

Definition at line 29 of file unreachable_instructions.cpp.

◆ xml_output_function()

static void xml_output_function ( const irep_idt function,
const source_locationt first_location,
const source_locationt last_location,
xmlt dest 
)
static

Definition at line 282 of file unreachable_instructions.cpp.