cprover
code_contracts.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Verify and use annotated invariants and pre/post-conditions
4 
5 Author: Michael Tautschnig
6 
7 Date: February 2016
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H
15 #define CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H
16 
17 #include <set>
18 #include <string>
19 #include <unordered_set>
20 
23 
24 #include <util/namespace.h>
25 
26 class messaget;
27 
29 {
30 public:
32  : ns(goto_model.symbol_table),
33  symbol_table(goto_model.symbol_table),
34  goto_functions(goto_model.goto_functions),
36  log(log)
37  {
38  }
39 
53  bool replace_calls(const std::set<std::string> &);
54 
71  bool enforce_contracts(const std::set<std::string> &);
72 
75  bool enforce_contracts();
76 
80  bool replace_calls();
81 
82 protected:
86 
89 
90  std::unordered_set<irep_idt> summarized;
91 
93  bool enforce_contract(const std::string &);
94 
97  bool add_pointer_checks(const std::string &);
98 
102 
108  goto_programt::instructionst::iterator &ins_it,
109  goto_programt &program,
110  exprt &assigns,
111  std::vector<exprt> &original_references,
112  std::set<exprt> &freely_assignable_exprs);
113 
119  goto_programt::instructionst::iterator &ins_it,
120  goto_programt &program,
121  exprt &assigns,
122  std::vector<exprt> &assigns_references,
123  std::set<exprt> &freely_assignable_exprs);
124 
131  const symbolt &f_sym,
132  const irep_idt &func_id,
133  goto_programt &created_decls,
134  std::vector<exprt> &created_references);
135 
136  void code_contracts(goto_functionst::goto_functiont &goto_function);
137 
139  bool has_contract(const irep_idt);
140 
141  bool
142  apply_contract(goto_programt &goto_program, goto_programt::targett target);
143 
144  void
145  add_contract_check(const irep_idt &, const irep_idt &, goto_programt &dest);
146 
147  const symbolt &new_tmp_symbol(
148  const typet &type,
149  const source_locationt &source_location,
150  const irep_idt &function_id,
151  const irep_idt &mode);
152 };
153 
154 #define FLAG_REPLACE_CALL "replace-call-with-contract"
155 #define HELP_REPLACE_CALL \
156  " --replace-call-with-contract <fun>\n" \
157  " replace calls to fun with fun's contract\n"
158 
159 #define FLAG_REPLACE_ALL_CALLS "replace-all-calls-with-contracts"
160 #define HELP_REPLACE_ALL_CALLS \
161  " --replace-all-calls-with-contracts\n" \
162  " as above for all functions with a contract\n"
163 
164 #define FLAG_ENFORCE_CONTRACT "enforce-contract"
165 #define HELP_ENFORCE_CONTRACT \
166  " --enforce-contract <fun> wrap fun with an assertion of its contract\n"
167 
168 #define FLAG_ENFORCE_ALL_CONTRACTS "enforce-all-contracts"
169 #define HELP_ENFORCE_ALL_CONTRACTS \
170  " --enforce-all-contracts as above for all functions with a contract\n"
171 
172 #endif // CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H
bool enforce_contracts()
Call enforce_contracts() on all functions that have a contract.
bool check_for_looped_mallocs(const goto_programt &)
Check if there are any malloc statements which may be repeated because of a goto statement that jumps...
bool add_pointer_checks(const std::string &)
Insert assertion statements into the goto program to ensure that assigned memory is within the assign...
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &source_location, const irep_idt &function_id, const irep_idt &mode)
messaget & log
void code_contracts(goto_functionst::goto_functiont &goto_function)
symbol_tablet & symbol_table
void instrument_assigns_statement(goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns, std::vector< exprt > &original_references, std::set< exprt > &freely_assignable_exprs)
Inserts an assertion statement into program before the assignment ins_it, to ensure that the left-han...
bool replace_calls()
Call replace_calls() on all calls to any function that has a contract.
void populate_assigns_references(const symbolt &f_sym, const irep_idt &func_id, goto_programt &created_decls, std::vector< exprt > &created_references)
Creates a local variable declaration for each expression in the assigns clause (of the function given...
std::unordered_set< irep_idt > summarized
bool has_contract(const irep_idt)
Does the named function have a contract?
bool apply_contract(goto_programt &goto_program, goto_programt::targett target)
code_contractst(goto_modelt &goto_model, messaget &log)
unsigned temporary_counter
void instrument_call_statement(goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns, std::vector< exprt > &assigns_references, std::set< exprt > &freely_assignable_exprs)
Inserts an assertion statement into program before the function call at ins_it, to ensure that any me...
goto_functionst & goto_functions
void add_contract_check(const irep_idt &, const irep_idt &, goto_programt &dest)
bool enforce_contract(const std::string &)
Enforce contract of a single function.
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
A collection of goto functions.
::goto_functiont goto_functiont
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
instructionst::iterator targett
Definition: goto_program.h:550
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
The symbol table.
Definition: symbol_table.h:20
Symbol table entry.
Definition: symbol.h:28
The type of an expression, extends irept.
Definition: type.h:28
Goto Programs with Functions.
Symbol Table + CFG.