#include <code_contracts.h>
|
bool | enforce_contract (const std::string &) |
| Enforce contract of a single function. More...
|
|
bool | add_pointer_checks (const std::string &) |
| Insert assertion statements into the goto program to ensure that assigned memory is within the assignable memory frame. More...
|
|
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 back. More...
|
|
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-hand-side of the assignment aliases some expression in original_references, unless it is contained in freely_assignable_exprs. More...
|
|
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 memory which may be written by the call is aliased by some expression in assigns_references,unless it is contained in freely_assignable_exprs. More...
|
|
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 by f_sym), and stores them in created_decls. More...
|
|
void | code_contracts (goto_functionst::goto_functiont &goto_function) |
|
bool | has_contract (const irep_idt) |
| Does the named function have a contract? More...
|
|
bool | apply_contract (goto_programt &goto_program, goto_programt::targett target) |
|
void | add_contract_check (const irep_idt &, const irep_idt &, goto_programt &dest) |
|
const symbolt & | new_tmp_symbol (const typet &type, const source_locationt &source_location, const irep_idt &function_id, const irep_idt &mode) |
|
Definition at line 28 of file code_contracts.h.
◆ code_contractst()
◆ add_contract_check()
◆ add_pointer_checks()
bool code_contractst::add_pointer_checks |
( |
const std::string & |
function_name | ) |
|
|
protected |
Insert assertion statements into the goto program to ensure that assigned memory is within the assignable memory frame.
Definition at line 612 of file code_contracts.cpp.
◆ apply_contract()
◆ check_for_looped_mallocs()
bool code_contractst::check_for_looped_mallocs |
( |
const goto_programt & |
program | ) |
|
|
protected |
Check if there are any malloc statements which may be repeated because of a goto statement that jumps back.
Definition at line 551 of file code_contracts.cpp.
◆ code_contracts()
◆ enforce_contract()
bool code_contractst::enforce_contract |
( |
const std::string & |
fun_to_enforce | ) |
|
|
protected |
◆ enforce_contracts() [1/2]
bool code_contractst::enforce_contracts |
( |
| ) |
|
◆ enforce_contracts() [2/2]
bool code_contractst::enforce_contracts |
( |
const std::set< std::string > & |
funs_to_enforce | ) |
|
Turn requires & ensures into assumptions and assertions for each of the named functions.
Use this function to prove the correctness of a function F independently of its calling context. If you have proved that F is correct, then you can soundly replace all calls to F with F's contract using the code_contractst::replace_calls() function; this means that symbolic execution does not need to explore F every time it is called, increasing scalability.
Implementation: mangle the name of each function F into a new name, __CPROVER_contracts_original_F
(CF
for short). Then mint a new function called F
that assumes CF
's requires
clause, calls CF
, and then asserts CF
's ensures
clause.
- Returns
true
on failure, false
otherwise
Definition at line 951 of file code_contracts.cpp.
◆ has_contract()
bool code_contractst::has_contract |
( |
const irep_idt |
fun_name | ) |
|
|
protected |
◆ instrument_assigns_statement()
void code_contractst::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 |
|
) |
| |
|
protected |
Inserts an assertion statement into program before the assignment ins_it, to ensure that the left-hand-side of the assignment aliases some expression in original_references, unless it is contained in freely_assignable_exprs.
Definition at line 399 of file code_contracts.cpp.
◆ instrument_call_statement()
void code_contractst::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 |
|
) |
| |
|
protected |
Inserts an assertion statement into program before the function call at ins_it, to ensure that any memory which may be written by the call is aliased by some expression in assigns_references,unless it is contained in freely_assignable_exprs.
Definition at line 424 of file code_contracts.cpp.
◆ new_tmp_symbol()
◆ populate_assigns_references()
void code_contractst::populate_assigns_references |
( |
const symbolt & |
f_sym, |
|
|
const irep_idt & |
func_id, |
|
|
goto_programt & |
created_decls, |
|
|
std::vector< exprt > & |
created_references |
|
) |
| |
|
protected |
Creates a local variable declaration for each expression in the assigns clause (of the function given by f_sym), and stores them in created_decls.
Then creates assignment statements to capture the memory addresses of each expression in the assigns clause within the associated local variable, populating a vector created_references of these local variables.
Definition at line 366 of file code_contracts.cpp.
◆ replace_calls() [1/2]
bool code_contractst::replace_calls |
( |
| ) |
|
◆ replace_calls() [2/2]
bool code_contractst::replace_calls |
( |
const std::set< std::string > & |
funs_to_replace | ) |
|
Replace all calls to each function in the list with that function's contract.
Use this function when proving code that calls into an expensive function, F
. You can write a contract for F using __CPROVER_requires and __CPROVER_ensures, and then use this function to replace all calls to F
with an assertion that the requires
clause holds followed by an assumption that the ensures
clause holds. In order to ensure that F
actually abides by its ensures
and requires
clauses, you should separately call code_constractst::enforce_contracts()
on F
and verify it using cbmc --function F
.
- Returns
true
on failure, false
otherwise
Definition at line 876 of file code_contracts.cpp.
◆ goto_functions
◆ log
◆ ns
◆ summarized
std::unordered_set<irep_idt> code_contractst::summarized |
|
protected |
◆ symbol_table
◆ temporary_counter
unsigned code_contractst::temporary_counter |
|
protected |
The documentation for this class was generated from the following files: