Loading...

Searching...

No Matches

Classes | Public Member Functions | Private Attributes | List of all members

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:

[フレーム]

[legend]

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.

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.

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.

void output_safe_dereferences (std::ostream &stream, const goto_programt &program, const namespacet &ns)

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

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_exprt s 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