CBMC
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 <util/symbol.h>
18 
20 
21 class goto_functionst;
22 class goto_modelt;
23 class message_handlert;
24 
26 {
27 public:
31  const irep_idt &_fun_id)
33  {
34  }
35 
36  void update_requires(goto_programt &requires_);
37  void update_ensures(goto_programt &ensures);
38 
39  virtual void create_declarations() = 0;
40 
41  void add_memory_map_decl(goto_programt &program);
42  void add_memory_map_dead(goto_programt &program);
43 
44 protected:
45  void add_declarations(const std::string &decl_string);
46  void update_fn_call(
47  goto_programt::targett &target,
48  const std::string &name,
49  bool add_address_of);
50 
53 
56  const irep_idt &fun_id;
57 
58  // written by the child classes.
59  std::string memmap_name;
60  std::string requires_fn_name;
61  std::string ensures_fn_name;
63 
65 };
66 
68 {
69 public:
73  const irep_idt &_fun_id);
74 
75  virtual void create_declarations();
76 
77 protected:
78  virtual void create_requires_fn_call(goto_programt::targett &target);
79  virtual void create_ensures_fn_call(goto_programt::targett &target);
80 };
81 
83 {
84 public:
88  const irep_idt &_fun_id);
89 
90  virtual void create_declarations();
91 
92 protected:
93  virtual void create_requires_fn_call(goto_programt::targett &target);
94  virtual void create_ensures_fn_call(goto_programt::targett &target);
95 };
96 
100 {
101 public:
103  {
104  }
105 
106  // \brief return the set of functions invoked by
107  // the call graph of this program.
108  std::set<goto_programt::targett, goto_programt::target_less_than> &
109  is_fresh_calls();
110  void clear_set();
111  void operator()(goto_programt &prog);
112 
113 protected:
114  std::set<goto_programt::targett, goto_programt::target_less_than>
116 };
117 
122 {
123 public:
128  {
129  }
130 
131  // \brief return the set of functions invoked by
132  // the call graph of this program.
133  std::set<irep_idt> &function_calls();
134  void operator()(const goto_programt &prog);
135 
136 protected:
139  std::set<irep_idt> function_set;
140 };
141 
143 {
144 public:
146  {
147  }
148 
149  void operator()(const exprt &exp) override
150  {
151  }
152 };
153 
154 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H
Arrays with given size.
Definition: std_types.h:807
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
Predicate to be used with the exprt::visit() function.
void operator()(goto_programt &prog)
std::set< goto_programt::targett, goto_programt::target_less_than > & is_fresh_calls()
std::set< goto_programt::targett, goto_programt::target_less_than > function_set
void operator()(const exprt &exp) override
Predicate to be used with the exprt::visit() function.
void operator()(const goto_programt &prog)
const goto_functionst & goto_functions
std::set< irep_idt > & function_calls()
std::set< irep_idt > function_set
functions_in_scope_visitort(const goto_functionst &goto_functions, message_handlert &message_handler)
message_handlert & message_handler
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::iterator targett
Definition: goto_program.h:614
virtual void create_ensures_fn_call(goto_programt::targett &target)=0
const irep_idt & fun_id
void update_fn_call(goto_programt::targett &target, const std::string &name, bool add_address_of)
std::string ensures_fn_name
message_handlert & message_handler
std::string requires_fn_name
void add_memory_map_decl(goto_programt &program)
void update_requires(goto_programt &requires_)
void add_memory_map_dead(goto_programt &program)
virtual void create_declarations()=0
array_typet get_memmap_type()
goto_modelt & goto_model
void add_declarations(const std::string &decl_string)
std::string memmap_name
is_fresh_baset(goto_modelt &goto_model, message_handlert &message_handler, const irep_idt &_fun_id)
void update_ensures(goto_programt &ensures)
virtual void create_requires_fn_call(goto_programt::targett &target)=0
is_fresh_enforcet(goto_modelt &goto_model, message_handlert &message_handler, const irep_idt &_fun_id)
virtual void create_ensures_fn_call(goto_programt::targett &target)
virtual void create_requires_fn_call(goto_programt::targett &target)
virtual void create_declarations()
is_fresh_replacet(goto_modelt &goto_model, message_handlert &message_handler, const irep_idt &_fun_id)
virtual void create_ensures_fn_call(goto_programt::targett &target)
virtual void create_declarations()
virtual void create_requires_fn_call(goto_programt::targett &target)
Symbol table entry.
Definition: symbol.h:28
Concrete Goto Program.
double exp(double x)
Definition: math.c:2546
Symbol table entry.