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
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
code_contractst::code_contracts
void code_contracts(goto_functionst::goto_functiont &goto_function)
Definition: code_contracts.cpp:301
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
code_contractst::add_contract_check
void add_contract_check(const irep_idt &, const irep_idt &, goto_programt &dest)
Definition: code_contracts.cpp:759
code_contractst::populate_assigns_references
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...
Definition: code_contracts.cpp:366
code_contractst::instrument_call_statement
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...
Definition: code_contracts.cpp:424
typet
The type of an expression, extends irept.
Definition: type.h:29
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
code_contractst::log
messaget & log
Definition: code_contracts.h:88
namespace.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
code_contractst::code_contractst
code_contractst(goto_modelt &goto_model, messaget &log)
Definition: code_contracts.h:31
code_contractst::temporary_counter
unsigned temporary_counter
Definition: code_contracts.h:87
code_contractst::has_contract
bool has_contract(const irep_idt)
Does the named function have a contract?
Definition: code_contracts.cpp:149
code_contractst::instrument_assigns_statement
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...
Definition: code_contracts.cpp:399
code_contractst::check_for_looped_mallocs
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...
Definition: code_contracts.cpp:551
code_contractst::apply_contract
bool apply_contract(goto_programt &goto_program, goto_programt::targett target)
Definition: code_contracts.cpp:160
code_contractst::add_pointer_checks
bool add_pointer_checks(const std::string &)
Insert assertion statements into the goto program to ensure that assigned memory is within the assign...
Definition: code_contracts.cpp:612
code_contractst
Definition: code_contracts.h:29
code_contractst::ns
namespacet ns
Definition: code_contracts.h:83
source_locationt
Definition: source_location.h:20
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
code_contractst::new_tmp_symbol
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &source_location, const irep_idt &function_id, const irep_idt &mode)
Definition: code_contracts.cpp:321
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
code_contractst::enforce_contracts
bool enforce_contracts()
Call enforce_contracts() on all functions that have a contract.
Definition: code_contracts.cpp:940
code_contractst::goto_functions
goto_functionst & goto_functions
Definition: code_contracts.h:85
symbolt
Symbol table entry.
Definition: symbol.h:28
goto_functions.h
Goto Programs with Functions.
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
code_contractst::replace_calls
bool replace_calls()
Call replace_calls() on all calls to any function that has a contract.
Definition: code_contracts.cpp:929
code_contractst::summarized
std::unordered_set< irep_idt > summarized
Definition: code_contracts.h:90
code_contractst::enforce_contract
bool enforce_contract(const std::string &)
Enforce contract of a single function.
Definition: code_contracts.cpp:695
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
code_contractst::symbol_table
symbol_tablet & symbol_table
Definition: code_contracts.h:84