12 #ifndef CPROVER_ANALYSES_LOCAL_SAFE_POINTERS_H
13 #define CPROVER_ANALYSES_LOCAL_SAFE_POINTERS_H
34 return e1.
type() != e2.
type() && e1 < e2;
Operator to dereference a pointer.
Base class for all expressions.
typet & type()
Return the type of the expression.
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
void output_safe_dereferences(std::ostream &stream, const goto_programt &program, const namespacet &ns)
Output safely dereferenced expressions per instruction in human-readable format.
bool is_safe_dereference(const dereference_exprt &deref, goto_programt::const_targett program_point)
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_poin...
void output(std::ostream &stream, const goto_programt &program, const namespacet &ns)
Output non-null expressions per instruction in human-readable format.
std::map< unsigned, std::set< exprt, type_comparet > > non_null_expressions
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
API to expression classes for Pointers.
API to expression classes.
Comparator that regards type-equal expressions as equal, and otherwise uses the natural (operator<) o...
bool operator()(const exprt &e1, const exprt &e2) const