Class interface to library types and functions defined in cprover_contracts.c. More...

#include <dfcc_library.h>

Collaboration diagram for dfcc_libraryt:

Public Member Functions
	dfcc_libraryt (goto_modelt &goto_model, message_handlert &lmessage_handler)
	Class constructor. More...

void	load (std::set< irep_idt > &to_instrument)
	After calling this function, all library types and functions are present in the the goto_model. More...

std::optional< dfcc_funt >	get_dfcc_fun (const irep_idt &id) const
	Returns the dfcc_funt that corresponds to the given id if any. More...

const irep_idt &	get_dfcc_fun_name (dfcc_funt fun) const
	Returns the name of the given dfcc_funt. More...

bool	is_dfcc_library_symbol (const irep_idt &id) const
	True iff the given id is one of the library symbols. More...

void	specialize (const std::size_t contract_assigns_size_hint)
	Specializes the library by unwinding loops in library functions to the given assigns clause size. More...

void	inhibit_front_end_builtins ()
	Adds an ASSERT(false) body to all front-end functions __CPROVER_object_whole __CPROVER_object_upto __CPROVER_object_from __CPROVER_assignable __CPROVER_freeable An error will be triggered in case calls to these functions occur outside of a contrat clause and were hence not mapped to their library implementation. More...

void	disable_checks ()
	Adds "checked" pragmas to instructions of all library functions instructions. More...

bool	is_front_end_builtin (const irep_idt &function_id) const
	Returns true iff the given function_id is one of `__CPROVER_assignable`, `__CPROVER_object_whole`, `__CPROVER_object_from`, `__CPROVER_object_upto`, `__CPROVER_freeable` More...

dfcc_funt	get_hook (const irep_idt &function_id) const
	Returns the library instrumentation hook for the given front-end function. More...

std::optional< dfcc_funt >	get_havoc_hook (const irep_idt &function_id) const
	Returns the library instrumentation hook for the given built-in. More...

const symbolt &	get_instrumented_functions_map_symbol ()
	Returns the "__dfcc_instrumented_functions" symbol or creates it if it does not exist already. More...

void	add_instrumented_functions_map_init_instructions (const std::set< irep_idt > &instrumented_functions, const source_locationt &source_location, goto_programt &dest)
	Generates instructions to initialize the instrumented function map symbol from the given set of instrumented function. More...

const code_function_callt	write_set_create_call (const exprt &write_set_ptr, const exprt &contract_assigns_size, const exprt &contract_frees_size, const exprt &assume_requires_ctx, const exprt &assert_requires_ctx, const exprt &assume_ensures_ctx, const exprt &assert_ensures_ctx, const exprt &allow_allocate, const exprt &allow_deallocate, const source_locationt &source_location)
	Builds call to __CPROVER_contracts_write_set_create. More...

const code_function_callt	write_set_create_call (const exprt &write_set_ptr, const exprt &contract_assigns_size, const source_locationt &source_location)
	Builds call to __CPROVER_contracts_write_set_create. More...

const code_function_callt	write_set_release_call (const exprt &write_set_ptr, const source_locationt &source_location)
	Builds call to __CPROVER_contracts_write_set_release. More...

