Generates GOTO functions modelling a contract assigns and frees clauses. More...

#include <dfcc_contract_functions.h>

Collaboration diagram for dfcc_contract_functionst:

Public Member Functions
	dfcc_contract_functionst (const symbolt &pure_contract_symbol, goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen, dfcc_instrumentt &instrument)

void	instrument_without_loop_contracts_check_no_pointer_contracts (const irep_idt &spec_function_id)
	Instruments the given function without loop contracts and checks that no function pointer contracts were discovered. More...

const symbolt &	get_spec_assigns_function_symbol () const
	Returns the contract::c_assigns function symbol. More...

const symbolt &	get_spec_assigns_havoc_function_symbol () const
	Returns the contract::c_assigns::havoc function symbol. More...

const symbolt &	get_spec_frees_function_symbol () const
	Returns the contract::frees function symbol. More...

const std::size_t	get_nof_assigns_targets () const
	Returns the maximum number of targets in the assigns clause. More...

const std::size_t	get_nof_frees_targets () const
	Returns the maximum number of targets in the frees clause. More...

Public Attributes
const symbolt &	pure_contract_symbol
	The function symbol carrying the contract. More...

const code_with_contract_typet &	code_with_contract
	The code_with_contract_type carrying the contract clauses. More...

const irep_idt	spec_assigns_function_id
	Identifier of the contract::c_assigns function. More...

const irep_idt	spec_assigns_havoc_function_id
	Identifier of the contract::c_assigns::havoc function. More...

const irep_idt	spec_frees_function_id
	Identifier of the contract::frees function. More...

const irep_idt &	language_mode
	Language mode of the contract symbol. More...

Protected Member Functions
void	gen_spec_assigns_function ()
	Translates the contract's assigns clause to a GOTO function that uses the `assignable`, `object_upto`, `object_from`, object_whole` built-ins to express targets. More...

void	gen_spec_frees_function ()
	Translates the contract's frees clause to a GOTO function that uses the `freeable` built-in to express targets. More...

Protected Attributes
goto_modelt &	goto_model

message_handlert &	message_handler

messaget	log

dfcc_libraryt &	library

dfcc_spec_functionst &	spec_functions

dfcc_contract_clauses_codegent &	contract_clauses_codegen

dfcc_instrumentt &	instrument

namespacet	ns

std::size_t	nof_assigns_targets

std::size_t	nof_frees_targets

Detailed Description

Generates GOTO functions modelling a contract assigns and frees clauses.

The generated functions are the following:

// Populates write_set_to_fill with targets of the assigns clause
// checks its own body against write_set_to_check:
void contract_id::c_assigns(
    function-params,
    write_set_to_fill,
    write_set_to_check);

// Havocs the targets specified in the assigns clause, assuming
// write_set_to_havoc is a snapshot created using contract_id::c_assigns
void contract_id::c_assigns::havoc(write_set_to_havoc);

// Populates write_set_to_fill with targets of the frees clause
// checks its own body against write_set_to_check:
void contract_id::frees(
    function-params,
    write_set_to_fill,
    write_set_to_check);

Definition at line 63 of file dfcc_contract_functions.h.

Constructor & Destructor Documentation

◆ dfcc_contract_functionst()

dfcc_contract_functionst::dfcc_contract_functionst	(	const symbolt &	pure_contract_symbol,
		goto_modelt &	goto_model,
		message_handlert &	message_handler,
		dfcc_libraryt &	library,
		dfcc_spec_functionst &	spec_functions,
		dfcc_contract_clauses_codegent &	contract_clauses_codegen,
		dfcc_instrumentt &	instrument
	)

Parameters

pure_contract_symbol	the contract to generate code from
goto_model	goto model being transformed
message_handler	used debug/warning/error messages
library	the contracts instrumentation library
spec_functions	provides translation methods for assignable set
contract_clauses_codegen	provides GOTO code generation methods for assigns and free clauses.
instrument	Used to instrument generated functions for side effects

Definition at line 30 of file dfcc_contract_functions.cpp.

Member Function Documentation

◆ gen_spec_assigns_function()

void dfcc_contract_functionst::gen_spec_assigns_function ( )

protected

Translates the contract's assigns clause to a GOTO function that uses the assignable, object_upto, object_from, object_whole` built-ins to express targets.

Definition at line 118 of file dfcc_contract_functions.cpp.

◆ gen_spec_frees_function()

void dfcc_contract_functionst::gen_spec_frees_function ( )

protected

Translates the contract's frees clause to a GOTO function that uses the freeable built-in to express targets.

Definition at line 166 of file dfcc_contract_functions.cpp.

◆ get_nof_assigns_targets()

const std::size_t dfcc_contract_functionst::get_nof_assigns_targets ( ) const

Returns the maximum number of targets in the assigns clause.

Definition at line 108 of file dfcc_contract_functions.cpp.

◆ get_nof_frees_targets()

const std::size_t dfcc_contract_functionst::get_nof_frees_targets ( ) const

