13 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_WRAPPER_PROGRAM_H
14 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_WRAPPER_PROGRAM_H
117 const symbolt &caller_write_set_symbol,
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Generates GOTO functions modelling a contract assigns and frees clauses.
This class instruments GOTO functions or instruction sequences for frame condition checking and loop ...
Class interface to library types and functions defined in cprover_contracts.c.
Generates the body of a wrapper function from a contract specified using requires,...
const source_locationt wrapper_sl
Source location with wrapper function name as function name.
void encode_ensures_clauses()
Encodes postconditions, instruments them to check for side effects.
const symbol_exprt contract_write_set
Symbol for the write set object derived from the contract.
void encode_havoced_function_call()
Creates instructions that havoc the contract write set, create a nondet return value,...
const symbol_exprt caller_write_set
void encode_requires_write_set()
Encodes the empty write set used to check for side effects in requires.
void encode_requires_clauses()
Encodes preconditions, instruments them to check for side effects.
void encode_is_fresh_set()
Encodes the object set used to evaluate is fresh predicates,.
const symbol_exprt addr_of_requires_write_set
Symbol for the pointer to the write set used to check requires clauses.
void encode_contract_write_set()
Encodes the write set of the contract being checked/replaced (populated by calling functions provided...
const dfcc_contract_functionst & contract_functions
goto_programt link_allocated_caller
message_handlert & message_handler
const code_with_contract_typet & contract_code_type
const symbolt & contract_symbol
const symbol_exprt requires_write_set
Symbol for the write set used to check requires clauses for side effects.
exprt::operandst contract_lambda_parameters
Vector of arguments to use to instantiate the lambdas wrapping the contract clauses.
const symbol_exprt addr_of_ensures_write_set
Symbol for the pointer to the write set used to check ensures clauses.
goto_programt postconditions
const dfcc_contract_modet contract_mode
void encode_checked_function_call()
Creates a checked function call to the wrapped function, passing it the contract-derived write set as...
std::set< irep_idt > function_pointer_contracts
Set of required or ensured contracts for function pointers discovered when processing the contract of...
goto_programt write_set_checks
goto_programt link_is_fresh
const symbol_exprt addr_of_is_fresh_set
Symbol for the pointer to the is_fresh object set.
dfcc_lift_memory_predicatest & memory_predicates
const symbolt & wrapper_symbol
void add_to_dest(goto_programt &dest, std::set< irep_idt > &dest_fp_contracts)
Adds the whole program to dest and the discovered function pointer contracts dest_fp_contracts.
void encode_function_call()
Encodes the function call section of the wrapper program.
goto_programt function_call
const symbolt & wrapped_symbol
dfcc_wrapper_programt(const dfcc_contract_modet contract_mode, const symbolt &wrapper_symbol, const symbolt &wrapped_symbol, const dfcc_contract_functionst &contract_functions, const symbolt &caller_write_set_symbol, goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_instrumentt &instrument, dfcc_lift_memory_predicatest &memory_predicates)
goto_programt preconditions
const symbol_exprt addr_of_contract_write_set
Symbol for the pointer to the write set object derived from the contract.
const symbol_exprt ensures_write_set
Symbol for the write set used to check ensures clauses for side effects.
std::optional< symbol_exprt > return_value_opt
Symbol for the return value of the wrapped function.
dfcc_instrumentt & instrument
void encode_ensures_write_set()
Encodes the empty write set used to check for side effects in ensures.
goto_programt link_deallocated_contract
const symbol_exprt is_fresh_set
Symbol for the object set used to evaluate is_fresh predicates.
std::vector< exprt > operandst
A generic container class for the GOTO intermediate representation of one function.
Class that provides messages with a built-in verbosity 'level'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Expression to hold a symbol (variable)
Translates assigns and frees clauses of a function contract into goto functions that allow to build a...
Enum type representing the contract checking and replacement modes.
dfcc_contract_modet
Enum type representing the contract checking and replacement modes.
API to expression classes.