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 #include <util/std_expr.h>
17 
25 {
32  {
33  const namespacet &ns;
34 
35  public:
36  explicit base_type_comparet(const namespacet &ns)
37  : ns(ns)
38  {
39  }
40 
42  : ns(other.ns)
43  {
44  }
45 
47  {
48  INVARIANT(&ns == &other.ns, "base_type_comparet: clashing namespaces");
49  return *this;
50  }
51 
52  bool operator()(const exprt &e1, const exprt &e2) const;
53  };
54 
55  std::map<unsigned, std::set<exprt, base_type_comparet>> non_null_expressions;
56 
57  const namespacet &ns;
58 
59 public:
61  : ns(ns)
62  {
63  }
64 
66 
68  const exprt &expr, goto_programt::const_targett program_point);
69 
71  const dereference_exprt &deref,
72  goto_programt::const_targett program_point)
73  {
74  return is_non_null_at_program_point(deref.op0(), program_point);
75  }
76 
77  void output(std::ostream &stream, const goto_programt &program);
78 
80  std::ostream &stream, const goto_programt &program);
81 };
82 
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.
exprt & op0()
Definition: expr.h:72
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)
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
void operator()(const goto_programt &goto_program)
Compute safe dereference expressions for a given GOTO program.
Operator to dereference a pointer.
Definition: std_expr.h:3282
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
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
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.
Definition: goto_program.h:70
base_type_comparet(const base_type_comparet &other)
const namespacet & ns
Base class for all expressions.
Definition: expr.h:42
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...
goto_programt & goto_program
Definition: cover.cpp:63
Concrete Goto Program.
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