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)

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.

Typedefs

Functions

Detailed Description

Typedef Documentation

◆ dead_mapt

Function Documentation

◆ add_to_json()

◆ add_to_xml()

◆ all_unreachable()

◆ build_dead_map_from_ai()

◆ compute_called_functions_from_ai()

◆ file_name_string_opt()

◆ json_output_function()

◆ line_string_opt()

◆ list_functions()

◆ output_dead_plain()

◆ reachable_functions()

◆ static_reachable_functions()

◆ static_unreachable_functions()

◆ static_unreachable_instructions()

◆ unreachable_functions()

◆ unreachable_instructions() [1/2]

◆ unreachable_instructions() [2/2]

◆ xml_output_function()