cprover
Loading...
Searching...
No Matches
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()

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

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

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

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

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

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

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

Definition at line 255 of file unreachable_instructions.cpp.

◆ list_functions()

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

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]

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

Definition at line 29 of file unreachable_instructions.cpp.

◆ xml_output_function()

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.