cprover
|
#include <contracts.h>
Public Member Functions | |
code_contractst (goto_modelt &goto_model, messaget &log) | |
bool | replace_calls (const std::set< std::string > &functions) |
Replace all calls to each function in the list with that function's contract. More... | |
bool | enforce_contracts (const std::set< std::string > &functions) |
Turn requires & ensures into assumptions and assertions for each of the named functions. More... | |
bool | enforce_contracts () |
Call enforce_contracts() on all functions that have a contract. More... | |
bool | replace_calls () |
Call replace_calls() on all calls to any function that has a contract. More... | |
void | apply_loop_contracts () |
const symbolt & | new_tmp_symbol (const typet &type, const source_locationt &source_location, const irep_idt &mode) |
void | check_apply_loop_contracts (goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, goto_programt::targett loop_head, const loopt &loop, const irep_idt &mode) |
symbol_tablet & | get_symbol_table () |
goto_functionst & | get_goto_functions () |
Public Attributes | |
namespacet | ns |
Protected Member Functions | |
bool | enforce_contract (const irep_idt &function) |
Enforce contract of a single function. More... | |
bool | check_frame_conditions_function (const irep_idt &function) |
Instrument functions to check frame conditions. More... | |
void | check_frame_conditions (goto_programt &program, const symbolt &target) |
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 &program) |
Check if there are any malloc statements which may be repeated because of a goto statement that jumps back. More... | |
void | instrument_assign_statement (goto_programt::instructionst::iterator &instruction_it, goto_programt &program, exprt &assigns, std::set< irep_idt > &freely_assignable_symbols, assigns_clauset &assigns_clause) |
Inserts an assertion statement into program before the assignment instruction_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::set< irep_idt > &freely_assignable_symbols, assigns_clauset &assigns_clause) |
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... | |
exprt | create_alias_expression (const exprt &lhs, std::vector< exprt > &aliasable_references) |
Creates a boolean expression which is true when there exists an expression in aliasable_references with the same pointer object and pointer offset as the address of lhs. More... | |
void | apply_loop_contract (const irep_idt &function, goto_functionst::goto_functiont &goto_function) |
Apply loop contracts, whenever available, to all loops in function . More... | |
bool | has_contract (const irep_idt) |
Does the named function have a contract? More... | |
bool | apply_function_contract (goto_programt &goto_program, goto_programt::targett target) |
Replaces function calls with assertions based on requires clauses, non-deterministic assignments for the write set, and assumptions based on ensures clauses. More... | |
void | add_contract_check (const irep_idt &wrapper_function, const irep_idt &mangled_function, goto_programt &dest) |
Instruments wrapper_function adding assumptions based on requires clauses and assertions based on ensures clauses. More... | |
void | add_quantified_variable (const exprt &expression, replace_symbolt &replace, const irep_idt &mode) |
This function recursively searches the expression to find nested or non-nested quantified expressions. More... | |
void | replace_history_parameter (exprt &expr, std::map< exprt, exprt > ¶meter2history, source_locationt location, const irep_idt &mode, goto_programt &history, const irep_idt &id) |
This function recursively identifies the "old" expressions within expr and replaces them with correspoding history variables. More... | |
std::pair< goto_programt, goto_programt > | create_ensures_instruction (codet &expression, source_locationt location, const irep_idt &mode) |
This function creates and returns an instruction that corresponds to the ensures clause. More... | |
Protected Attributes | |
symbol_tablet & | symbol_table |
goto_functionst & | goto_functions |
messaget & | log |
goto_convertt | converter |
std::unordered_set< irep_idt > | summarized |
Definition at line 61 of file contracts.h.
|
inline |
Definition at line 64 of file contracts.h.
|
protected |
Instruments wrapper_function
adding assumptions based on requires clauses and assertions based on ensures clauses.
Definition at line 1047 of file contracts.cpp.
|
protected |
This function recursively searches the expression to find nested or non-nested quantified expressions.
When a quantified expression is found, the quantified variable is added to the symbol table and to the expression map.
Definition at line 327 of file contracts.cpp.
|
protected |
Replaces function calls with assertions based on requires clauses, non-deterministic assignments for the write set, and assumptions based on ensures clauses.
Definition at line 475 of file contracts.cpp.
|
protected |
Apply loop contracts, whenever available, to all loops in function
.
Loop invariants, loop variants, and loop assigns clauses.
Definition at line 625 of file contracts.cpp.
void code_contractst::apply_loop_contracts | ( | ) |
Definition at line 1244 of file contracts.cpp.
void code_contractst::check_apply_loop_contracts | ( | goto_functionst::goto_functiont & | goto_function, |
const local_may_aliast & | local_may_alias, | ||
goto_programt::targett | loop_head, | ||
const loopt & | loop, | ||
const irep_idt & | mode | ||
) |
Definition at line 95 of file contracts.cpp.
|
protected |
Check if there are any malloc statements which may be repeated because of a goto statement that jumps back.
Definition at line 823 of file contracts.cpp.
|
protected |
Insert assertion statements into the goto program to ensure that assigned memory is within the assignable memory frame.
Definition at line 914 of file contracts.cpp.
|
protected |
Instrument functions to check frame conditions.
Definition at line 886 of file contracts.cpp.
|
protected |
Creates a boolean expression which is true when there exists an expression in aliasable_references with the same pointer object and pointer offset as the address of lhs.
Definition at line 669 of file contracts.cpp.
|
protected |
This function creates and returns an instruction that corresponds to the ensures clause.
It also returns a list of instructions related to initializing history variables, if required.
Definition at line 453 of file contracts.cpp.
|
protected |
Enforce contract of a single function.
Definition at line 984 of file contracts.cpp.
bool code_contractst::enforce_contracts | ( | ) |
Call enforce_contracts() on all functions that have a contract.
true
on failure, false
otherwise Definition at line 1261 of file contracts.cpp.
bool code_contractst::enforce_contracts | ( | const std::set< std::string > & | functions | ) |
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.
true
on failure, false
otherwise Definition at line 1272 of file contracts.cpp.
goto_functionst & code_contractst::get_goto_functions | ( | ) |
Definition at line 664 of file contracts.cpp.
symbol_tablet & code_contractst::get_symbol_table | ( | ) |
Definition at line 659 of file contracts.cpp.
|
protected |
Does the named function have a contract?
Definition at line 320 of file contracts.cpp.
|
protected |
Inserts an assertion statement into program before the assignment instruction_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 682 of file contracts.cpp.
|
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 711 of file contracts.cpp.
const symbolt & code_contractst::new_tmp_symbol | ( | const typet & | type, |
const source_locationt & | source_location, | ||
const irep_idt & | mode | ||
) |
Definition at line 645 of file contracts.cpp.
bool code_contractst::replace_calls | ( | ) |
Call replace_calls() on all calls to any function that has a contract.
true
on failure, false
otherwise Definition at line 1250 of file contracts.cpp.
bool code_contractst::replace_calls | ( | const std::set< std::string > & | functions | ) |
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
.
true
on failure, false
otherwise Definition at line 1195 of file contracts.cpp.
|
protected |
This function recursively identifies the "old" expressions within expr and replaces them with correspoding history variables.
Definition at line 395 of file contracts.cpp.
|
protected |
Definition at line 141 of file contracts.h.
|
protected |
Definition at line 138 of file contracts.h.
|
protected |
Definition at line 140 of file contracts.h.
namespacet code_contractst::ns |
Definition at line 134 of file contracts.h.
|
protected |
Definition at line 143 of file contracts.h.
|
protected |
Definition at line 137 of file contracts.h.