Intra-procedural dead-store detector (CWE-563). More...

#include <dead_store_analysis.h>

Inheritance diagram for goto_check_dead_store:

Public Member Functions
	goto_check_dead_store (const contextt &context, std::vector< dead_store_advisoryt > &out)
Public Member Functions inherited from goto_functions_algorithm
	goto_functions_algorithm (bool sideffect)
unsigned	get_number_of_functions ()
unsigned	get_number_of_loops ()
bool	run (goto_functionst &) override
	Executes the algorithm over a T object.
void	setTarget (const std::string &_tgt)
Public Member Functions inherited from algorithm< goto_functionst >
	algorithm (bool sideeffect)
virtual	~algorithm ()=default
bool	has_sideeffect ()
	Says wether the algorithm is a plain analysis or if it also changes the structure.

Protected Member Functions
bool	runOnFunction (std::pair< const irep_idt, goto_functiont > &F) override
Protected Member Functions inherited from goto_functions_algorithm
virtual bool	runOnLoop (loopst &loop, goto_programt &goto_program)
virtual bool	runOnProgram (goto_functionst &)

Protected Attributes
const contextt &	context
std::vector< dead_store_advisoryt > &	advisories
Protected Attributes inherited from goto_functions_algorithm
std::string	target_function = ""
Protected Attributes inherited from algorithm< goto_functionst >
const bool	sideeffect

Detailed Description

Intra-procedural dead-store detector (CWE-563).

Runs a backward live-variable analysis over each function's GOTO control-flow graph and appends one advisory per plain assignment to a tracked scalar local whose written value is never read afterwards. The pass is non-mutating: the GOTO program is left unchanged.

Only automatic-storage, non-extern, non-address-taken scalar locals are tracked; excluding address-taken variables keeps the analysis sound without an alias analysis (a variable whose address is never taken cannot be read through a pointer). Aggregates, arrays, return_value$* and __ESBMC_* symbols are out of scope.

Must run BEFORE mark_decl_as_non_det, which rewrites uninitialised DECLs into DECL; ASSIGN x = nondet; that synthetic store would otherwise be reported as a spurious dead store.

Constructor & Destructor Documentation

◆ goto_check_dead_store()

goto_check_dead_store::goto_check_dead_store	(	const contextt &	context,
		std::vector< dead_store_advisoryt > &	out )

inline

Member Function Documentation

◆ runOnFunction()

bool goto_check_dead_store::runOnFunction ( std::pair< const irep_idt, goto_functiont > & F )

overrideprotectedvirtual

Reimplemented from goto_functions_algorithm.

Member Data Documentation

◆ advisories

std::vector<dead_store_advisoryt>& goto_check_dead_store::advisories

protected

◆ context

const contextt& goto_check_dead_store::context

protected

The documentation for this class was generated from the following files:

src/goto-programs/dead_store_analysis.h
src/goto-programs/dead_store_analysis.cpp

Public Member Functions

Protected Member Functions

Protected Attributes