const code_function_callt	write_set_add_allocated_call (const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
	Builds call to __CPROVER_contracts_write_set_add_allocated. More...

const code_function_callt	write_set_add_decl_call (const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
	Builds call to __CPROVER_contracts_write_set_add_decl. More...

const code_function_callt	write_set_record_dead_call (const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
	Builds call to __CPROVER_contracts_write_set_record_dead. More...

const code_function_callt	write_set_record_deallocated_call (const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
	Builds call to __CPROVER_contracts_write_set_record_deallocated. More...

const code_function_callt	write_set_check_allocated_deallocated_is_empty_call (const exprt &check_var, const exprt &write_set_ptr, const source_locationt &source_location)
	Builds call to __CPROVER_contracts_write_set_check_allocated_deallocated_is_empty. More...

const code_function_callt	write_set_check_assignment_call (const exprt &check_var, const exprt &write_set_ptr, const exprt &ptr, const exprt &size, const source_locationt &source_location)
	Builds call to __CPROVER_contracts_write_set_check_assignment. More...

const code_function_callt	write_set_check_array_set_call (const exprt &check_var, const exprt &write_set_ptr, const exprt &dest, const source_locationt &source_location)
	Builds call to __CPROVER_contracts_write_set_check_array_set. More...

const code_function_callt	write_set_check_array_copy_call (const exprt &check_var, const exprt &write_set_ptr, const exprt &dest, const source_locationt &source_location)
	Builds call to __CPROVER_contracts_write_set_check_array_copy. More...

const code_function_callt	write_set_check_array_replace_call (const exprt &check_var, const exprt &write_set_ptr, const exprt &dest, const exprt &src, const source_locationt &source_location)
	Builds call to __CPROVER_contracts_write_set_check_array_replace. More...

const code_function_callt	write_set_check_havoc_object_call (const exprt &check_var, const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
	Builds call to __CPROVER_contracts_write_set_check_havoc_object. More...

const code_function_callt	write_set_check_deallocate_call (const exprt &check_var, const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
	Builds call to __CPROVER_contracts_write_set_check_deallocate. More...

const code_function_callt	write_set_check_assigns_clause_inclusion_call (const exprt &check_var, const exprt &reference_write_set_ptr, const exprt &candidate_write_set_ptr, const source_locationt &source_location)
	Builds call to __CPROVER_contracts_write_set_check_assigns_clause_inclusion. More...

const code_function_callt	write_set_check_frees_clause_inclusion_call (const exprt &check_var, const exprt &reference_write_set_ptr, const exprt &candidate_write_set_ptr, const source_locationt &source_location)
	Builds call to __CPROVER_contracts_write_set_check_frees_clause_inclusion. More...

const code_function_callt	write_set_deallocate_freeable_call (const exprt &write_set_ptr, const exprt &target_write_set_ptr, const source_locationt &source_location)
	Builds call to __CPROVER_contracts_write_set_deallocate_freeable. More...

const code_function_callt	link_is_fresh_call (const exprt &write_set_ptr, const exprt &is_fresh_obj_set_ptr, const source_locationt &source_location)
	Builds call to __CPROVER_contracts_link_is_fresh. More...

const code_function_callt	link_allocated_call (const exprt &write_set_postconditions_ptr, const exprt &write_set_to_link_ptr, const source_locationt &source_location)
	Builds call to __CPROVER_contracts_link_allocated. More...

const code_function_callt	link_deallocated_call (const exprt &write_set_postconditions_ptr, const exprt &write_set_to_link_ptr, const source_locationt &source_location)
	Builds call to __CPROVER_contracts_link_deallocated. More...

const code_function_callt	check_replace_ensures_was_freed_preconditions_call (const exprt &ptr, const exprt &write_set_ptr, const source_locationt &source_location)
	Builds call to __CPROVER_contracts_check_replace_ensures_was_freed_preconditions. More...

const code_function_callt	obj_set_create_indexed_by_object_id_call (const exprt &obj_set_ptr, const source_locationt &source_location)
	Builds call to __CPROVER_contracts_obj_set_create_indexed_by_object_id. More...

const code_function_callt	obj_set_release_call (const exprt &obj_set_ptr, const source_locationt &source_location)
	Builds call to __CPROVER_contracts_obj_set_release. More...

Public Attributes
std::map< dfcc_typet, typet >	dfcc_type
	Maps enum values to the actual types (dynamically loaded) More...

std::map< dfcc_funt, symbolt >	dfcc_fun_symbol
	Maps enum values to the actual function symbols (dynamically loaded) More...

Protected Member Functions
std::set< irep_idt >	get_missing_funs ()
	Collects the names of all library functions currently missing from the goto_model into `missing`. More...

void	inline_functions ()
	Inlines library functions that need to be inlined before use. More...

void	fix_malloc_free_calls ()
	Fixes function calls to malloc and free in library functions. More...

Protected Attributes
goto_modelt &	goto_model

message_handlert &	message_handler

messaget	log

Static Protected Attributes
static bool	loaded = false
	True iff the contracts library symbols are loaded. More...

static bool	inlined = false
	True iff the library functions are inlined. More...

static bool	specialized = false
	True iff the library functions are specialized to a particular contract. More...

static bool	malloc_free_fixed = false
	True iff the library functions uses of malloc and free are fixed. More...

Private Attributes
const std::map< dfcc_typet, irep_idt >	dfcc_type_to_name
	Enum to type name mapping. More...

const std::map< irep_idt, dfcc_typet >	dfcc_name_to_type
	Swapped dfcc_type_to_name. More...

const std::map< dfcc_funt, irep_idt >	dfcc_fun_to_name
	enum to function name mapping More...

const std::map< irep_idt, dfcc_funt >	dfcc_name_to_fun

const std::map< irep_idt, dfcc_funt >	dfcc_hook
	Maps built-in function names to enums to use for instrumentation. More...

const std::map< irep_idt, dfcc_funt >	havoc_hook
	Maps front-end functions to library functions giving their havoc semantics. More...

const std::set< irep_idt >	assignable_builtin_names
	All built-in function names (front-end and instrumentation hooks) More...

Detailed Description

Class interface to library types and functions defined in cprover_contracts.c.

Definition at line 153 of file dfcc_library.h.

Constructor & Destructor Documentation

◆ dfcc_libraryt()

dfcc_libraryt::dfcc_libraryt	(	goto_modelt &	goto_model,
		message_handlert &	lmessage_handler
	)

Class constructor.

Definition at line 174 of file dfcc_library.cpp.

Member Function Documentation

◆ add_instrumented_functions_map_init_instructions()

void dfcc_libraryt::add_instrumented_functions_map_init_instructions	(	const std::set< irep_idt > &	instrumented_functions,
		const source_locationt &	source_location,
		goto_programt &	dest
	)

Generates instructions to initialize the instrumented function map symbol from the given set of instrumented function.

Definition at line 537 of file dfcc_library.cpp.

◆ check_replace_ensures_was_freed_preconditions_call()

const code_function_callt dfcc_libraryt::check_replace_ensures_was_freed_preconditions_call	(	const exprt &	ptr,
		const exprt &	write_set_ptr,
		const source_locationt &	source_location
	)

Builds call to __CPROVER_contracts_check_replace_ensures_was_freed_preconditions.

Definition at line 848 of file dfcc_library.cpp.

◆ disable_checks()

void dfcc_libraryt::disable_checks ( )

Adds "checked" pragmas to instructions of all library functions instructions.

By default checks are not disabled.

Definition at line 227 of file dfcc_library.cpp.

◆ fix_malloc_free_calls()

void dfcc_libraryt::fix_malloc_free_calls ( )

protected

Fixes function calls to malloc and free in library functions.

Change calls to __CPROVER_contracts_malloc into calls to malloc Change calls to __CPROVER_contracts_free into calls to free

Definition at line 463 of file dfcc_library.cpp.

◆ get_dfcc_fun()

std::optional< dfcc_funt > dfcc_libraryt::get_dfcc_fun ( const irep_idt & id ) const

Returns the dfcc_funt that corresponds to the given id if any.

Definition at line 365 of file dfcc_library.cpp.

◆ get_dfcc_fun_name()

const irep_idt & dfcc_libraryt::get_dfcc_fun_name ( dfcc_funt fun ) const

Returns the name of the given dfcc_funt.

Definition at line 379 of file dfcc_library.cpp.

◆ get_havoc_hook()

std::optional< dfcc_funt > dfcc_libraryt::get_havoc_hook ( const irep_idt & function_id ) const

Returns the library instrumentation hook for the given built-in.

function_id must be one of __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_from, __CPROVER_object_upto

Definition at line 207 of file dfcc_library.cpp.

◆ get_hook()

dfcc_funt dfcc_libraryt::get_hook ( const irep_idt & function_id ) const

Returns the library instrumentation hook for the given front-end function.

Returns the instrumentation function to use for a given front-end function.

Precondition: function_id is a front end built-in as defined by is_front_end_builtin.

Definition at line 199 of file dfcc_library.cpp.

◆ get_instrumented_functions_map_symbol()

const symbolt & dfcc_libraryt::get_instrumented_functions_map_symbol ( )

Returns the "__dfcc_instrumented_functions" symbol or creates it if it does not exist already.

This symbol is an unbounded map of booleans indexed by function pointer ID, meant to have value true for instrumented functions and false for non-instrumented functions. Initialisation instructions for this map are generated by add_instrumented_functions_map_init_instructions

Definition at line 515 of file dfcc_library.cpp.

◆ get_missing_funs()

std::set< irep_idt > dfcc_libraryt::get_missing_funs ( )

protected

Collects the names of all library functions currently missing from the goto_model into missing.

Definition at line 239 of file dfcc_library.cpp.

◆ inhibit_front_end_builtins()

void dfcc_libraryt::inhibit_front_end_builtins ( )

Adds an ASSERT(false) body to all front-end functions __CPROVER_object_whole __CPROVER_object_upto __CPROVER_object_from __CPROVER_assignable __CPROVER_freeable An error will be triggered in case calls to these functions occur outside of a contrat clause and were hence not mapped to their library implementation.

Definition at line 494 of file dfcc_library.cpp.

◆ inline_functions()

void dfcc_libraryt::inline_functions ( )

protected

Inlines library functions that need to be inlined before use.

Definition at line 406 of file dfcc_library.cpp.

◆ is_dfcc_library_symbol()

bool dfcc_libraryt::is_dfcc_library_symbol ( const irep_idt & id ) const

True iff the given id is one of the library symbols.

Definition at line 374 of file dfcc_library.cpp.

◆ is_front_end_builtin()

bool dfcc_libraryt::is_front_end_builtin ( const irep_idt & function_id ) const

Returns true iff the given function_id is one of __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_from, __CPROVER_object_upto, __CPROVER_freeable

Returns the instrumentation function to use for a given front-end function.

Definition at line 193 of file dfcc_library.cpp.

◆ link_allocated_call()

const code_function_callt dfcc_libraryt::link_allocated_call	(	const exprt &	write_set_postconditions_ptr,
		const exprt &	write_set_to_link_ptr,
		const source_locationt &	source_location
	)

Builds call to __CPROVER_contracts_link_allocated.

Definition at line 823 of file dfcc_library.cpp.

◆ link_deallocated_call()

const code_function_callt dfcc_libraryt::link_deallocated_call	(	const exprt &	write_set_postconditions_ptr,
		const exprt &	write_set_to_link_ptr,
		const source_locationt &	source_location
	)

Builds call to __CPROVER_contracts_link_deallocated.

Definition at line 835 of file dfcc_library.cpp.

◆ link_is_fresh_call()

const code_function_callt dfcc_libraryt::link_is_fresh_call	(	const exprt &	write_set_ptr,
		const exprt &	is_fresh_obj_set_ptr,
		const source_locationt &	source_location
	)

Builds call to __CPROVER_contracts_link_is_fresh.

Definition at line 811 of file dfcc_library.cpp.

◆ load()

void dfcc_libraryt::load ( std::set< irep_idt > & to_instrument )

After calling this function, all library types and functions are present in the the goto_model.

Any other functions that the DFCC functions rely on and need to be instrumented will be added to to_instrument

Definition at line 278 of file dfcc_library.cpp.

◆ obj_set_create_indexed_by_object_id_call()

const code_function_callt dfcc_libraryt::obj_set_create_indexed_by_object_id_call	(	const exprt &	obj_set_ptr,
		const source_locationt &	source_location
	)

Builds call to __CPROVER_contracts_obj_set_create_indexed_by_object_id.

Definition at line 862 of file dfcc_library.cpp.

◆ obj_set_release_call()

const code_function_callt dfcc_libraryt::obj_set_release_call	(	const exprt &	obj_set_ptr,
		const source_locationt &	source_location
	)

Builds call to __CPROVER_contracts_obj_set_release.

Definition at line 874 of file dfcc_library.cpp.

◆ specialize()

void dfcc_libraryt::specialize ( const std::size_t contract_assigns_size_hint )

Specializes the library by unwinding loops in library functions to the given assigns clause size.

Parameters

contract_assigns_size_hint size of the assigns clause being checked

Definition at line 429 of file dfcc_library.cpp.

◆ write_set_add_allocated_call()

const code_function_callt dfcc_libraryt::write_set_add_allocated_call	(	const exprt &	write_set_ptr,
		const exprt &	ptr,
		const source_locationt &	source_location
	)

Builds call to __CPROVER_contracts_write_set_add_allocated.

Definition at line 618 of file dfcc_library.cpp.

◆ write_set_add_decl_call()

const code_function_callt dfcc_libraryt::write_set_add_decl_call	(	const exprt &	write_set_ptr,
		const exprt &	ptr,
		const source_locationt &	source_location
	)

Builds call to __CPROVER_contracts_write_set_add_decl.

Definition at line 630 of file dfcc_library.cpp.

◆ write_set_check_allocated_deallocated_is_empty_call()

const code_function_callt dfcc_libraryt::write_set_check_allocated_deallocated_is_empty_call	(	const exprt &	check_var,
		const exprt &	write_set_ptr,
		const source_locationt &	source_location
	)

Builds call to __CPROVER_contracts_write_set_check_allocated_deallocated_is_empty.

Definition at line 667 of file dfcc_library.cpp.

◆ write_set_check_array_copy_call()

const code_function_callt dfcc_libraryt::write_set_check_array_copy_call	(	const exprt &	check_var,
		const exprt &	write_set_ptr,
		const exprt &	dest,
		const source_locationt &	source_location
	)

Builds call to __CPROVER_contracts_write_set_check_array_copy.

Definition at line 710 of file dfcc_library.cpp.

◆ write_set_check_array_replace_call()

const code_function_callt dfcc_libraryt::write_set_check_array_replace_call	(	const exprt &	check_var,
		const exprt &	write_set_ptr,
		const exprt &	dest,
		const exprt &	src,
		const source_locationt &	source_location
	)

Builds call to __CPROVER_contracts_write_set_check_array_replace.

Definition at line 724 of file dfcc_library.cpp.

◆ write_set_check_array_set_call()

const code_function_callt dfcc_libraryt::write_set_check_array_set_call	(	const exprt &	check_var,
		const exprt &	write_set_ptr,
		const exprt &	dest,
		const source_locationt &	source_location
	)

Builds call to __CPROVER_contracts_write_set_check_array_set.

Definition at line 696 of file dfcc_library.cpp.

◆ write_set_check_assignment_call()

const code_function_callt dfcc_libraryt::write_set_check_assignment_call	(	const exprt &	check_var,
		const exprt &	write_set_ptr,
		const exprt &	ptr,
		const exprt &	size,
		const source_locationt &	source_location
	)

Builds call to __CPROVER_contracts_write_set_check_assignment.

Definition at line 681 of file dfcc_library.cpp.

◆ write_set_check_assigns_clause_inclusion_call()

const code_function_callt dfcc_libraryt::write_set_check_assigns_clause_inclusion_call	(	const exprt &	check_var,
		const exprt &	reference_write_set_ptr,
		const exprt &	candidate_write_set_ptr,
		const source_locationt &	source_location
	)

Builds call to __CPROVER_contracts_write_set_check_assigns_clause_inclusion.

Definition at line 768 of file dfcc_library.cpp.

◆ write_set_check_deallocate_call()

const code_function_callt dfcc_libraryt::write_set_check_deallocate_call	(	const exprt &	check_var,
		const exprt &	write_set_ptr,
		const exprt &	ptr,
		const source_locationt &	source_location
	)

Builds call to __CPROVER_contracts_write_set_check_deallocate.

Definition at line 753 of file dfcc_library.cpp.

◆ write_set_check_frees_clause_inclusion_call()

const code_function_callt dfcc_libraryt::write_set_check_frees_clause_inclusion_call	(	const exprt &	check_var,
		const exprt &	reference_write_set_ptr,
		const exprt &	candidate_write_set_ptr,
		const source_locationt &	source_location
	)

Builds call to __CPROVER_contracts_write_set_check_frees_clause_inclusion.

Definition at line 784 of file dfcc_library.cpp.

◆ write_set_check_havoc_object_call()

const code_function_callt dfcc_libraryt::write_set_check_havoc_object_call	(	const exprt &	check_var,
		const exprt &	write_set_ptr,
		const exprt &	ptr,
		const source_locationt &	source_location
	)

Builds call to __CPROVER_contracts_write_set_check_havoc_object.

Definition at line 739 of file dfcc_library.cpp.

◆ write_set_create_call() [1/2]

const code_function_callt dfcc_libraryt::write_set_create_call	(	const exprt &	write_set_ptr,
		const exprt &	contract_assigns_size,
		const exprt &	contract_frees_size,
		const exprt &	assume_requires_ctx,
		const exprt &	assert_requires_ctx,
		const exprt &	assume_ensures_ctx,
		const exprt &	assert_ensures_ctx,
		const exprt &	allow_allocate,
		const exprt &	allow_deallocate,
		const source_locationt &	source_location
	)

Builds call to __CPROVER_contracts_write_set_create.

Definition at line 557 of file dfcc_library.cpp.

◆ write_set_create_call() [2/2]

const code_function_callt dfcc_libraryt::write_set_create_call	(	const exprt &	write_set_ptr,
		const exprt &	contract_assigns_size,
		const source_locationt &	source_location
	)

Builds call to __CPROVER_contracts_write_set_create.

Definition at line 589 of file dfcc_library.cpp.

◆ write_set_deallocate_freeable_call()

const code_function_callt dfcc_libraryt::write_set_deallocate_freeable_call	(	const exprt &	write_set_ptr,
		const exprt &	target_write_set_ptr,
		const source_locationt &	source_location
	)

Builds call to __CPROVER_contracts_write_set_deallocate_freeable.

Definition at line 799 of file dfcc_library.cpp.

◆ write_set_record_dead_call()

const code_function_callt dfcc_libraryt::write_set_record_dead_call	(	const exprt &	write_set_ptr,
		const exprt &	ptr,
		const source_locationt &	source_location
	)

Builds call to __CPROVER_contracts_write_set_record_dead.

Definition at line 642 of file dfcc_library.cpp.

◆ write_set_record_deallocated_call()

const code_function_callt dfcc_libraryt::write_set_record_deallocated_call	(	const exprt &	write_set_ptr,
		const exprt &	ptr,
		const source_locationt &	source_location
	)

Builds call to __CPROVER_contracts_write_set_record_deallocated.

Definition at line 654 of file dfcc_library.cpp.

◆ write_set_release_call()

const code_function_callt dfcc_libraryt::write_set_release_call	(	const exprt &	write_set_ptr,
		const source_locationt &	source_location
	)

Builds call to __CPROVER_contracts_write_set_release.

Definition at line 607 of file dfcc_library.cpp.

Member Data Documentation

◆ assignable_builtin_names

const std::set<irep_idt> dfcc_libraryt::assignable_builtin_names

private

All built-in function names (front-end and instrumentation hooks)

Definition at line 210 of file dfcc_library.h.

◆ dfcc_fun_symbol

std::map<dfcc_funt, symbolt> dfcc_libraryt::dfcc_fun_symbol

Maps enum values to the actual function symbols (dynamically loaded)

Definition at line 217 of file dfcc_library.h.

◆ dfcc_fun_to_name

const std::map<dfcc_funt, irep_idt> dfcc_libraryt::dfcc_fun_to_name

private

enum to function name mapping

Definition at line 198 of file dfcc_library.h.

◆ dfcc_hook

const std::map<irep_idt, dfcc_funt> dfcc_libraryt::dfcc_hook

private

Maps built-in function names to enums to use for instrumentation.

Definition at line 204 of file dfcc_library.h.

◆ dfcc_name_to_fun

const std::map<irep_idt, dfcc_funt> dfcc_libraryt::dfcc_name_to_fun

private

Definition at line 201 of file dfcc_library.h.

◆ dfcc_name_to_type

const std::map<irep_idt, dfcc_typet> dfcc_libraryt::dfcc_name_to_type

private

Swapped dfcc_type_to_name.

Definition at line 195 of file dfcc_library.h.

◆ dfcc_type

std::map<dfcc_typet, typet> dfcc_libraryt::dfcc_type

Maps enum values to the actual types (dynamically loaded)

Definition at line 214 of file dfcc_library.h.

◆ dfcc_type_to_name

const std::map<dfcc_typet, irep_idt> dfcc_libraryt::dfcc_type_to_name

private

Enum to type name mapping.

Definition at line 192 of file dfcc_library.h.

◆ goto_model

goto_modelt& dfcc_libraryt::goto_model

protected

Definition at line 174 of file dfcc_library.h.

◆ havoc_hook

const std::map<irep_idt, dfcc_funt> dfcc_libraryt::havoc_hook

private

Maps front-end functions to library functions giving their havoc semantics.

Definition at line 207 of file dfcc_library.h.

◆ inlined

bool dfcc_libraryt::inlined = false

staticprotected

True iff the library functions are inlined.

Definition at line 165 of file dfcc_library.h.

◆ loaded

bool dfcc_libraryt::loaded = false

staticprotected

True iff the contracts library symbols are loaded.

Definition at line 162 of file dfcc_library.h.

◆ log

messaget dfcc_libraryt::log

protected

Definition at line 176 of file dfcc_library.h.

◆ malloc_free_fixed

bool dfcc_libraryt::malloc_free_fixed = false

staticprotected

True iff the library functions uses of malloc and free are fixed.

True iff the library functions have already been fixed.

Definition at line 172 of file dfcc_library.h.

◆ message_handler

message_handlert& dfcc_libraryt::message_handler

protected

Definition at line 175 of file dfcc_library.h.

◆ specialized

bool dfcc_libraryt::specialized = false

staticprotected

True iff the library functions are specialized to a particular contract.

Definition at line 169 of file dfcc_library.h.

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

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

Public Member Functions

Public Attributes

Protected Member Functions

Protected Attributes

Static Protected Attributes

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ dfcc_libraryt()

Member Function Documentation

◆ add_instrumented_functions_map_init_instructions()

◆ check_replace_ensures_was_freed_preconditions_call()

◆ disable_checks()

◆ fix_malloc_free_calls()

◆ get_dfcc_fun()

◆ get_dfcc_fun_name()

◆ get_havoc_hook()

◆ get_hook()

◆ get_instrumented_functions_map_symbol()

◆ get_missing_funs()

◆ inhibit_front_end_builtins()

◆ inline_functions()

◆ is_dfcc_library_symbol()

◆ is_front_end_builtin()

◆ link_allocated_call()

◆ link_deallocated_call()

◆ link_is_fresh_call()

◆ load()

◆ obj_set_create_indexed_by_object_id_call()

◆ obj_set_release_call()

◆ specialize()

◆ write_set_add_allocated_call()

◆ write_set_add_decl_call()

◆ write_set_check_allocated_deallocated_is_empty_call()

◆ write_set_check_array_copy_call()

◆ write_set_check_array_replace_call()

◆ write_set_check_array_set_call()

◆ write_set_check_assignment_call()

◆ write_set_check_assigns_clause_inclusion_call()

◆ write_set_check_deallocate_call()

◆ write_set_check_frees_clause_inclusion_call()

◆ write_set_check_havoc_object_call()

◆ write_set_create_call() [1/2]

◆ write_set_create_call() [2/2]

◆ write_set_deallocate_freeable_call()

◆ write_set_record_dead_call()

◆ write_set_record_deallocated_call()

◆ write_set_release_call()

Member Data Documentation

◆ assignable_builtin_names

◆ dfcc_fun_symbol

◆ dfcc_fun_to_name

◆ dfcc_hook

◆ dfcc_name_to_fun

◆ dfcc_name_to_type

◆ dfcc_type

◆ dfcc_type_to_name

◆ goto_model

◆ havoc_hook

◆ inlined

◆ loaded

◆ log

◆ malloc_free_fixed

◆ message_handler

◆ specialized