cprover
memory_predicates.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Predicates to specify memory footprint in function contracts.
4 
5 Author: Felipe R. Monteiro
6 
7 Date: July 2021
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H
15 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H
16 
17 #include "contracts.h"
18 
20 {
21 public:
23  code_contractst &_parent,
24  messaget _log,
25  const irep_idt _fun_id)
26  : parent(_parent), log(_log), fun_id(_fun_id)
27  {
28  }
29 
30  void update_requires(goto_programt &requires);
31  void update_ensures(goto_programt &ensures);
32 
33  virtual void create_declarations() = 0;
34 
35 protected:
36  void add_declarations(const std::string &decl_string);
37  void update_fn_call(
38  goto_programt::targett &target,
39  const std::string &name,
40  bool add_address_of);
41 
44 
48 
49  // written by the child classes.
50  std::string memmap_name;
51  std::string requires_fn_name;
52  std::string ensures_fn_name;
53 };
54 
56 {
57 public:
59  code_contractst &_parent,
60  messaget _log,
61  const irep_idt _fun_id);
62 
63  virtual void create_declarations();
64 
65 protected:
66  virtual void create_requires_fn_call(goto_programt::targett &target);
67  virtual void create_ensures_fn_call(goto_programt::targett &target);
68 };
69 
71 {
72 public:
74  code_contractst &_parent,
75  messaget _log,
76  const irep_idt _fun_id);
77 
78  virtual void create_declarations();
79 
80 protected:
81  virtual void create_requires_fn_call(goto_programt::targett &target);
82  virtual void create_ensures_fn_call(goto_programt::targett &target);
83 };
84 
88 {
89 public:
91  {
92  }
93 
94  // \brief return the set of functions invoked by
95  // the call graph of this program.
96  std::set<goto_programt::targett> &is_fresh_calls();
97  void clear_set();
98  void operator()(goto_programt &prog);
99 
100 protected:
101  std::set<goto_programt::targett> function_set;
102 };
103 
108 {
109 public:
111  {
112  }
113 
114  // \brief Has this object been passed to exprt::visit() on an exprt whose
115  // descendants contain __CPROVER_return_value?
116  bool found_return_value();
117  void operator()(const exprt &exp) override;
118 
119 protected:
120  bool found;
121 };
122 
127 {
128 public:
131  messaget &log)
133  {
134  }
135 
136  // \brief return the set of functions invoked by
137  // the call graph of this program.
138  std::set<irep_idt> &function_calls();
139  void operator()(const goto_programt &prog);
140 
141 protected:
144  std::set<irep_idt> function_set;
145 };
146 
148 {
149 public:
151  {
152  }
153 
154  void operator()(const exprt &exp) override
155  {
156  }
157 };
158 
159 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
is_fresh_enforcet
Definition: memory_predicates.h:56
is_fresh_baset::add_declarations
void add_declarations(const std::string &decl_string)
Definition: memory_predicates.cpp:144
is_fresh_baset::requires_fn_name
std::string requires_fn_name
Definition: memory_predicates.h:51
is_fresh_baset::ensures_fn_name
std::string ensures_fn_name
Definition: memory_predicates.h:52
function_binding_visitort::operator()
void operator()(const exprt &exp) override
Definition: memory_predicates.h:154
is_fresh_replacet::is_fresh_replacet
is_fresh_replacet(code_contractst &_parent, messaget _log, const irep_idt _fun_id)
Definition: memory_predicates.cpp:296
find_is_fresh_calls_visitort::find_is_fresh_calls_visitort
find_is_fresh_calls_visitort()
Definition: memory_predicates.h:90
function_binding_visitort::function_binding_visitort
function_binding_visitort()
Definition: memory_predicates.h:150
is_fresh_replacet::create_ensures_fn_call
virtual void create_ensures_fn_call(goto_programt::targett &target)
Definition: memory_predicates.cpp:347
is_fresh_enforcet::create_requires_fn_call
virtual void create_requires_fn_call(goto_programt::targett &target)
Definition: memory_predicates.cpp:275
functions_in_scope_visitort::function_calls
std::set< irep_idt > & function_calls()
Definition: memory_predicates.cpp:37
return_value_visitort
Predicate to be used with the exprt::visit() function.
Definition: memory_predicates.h:108
functions_in_scope_visitort::operator()
void operator()(const goto_programt &prog)
Definition: memory_predicates.cpp:42
exprt
Base class for all expressions.
Definition: expr.h:54
find_is_fresh_calls_visitort::operator()
void operator()(goto_programt &prog)
Definition: memory_predicates.cpp:97
is_fresh_baset::create_declarations
virtual void create_declarations()=0
return_value_visitort::return_value_visitort
return_value_visitort()
Definition: memory_predicates.h:110
is_fresh_baset::update_ensures
void update_ensures(goto_programt &ensures)
Definition: memory_predicates.cpp:128
is_fresh_baset::parent
code_contractst & parent
Definition: memory_predicates.h:45
is_fresh_baset::log
messaget log
Definition: memory_predicates.h:46
is_fresh_replacet::create_requires_fn_call
virtual void create_requires_fn_call(goto_programt::targett &target)
Definition: memory_predicates.cpp:342
functions_in_scope_visitort::function_set
std::set< irep_idt > function_set
Definition: memory_predicates.h:144
is_fresh_replacet
Definition: memory_predicates.h:71
is_fresh_baset::update_fn_call
void update_fn_call(goto_programt::targett &target, const std::string &name, bool add_address_of)
Definition: memory_predicates.cpp:208
is_fresh_enforcet::create_ensures_fn_call
virtual void create_ensures_fn_call(goto_programt::targett &target)
Definition: memory_predicates.cpp:280
find_is_fresh_calls_visitort::function_set
std::set< goto_programt::targett > function_set
Definition: memory_predicates.h:101
is_fresh_baset::fun_id
irep_idt fun_id
Definition: memory_predicates.h:47
function_binding_visitort
Definition: memory_predicates.h:148
code_contractst
Definition: contracts.h:62
const_expr_visitort
Definition: expr.h:373
functions_in_scope_visitort::log
messaget & log
Definition: memory_predicates.h:143
is_fresh_baset::create_ensures_fn_call
virtual void create_ensures_fn_call(goto_programt::targett &target)=0
return_value_visitort::operator()
void operator()(const exprt &exp) override
Definition: memory_predicates.cpp:29
is_fresh_baset
Definition: memory_predicates.h:20
find_is_fresh_calls_visitort
Predicate to be used with the exprt::visit() function.
Definition: memory_predicates.h:88
find_is_fresh_calls_visitort::is_fresh_calls
std::set< goto_programt::targett > & is_fresh_calls()
Definition: memory_predicates.cpp:87
contracts.h
Verify and use annotated invariants and pre/post-conditions.
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:25
functions_in_scope_visitort::functions_in_scope_visitort
functions_in_scope_visitort(const goto_functionst &goto_functions, messaget &log)
Definition: memory_predicates.h:129
is_fresh_enforcet::is_fresh_enforcet
is_fresh_enforcet(code_contractst &_parent, messaget _log, const irep_idt _fun_id)
Definition: memory_predicates.cpp:228
is_fresh_baset::memmap_name
std::string memmap_name
Definition: memory_predicates.h:50
is_fresh_baset::create_requires_fn_call
virtual void create_requires_fn_call(goto_programt::targett &target)=0
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
is_fresh_enforcet::create_declarations
virtual void create_declarations()
Definition: memory_predicates.cpp:245
is_fresh_baset::is_fresh_baset
is_fresh_baset(code_contractst &_parent, messaget _log, const irep_idt _fun_id)
Definition: memory_predicates.h:22
is_fresh_replacet::create_declarations
virtual void create_declarations()
Definition: memory_predicates.cpp:315
return_value_visitort::found_return_value
bool found_return_value()
Definition: memory_predicates.cpp:24
return_value_visitort::found
bool found
Definition: memory_predicates.h:120
find_is_fresh_calls_visitort::clear_set
void clear_set()
Definition: memory_predicates.cpp:92
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:646
functions_in_scope_visitort
Predicate to be used with the exprt::visit() function.
Definition: memory_predicates.h:127
is_fresh_baset::update_requires
void update_requires(goto_programt &requires)
Definition: memory_predicates.cpp:118
functions_in_scope_visitort::goto_functions
const goto_functionst & goto_functions
Definition: memory_predicates.h:142