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 std::optional< 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. More...
void	dfcc (const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, const std::optional< 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. More...

Detailed Description

Function Documentation

dfcc() [1/2]

void dfcc	(	const optionst &	options,
		goto_modelt &	goto_model,
		const irep_idt &	harness_id,
		const std::optional< 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

options	CLI options (used to lookup options for language config when re-defining the model's entry point)
goto_model	GOTO model to transform
harness_id	proof harness name, must be the entry point of the model
to_check	function to check against its contract
allow_recursive_calls	Allow the checked function to be recursive
to_replace	set of functions to replace with their contract
apply_loop_contracts	apply loop contract transformations iff true
unwind_transformed_loops	unwind transformed loops after applying loop contracts.
to_exclude_from_nondet_static	set of symbols to exclude when havocing static program symbols.
message_handler	used for debug/warning/error messages

Definition at line 115 of file dfcc.cpp.

dfcc() [2/2]

void dfcc	(	const optionst &	options,
		goto_modelt &	goto_model,
		const irep_idt &	harness_id,
		const std::optional< 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

options	CLI options (used to lookup options for language config when re-defining the model's entry point)
goto_model	GOTO model to transform
harness_id	Proof harness name, must be the entry point of the model
to_check	(function,contract) pair for contract checking
allow_recursive_calls	Allow the checked function to be recursive
to_replace	Functions-to-contract mapping for replacement
apply_loop_contracts	Apply loop contract transformations iff true
unwind_transformed_loops	unwind transformed loops after applying loop contracts.
to_exclude_from_nondet_static	Set of symbols to exclude when havocing static program symbols.
message_handler	used for debug/warning/error messages

Definition at line 145 of file dfcc.cpp.