local_safe_pointerst Class Reference

A very simple, cheap analysis to determine when dereference operations are trivially guarded by a check against a null pointer access. More...

#include <local_safe_pointers.h>

Collaboration diagram for local_safe_pointerst:

Classes
struct	type_comparet
	Comparator that regards type-equal expressions as equal, and otherwise uses the natural (operator<) ordering on irept. More...

Public Member Functions
void	operator() (const goto_programt &goto_program)
	Compute safe dereference expressions for a given GOTO program. More...
bool	is_non_null_at_program_point (const exprt &expr, goto_programt::const_targett program_point)
	Return true if the local-safe-pointers analysis has determined expr cannot be null as of program_point (i.e. More...
bool	is_safe_dereference (const dereference_exprt &deref, goto_programt::const_targett program_point)
void	output (std::ostream &stream, const goto_programt &program, const namespacet &ns)
	Output non-null expressions per instruction in human-readable format. More...
void	output_safe_dereferences (std::ostream &stream, const goto_programt &program, const namespacet &ns)
	Output safely dereferenced expressions per instruction in human-readable format. More...

Private Attributes
std::map< unsigned, std::set< exprt, type_comparet > >	non_null_expressions

Detailed Description

A very simple, cheap analysis to determine when dereference operations are trivially guarded by a check against a null pointer access.

In the interests of a very cheap analysis we only search for very local guards – at the moment only if(x != null) { *x } and assume(x != null); *x are handled. Control-flow convergence and possibly-aliasing operations are handled pessimistically.

Definition at line 27 of file local_safe_pointers.h.

Member Function Documentation

is_non_null_at_program_point()

bool local_safe_pointerst::is_non_null_at_program_point	(	const exprt &	expr,
		goto_programt::const_targett	program_point
	)

Return true if the local-safe-pointers analysis has determined expr cannot be null as of program_point (i.e.

that expr is non-null when the program_point instruction starts executing)

Definition at line 278 of file local_safe_pointers.cpp.

is_safe_dereference()

bool local_safe_pointerst::is_safe_dereference ( const dereference_exprt &  deref, goto_programt::const_targett  program_point  )

inline

Definition at line 47 of file local_safe_pointers.h.

operator()()

void local_safe_pointerst::operator()

(

const goto_programt &

goto_program

)

Compute safe dereference expressions for a given GOTO program.

This populates non_null_expressions mapping instruction location numbers onto a set of expressions that are known to be non-null BEFORE that instruction is executed.

Parameters

goto_program

program to analyse

Definition at line 82 of file local_safe_pointers.cpp.

output()

void local_safe_pointerst::output	(	std::ostream &	out,
		const goto_programt &	goto_program,
		const namespacet &	ns
	)

Output non-null expressions per instruction in human-readable format.

Parameters

out	stream to write output to
goto_program	GOTO program analysed (the same one passed to operator())
ns	namespace

Definition at line 189 of file local_safe_pointers.cpp.

output_safe_dereferences()

void local_safe_pointerst::output_safe_dereferences	(	std::ostream &	out,
		const goto_programt &	goto_program,
		const namespacet &	ns
	)

Output safely dereferenced expressions per instruction in human-readable format.

For example, if we have an instruction ASSUME x->y->z == a->b and we know expressions x->y, a and other are not null prior to it, this will print {x->y, a}, the intersection of the dereference_exprts used here and the known-not-null expressions.

Parameters

out	stream to write output to
goto_program	GOTO program analysed (the same one passed to operator())
ns	namespace

Definition at line 233 of file local_safe_pointers.cpp.

Member Data Documentation

non_null_expressions

std::map<unsigned, std::set<exprt, type_comparet> > local_safe_pointerst::non_null_expressions

private

Definition at line 39 of file local_safe_pointers.h.

---

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

• /home/runner/work/cbmc/cbmc/src/analyses/local_safe_pointers.h
• /home/runner/work/cbmc/cbmc/src/analyses/local_safe_pointers.cpp