Returns the maximum number of targets in the frees clause.

Definition at line 113 of file dfcc_contract_functions.cpp.

◆ get_spec_assigns_function_symbol()

const symbolt & dfcc_contract_functionst::get_spec_assigns_function_symbol ( ) const

Returns the contract::c_assigns function symbol.

Definition at line 92 of file dfcc_contract_functions.cpp.

◆ get_spec_assigns_havoc_function_symbol()

const symbolt & dfcc_contract_functionst::get_spec_assigns_havoc_function_symbol ( ) const

Returns the contract::c_assigns::havoc function symbol.

Definition at line 98 of file dfcc_contract_functions.cpp.

◆ get_spec_frees_function_symbol()

const symbolt & dfcc_contract_functionst::get_spec_frees_function_symbol ( ) const

Returns the contract::frees function symbol.

Definition at line 103 of file dfcc_contract_functions.cpp.

◆ instrument_without_loop_contracts_check_no_pointer_contracts()

void dfcc_contract_functionst::instrument_without_loop_contracts_check_no_pointer_contracts ( const irep_idt & spec_function_id )

Instruments the given function without loop contracts and checks that no function pointer contracts were discovered.

Definition at line 77 of file dfcc_contract_functions.cpp.

Member Data Documentation

◆ code_with_contract

const code_with_contract_typet& dfcc_contract_functionst::code_with_contract

The code_with_contract_type carrying the contract clauses.

Definition at line 107 of file dfcc_contract_functions.h.

◆ contract_clauses_codegen

dfcc_contract_clauses_codegent& dfcc_contract_functionst::contract_clauses_codegen

protected

Definition at line 127 of file dfcc_contract_functions.h.

◆ goto_model

goto_modelt& dfcc_contract_functionst::goto_model

protected

Definition at line 122 of file dfcc_contract_functions.h.

◆ instrument

dfcc_instrumentt& dfcc_contract_functionst::instrument

protected

Definition at line 128 of file dfcc_contract_functions.h.

◆ language_mode

const irep_idt& dfcc_contract_functionst::language_mode

Language mode of the contract symbol.

Definition at line 119 of file dfcc_contract_functions.h.

◆ library

dfcc_libraryt& dfcc_contract_functionst::library

protected

Definition at line 125 of file dfcc_contract_functions.h.

◆ log

messaget dfcc_contract_functionst::log

protected

Definition at line 124 of file dfcc_contract_functions.h.

◆ message_handler

message_handlert& dfcc_contract_functionst::message_handler

protected

Definition at line 123 of file dfcc_contract_functions.h.

◆ nof_assigns_targets

std::size_t dfcc_contract_functionst::nof_assigns_targets

protected

Definition at line 130 of file dfcc_contract_functions.h.

◆ nof_frees_targets

std::size_t dfcc_contract_functionst::nof_frees_targets

protected

Definition at line 131 of file dfcc_contract_functions.h.

◆ ns

namespacet dfcc_contract_functionst::ns

protected

Definition at line 129 of file dfcc_contract_functions.h.

◆ pure_contract_symbol

const symbolt& dfcc_contract_functionst::pure_contract_symbol

The function symbol carrying the contract.

Definition at line 104 of file dfcc_contract_functions.h.

◆ spec_assigns_function_id

const irep_idt dfcc_contract_functionst::spec_assigns_function_id

Identifier of the contract::c_assigns function.

Definition at line 110 of file dfcc_contract_functions.h.

◆ spec_assigns_havoc_function_id

const irep_idt dfcc_contract_functionst::spec_assigns_havoc_function_id

Identifier of the contract::c_assigns::havoc function.

Definition at line 113 of file dfcc_contract_functions.h.

◆ spec_frees_function_id

const irep_idt dfcc_contract_functionst::spec_frees_function_id

Identifier of the contract::frees function.

Definition at line 116 of file dfcc_contract_functions.h.

◆ spec_functions

dfcc_spec_functionst& dfcc_contract_functionst::spec_functions

protected

Definition at line 126 of file dfcc_contract_functions.h.

The documentation for this class was generated from the following files:

/home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h
/home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp

Public Member Functions

Public Attributes

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ dfcc_contract_functionst()

Member Function Documentation

◆ gen_spec_assigns_function()

◆ gen_spec_frees_function()

◆ get_nof_assigns_targets()

◆ get_nof_frees_targets()

◆ get_spec_assigns_function_symbol()

◆ get_spec_assigns_havoc_function_symbol()

◆ get_spec_frees_function_symbol()

◆ instrument_without_loop_contracts_check_no_pointer_contracts()

Member Data Documentation

◆ code_with_contract

◆ contract_clauses_codegen

◆ goto_model

◆ instrument

◆ language_mode

◆ library

◆ log

◆ message_handler

◆ nof_assigns_targets

◆ nof_frees_targets

◆ ns

◆ pure_contract_symbol

◆ spec_assigns_function_id

◆ spec_assigns_havoc_function_id

◆ spec_frees_function_id

◆ spec_functions