cprover
local_safe_pointers.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Local safe pointer analysis
4 
5 Author: Diffblue Ltd
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_ANALYSES_LOCAL_SAFE_POINTERS_H
13 #define CPROVER_ANALYSES_LOCAL_SAFE_POINTERS_H
14 
16 
17 #include <util/pointer_expr.h>
18 #include <util/std_expr.h>
19 
27 {
31  {
32  bool operator()(const exprt &e1, const exprt &e2) const
33  {
34  return e1.type() != e2.type() && e1 < e2;
35  }
36  };
37 
38  std::map<unsigned, std::set<exprt, type_comparet>> non_null_expressions;
39 
40 public:
41  void operator()(const goto_programt &goto_program);
42 
44  const exprt &expr, goto_programt::const_targett program_point);
45 
47  const dereference_exprt &deref,
48  goto_programt::const_targett program_point)
49  {
50  return is_non_null_at_program_point(deref.op(), program_point);
51  }
52 
53  void output(
54  std::ostream &stream,
55  const goto_programt &program,
56  const namespacet &ns);
57 
59  std::ostream &stream,
60  const goto_programt &program,
61  const namespacet &ns);
62 };
63 
64 #endif // CPROVER_ANALYSES_LOCAL_SAFE_POINTERS_H
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:386
local_safe_pointerst::output_safe_dereferences
void output_safe_dereferences(std::ostream &stream, const goto_programt &program, const namespacet &ns)
Output safely dereferenced expressions per instruction in human-readable format.
Definition: local_safe_pointers.cpp:233
local_safe_pointerst
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
Definition: local_safe_pointers.h:27
exprt
Base class for all expressions.
Definition: expr.h:54
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
pointer_expr.h
API to expression classes for Pointers.
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
local_safe_pointerst::output
void output(std::ostream &stream, const goto_programt &program, const namespacet &ns)
Output non-null expressions per instruction in human-readable format.
Definition: local_safe_pointers.cpp:189
goto_program.h
Concrete Goto Program.
local_safe_pointerst::type_comparet
Comparator that regards type-equal expressions as equal, and otherwise uses the natural (operator<) o...
Definition: local_safe_pointers.h:31
local_safe_pointerst::type_comparet::operator()
bool operator()(const exprt &e1, const exprt &e2) const
Definition: local_safe_pointers.h:32
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:564
local_safe_pointerst::operator()
void operator()(const goto_programt &goto_program)
Compute safe dereference expressions for a given GOTO program.
Definition: local_safe_pointers.cpp:82
local_safe_pointerst::non_null_expressions
std::map< unsigned, std::set< exprt, type_comparet > > non_null_expressions
Definition: local_safe_pointers.h:38
local_safe_pointerst::is_non_null_at_program_point
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...
Definition: local_safe_pointers.cpp:278
std_expr.h
API to expression classes.
local_safe_pointerst::is_safe_dereference
bool is_safe_dereference(const dereference_exprt &deref, goto_programt::const_targett program_point)
Definition: local_safe_pointers.h:46