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