CBMC
|
A contract is represented by a function declaration or definition with contract clauses attached to its signature: More...
#include <dfcc_contract_handler.h>
Public Member Functions | |
dfcc_contract_handlert (goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_instrumentt &instrument, dfcc_lift_memory_predicatest &memory_predicates, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen) | |
void | add_contract_instructions (const dfcc_contract_modet contract_mode, const irep_idt &wrapper_id, const irep_idt &wrapped_id, const irep_idt &contract_id, const symbolt &wrapper_write_set_symbol, goto_programt &dest, std::set< irep_idt > &function_pointer_contracts) |
Adds instructions in dest modeling contract checking, assuming that ret_t wrapper_id(params) is the function receiving the instructions. More... | |
const std::size_t | get_assigns_clause_size (const irep_idt &contract_id) |
Returns the size assigns clause of the given contract in number of targets. More... | |
const symbolt & | get_pure_contract_symbol (const irep_idt &contract_id, const std::optional< irep_idt > function_id_opt={}) |
Searches for a symbol named "contract::contract_id" in the symbol table. More... | |
Protected Member Functions | |
const dfcc_contract_functionst & | get_contract_functions (const irep_idt &contract_id) |
Returns the dfcc_contract_functionst object for the given contract from the cache, creates it if it does not exists. More... | |
void | check_signature_compat (const irep_idt &contract_id, const code_typet &contract_type, const irep_idt &pure_contract_id, const code_typet &pure_contract_type) |
Throws an error if the type signatures are not compatible. More... | |
Static Protected Attributes | |
static std::map< irep_idt, dfcc_contract_functionst > | contract_cache |
A contract is represented by a function declaration or definition with contract clauses attached to its signature:
In the symbol table, this declaration creates two symbols:
ret_t foo(foo_params)
which represents the function (with optional body)ret_t contract::foo(foo_params)
which represents the pure contract part and carries the contract clauses in its .type
attribute.This class allows, given a contract name foo
, to lookup the symbol contract::foo
and translate its assigns and frees clauses into GOTO functions that build dynamic frames at runtime (stored in an object of type dfcc_contract_functionst).
Translation results are cached so it is safe to call get_contract_functions
several times.
This class also implements the dfcc_contract_handlert interface and allows to generate instructions modelling contract checking and contract replacement.
Definition at line 64 of file dfcc_contract_handler.h.
dfcc_contract_handlert::dfcc_contract_handlert | ( | goto_modelt & | goto_model, |
message_handlert & | message_handler, | ||
dfcc_libraryt & | library, | ||
dfcc_instrumentt & | instrument, | ||
dfcc_lift_memory_predicatest & | memory_predicates, | ||
dfcc_spec_functionst & | spec_functions, | ||
dfcc_contract_clauses_codegent & | contract_clauses_codegen | ||
) |
Definition at line 38 of file dfcc_contract_handler.cpp.
void dfcc_contract_handlert::add_contract_instructions | ( | const dfcc_contract_modet | contract_mode, |
const irep_idt & | wrapper_id, | ||
const irep_idt & | wrapped_id, | ||
const irep_idt & | contract_id, | ||
const symbolt & | wrapper_write_set_symbol, | ||
goto_programt & | dest, | ||
std::set< irep_idt > & | function_pointer_contracts | ||
) |
Adds instructions in dest
modeling contract checking, assuming that ret_t wrapper_id(params)
is the function receiving the instructions.
[in] | contract_mode | checking or replacement mode |
[in] | wrapper_id | name of function receiving the instructions |
[in] | wrapped_id | name of function that is being checked/replaced |
[in] | contract_id | name of the contract to check |
[in] | wrapper_write_set_symbol | write_set parameter of the wrapper |
[out] | dest | destination program where instructions are added (should eventually become the body of wrapper_id) |
[out] | function_pointer_contracts | list of contracts found in either pre or post conditions of the processed contract. These contracts need to be swapped_and_wrapped in replacement mode if they are not already. |
Definition at line 88 of file dfcc_contract_handler.cpp.
|
protected |
Throws an error if the type signatures are not compatible.
contract_id | name of the function that carries the contract |
contract_type | code_type of contract_id |
pure_contract_id | name of the pure contract symbol for contract_id |
pure_contract_type | code_type of pure_contract_id |
Definition at line 171 of file dfcc_contract_handler.cpp.
const std::size_t dfcc_contract_handlert::get_assigns_clause_size | ( | const irep_idt & | contract_id | ) |
Returns the size assigns clause of the given contract in number of targets.
Definition at line 83 of file dfcc_contract_handler.cpp.
|
protected |
Returns the dfcc_contract_functionst
object for the given contract from the cache, creates it if it does not exists.
Definition at line 59 of file dfcc_contract_handler.cpp.
const symbolt & dfcc_contract_handlert::get_pure_contract_symbol | ( | const irep_idt & | contract_id, |
const std::optional< irep_idt > | function_id_opt = {} |
||
) |
Searches for a symbol named "contract::contract_id" in the symbol table.
If the "contract::contract_id" is found and function_id_opt
is present, type signature compatibility is checked between the contract and the function, and an exception is thrown if they are incompatible. If the symbol was not found and function_id_opt
was provided, the function is used as a template to derive a new default contract with empty requires, empty assigns, empty frees, empty ensures clauses. If the symbol was not found and function_id_opt
was not provided, a PRECONDITION is triggered.
Definition at line 111 of file dfcc_contract_handler.cpp.
|
staticprotected |
Definition at line 127 of file dfcc_contract_handler.h.
|
protected |
Definition at line 123 of file dfcc_contract_handler.h.
|
protected |
Definition at line 116 of file dfcc_contract_handler.h.
|
protected |
Definition at line 120 of file dfcc_contract_handler.h.
|
protected |
Definition at line 119 of file dfcc_contract_handler.h.
|
protected |
Definition at line 118 of file dfcc_contract_handler.h.
|
protected |
Definition at line 121 of file dfcc_contract_handler.h.
|
protected |
Definition at line 117 of file dfcc_contract_handler.h.
|
protected |
Definition at line 124 of file dfcc_contract_handler.h.
|
protected |
Definition at line 122 of file dfcc_contract_handler.h.