cprover
memory_predicates.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Predicates to specify memory footprint in function contracts.
4
5Author: Felipe R. Monteiro
6
7Date: 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{
21public:
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
35protected:
36 void add_declarations(const std::string &decl_string);
37 void update_fn_call(
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{
57public:
59 code_contractst &_parent,
60 messaget _log,
61 const irep_idt _fun_id);
62
63 virtual void create_declarations();
64
65protected:
68};
69
71{
72public:
74 code_contractst &_parent,
75 messaget _log,
76 const irep_idt _fun_id);
77
78 virtual void create_declarations();
79
80protected:
83};
84
88{
89public:
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
100protected:
101 std::set<goto_programt::targett> function_set;
102};
103
108{
109public:
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
119protected:
120 bool found;
121};
122
127{
128public:
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
141protected:
144 std::set<irep_idt> function_set;
145};
146
148{
149public:
151 {
152 }
153
154 void operator()(const exprt &exp) override
155 {
156 }
157};
158
159#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
Predicate to be used with the exprt::visit() function.
void operator()(goto_programt &prog)
std::set< goto_programt::targett > function_set
std::set< goto_programt::targett > & is_fresh_calls()
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, messaget &log)
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:592
virtual void create_ensures_fn_call(goto_programt::targett &target)=0
void update_fn_call(goto_programt::targett &target, const std::string &name, bool add_address_of)
std::string ensures_fn_name
std::string requires_fn_name
code_contractst & parent
void update_requires(goto_programt &requires)
virtual void create_declarations()=0
void add_declarations(const std::string &decl_string)
std::string memmap_name
is_fresh_baset(code_contractst &_parent, messaget _log, const irep_idt _fun_id)
void update_ensures(goto_programt &ensures)
virtual void create_requires_fn_call(goto_programt::targett &target)=0
virtual void create_ensures_fn_call(goto_programt::targett &target)
virtual void create_requires_fn_call(goto_programt::targett &target)
is_fresh_enforcet(code_contractst &_parent, messaget _log, const irep_idt _fun_id)
virtual void create_declarations()
is_fresh_replacet(code_contractst &_parent, messaget _log, 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)
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
Predicate to be used with the exprt::visit() function.
void operator()(const exprt &exp) override
Verify and use annotated invariants and pre/post-conditions.