cprover
Loading...
Searching...
No Matches
Dynamic Frame Condition Checking (DFCC)
+ Collaboration diagram for Dynamic Frame Condition Checking (DFCC):

Files

file  dfcc.h
 Main class orchestrating the the whole program transformation for function contracts with Dynamic Frame Condition Checking (DFCC)
 

Classes

class  dfcct
 Entry point into the contracts transformation. More...
 

Functions

void dfcc (const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, const optionalt< irep_idt > &to_check, const bool allow_recursive_calls, const std::set< irep_idt > &to_replace, const bool apply_loop_contracts, const bool unwind_transformed_loops, const std::set< std::string > &to_exclude_from_nondet_static, message_handlert &message_handler)
 Applies function contracts transformation to GOTO model, using the dynamic frame condition checking approach.
 
void dfcc (const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, const optionalt< std::pair< irep_idt, irep_idt > > &to_check, const bool allow_recursive_calls, const std::map< irep_idt, irep_idt > &to_replace, const bool apply_loop_contracts, const bool unwind_transformed_loops, const std::set< std::string > &to_exclude_from_nondet_static, message_handlert &message_handler)
 Applies function contracts and loop contracts transformation to GOTO model, using the dynamic frame condition checking approach.
 

Detailed Description

Function Documentation

◆ dfcc() [1/2]

void dfcc ( const optionst & options,
goto_modelt & goto_model,
const irep_idt & harness_id,
const optionalt< irep_idt > & to_check,
const bool allow_recursive_calls,
const std::set< irep_idt > & to_replace,
const bool apply_loop_contracts,
const bool unwind_transformed_loops,
const std::set< std::string > & to_exclude_from_nondet_static,
message_handlert & message_handler )

Applies function contracts transformation to GOTO model, using the dynamic frame condition checking approach.

Precondition
This function requires that the contract associated to function foo exists in the symbol table as symbol contract::foo.
Parameters
optionsCLI options (used to lookup options for language config when re-defining the model's entry point)
goto_modelGOTO model to transform
harness_idproof harness name, must be the entry point of the model
to_checkfunction to check against its contract
allow_recursive_callsAllow the checked function to be recursive
to_replaceset of functions to replace with their contract
apply_loop_contractsapply loop contract transformations iff true
unwind_transformed_loopsunwind transformed loops after applying loop contracts.
to_exclude_from_nondet_staticset of symbols to exclude when havocing static program symbols.
message_handlerused for debug/warning/error messages

Definition at line 116 of file dfcc.cpp.

◆ dfcc() [2/2]

void dfcc ( const optionst & options,
goto_modelt & goto_model,
const irep_idt & harness_id,
const optionalt< std::pair< irep_idt, irep_idt > > & to_check,
const bool allow_recursive_calls,
const std::map< irep_idt, irep_idt > & to_replace,
const bool apply_loop_contracts,
const bool unwind_transformed_loops,
const std::set< std::string > & to_exclude_from_nondet_static,
message_handlert & message_handler )

Applies function contracts and loop contracts transformation to GOTO model, using the dynamic frame condition checking approach.

Functions to check/replace are explicitly mapped to contracts. When checking function foo against contract bar, we require the actual contract symbol to exist as contract::bar in the symbol table.

Parameters
optionsCLI options (used to lookup options for language config when re-defining the model's entry point)
goto_modelGOTO model to transform
harness_idProof harness name, must be the entry point of the model
to_check(function,contract) pair for contract checking
allow_recursive_callsAllow the checked function to be recursive
to_replaceFunctions-to-contract mapping for replacement
apply_loop_contractsApply loop contract transformations iff true
unwind_transformed_loopsunwind transformed loops after applying loop contracts.
to_exclude_from_nondet_staticSet of symbols to exclude when havocing static program symbols.
message_handlerused for debug/warning/error messages

Definition at line 146 of file dfcc.cpp.