Types and functions for dynamic frames instrumentation in contracts. More...

Classes
struct	__CPROVER_contracts_car_t
	A conditionally writable range of bytes. More...

struct	__CPROVER_contracts_car_set_t
	A set of __CPROVER_contracts_car_t. More...

struct	__CPROVER_contracts_obj_set_t
	A set of pointers. More...

struct	__CPROVER_contracts_ptr_pred_ctx_t
	Stores context information supporting the evaluation of pointer predicates in both assume and assert contexts for all predicates: pointer equals, pointer_in_range_dfcc, pointer_is_fresh, obeys_contract. More...

struct	__CPROVER_contracts_write_set_t
	Runtime representation of a write set. More...

Macros
#define	__CPROVER_contracts_library_defined

Typedefs
typedef __CPROVER_contracts_car_set_t *	__CPROVER_contracts_car_set_ptr_t
	Type of pointers to __CPROVER_contracts_car_set_t.

typedef __CPROVER_contracts_obj_set_t *	__CPROVER_contracts_obj_set_ptr_t
	Type of pointers to __CPROVER_contracts_obj_set_t.

typedef __CPROVER_contracts_ptr_pred_ctx_t *	__CPROVER_contracts_ptr_pred_ctx_ptr_t
	Type of pointers to __CPROVER_contracts_ptr_pred_ctx_t.

typedef __CPROVER_contracts_write_set_t *	__CPROVER_contracts_write_set_ptr_t
	Type of pointers to __CPROVER_contracts_write_set_t.

Functions
int	__builtin_clzl (unsigned long)

__CPROVER_bool	__VERIFIER_nondet___CPROVER_bool (void)

__CPROVER_size_t	__VERIFIER_nondet_size (void)

__CPROVER_contracts_car_t	__CPROVER_contracts_car_create (void *ptr, __CPROVER_size_t size)
	Creates a __CPROVER_car_t struct from `ptr` and `size`.

void	__CPROVER_contracts_car_set_create (__CPROVER_contracts_car_set_ptr_t set, __CPROVER_size_t max_elems)
	Initialises a __CPROVER_contracts_car_set_ptr_t object.

void	__CPROVER_contracts_car_set_insert (__CPROVER_contracts_car_set_ptr_t set, __CPROVER_size_t idx, void *ptr, __CPROVER_size_t size)
	Inserts a __CPROVER_contracts_car_t snapshotted from `ptr` and `size` into `set` at index `idx`.

void	__CPROVER_contracts_car_set_remove (__CPROVER_contracts_car_set_ptr_t set, void *ptr)
	Invalidates all cars in the `set` that point into the same object as the given `ptr`.

__CPROVER_bool	__CPROVER_contracts_car_set_contains (__CPROVER_contracts_car_set_ptr_t set, __CPROVER_contracts_car_t candidate)
	Checks if `candidate` is included in one of `set` 's elements.

void	__CPROVER_contracts_obj_set_create_indexed_by_object_id (__CPROVER_contracts_obj_set_ptr_t set)
	Initialises a __CPROVER_contracts_obj_set_t object to use it in "indexed by object id" mode.

void	__CPROVER_contracts_obj_set_create_append (__CPROVER_contracts_obj_set_ptr_t set, __CPROVER_size_t max_elems)
	Initialises a __CPROVER_contracts_obj_set_t object to use it in "append" mode for at most `max_elems` elements.

void	__CPROVER_contracts_obj_set_release (__CPROVER_contracts_obj_set_ptr_t set)
	Releases resources used by `set`.

void	__CPROVER_contracts_obj_set_add (__CPROVER_contracts_obj_set_ptr_t set, void *ptr)
	Adds the `ptr` to `set`.

void	__CPROVER_contracts_obj_set_append (__CPROVER_contracts_obj_set_ptr_t set, void *ptr)
	Appends `ptr` to `set`.

void	__CPROVER_contracts_obj_set_remove (__CPROVER_contracts_obj_set_ptr_t set, void *ptr)
	Removes `ptr` form `set` if `ptr` exists in `set`, no-op otherwise.

__CPROVER_bool	__CPROVER_contracts_obj_set_contains (__CPROVER_contracts_obj_set_ptr_t set, void *ptr)
	Checks if a pointer with the same object id as `ptr` is contained in `set`.

__CPROVER_bool	__CPROVER_contracts_obj_set_contains_exact (__CPROVER_contracts_obj_set_ptr_t set, void *ptr)
	Checks if `ptr` is contained in `set`.

void	__CPROVER_contracts_ptr_pred_ctx_init (__CPROVER_contracts_ptr_pred_ctx_ptr_t set)
	Resets the nondet tracker for pointer predicates in `set`.

void	__CPROVER_contracts_ptr_pred_ctx_reset (__CPROVER_contracts_ptr_pred_ctx_ptr_t set)
	Resets the nondet tracker for pointer predicates in `set`.

void	__CPROVER_contracts_write_set_create (__CPROVER_contracts_write_set_ptr_t set, __CPROVER_size_t contract_assigns_size, __CPROVER_size_t contract_frees_size, __CPROVER_bool assume_requires_ctx, __CPROVER_bool assert_requires_ctx, __CPROVER_bool assume_ensures_ctx, __CPROVER_bool assert_ensures_ctx, __CPROVER_bool allow_allocate, __CPROVER_bool allow_deallocate)
	Initialises a __CPROVER_contracts_write_set_t object.

void	__CPROVER_contracts_write_set_release (__CPROVER_contracts_write_set_ptr_t set)
	Releases resources used by `set`.

void	__CPROVER_contracts_write_set_insert_assignable (__CPROVER_contracts_write_set_ptr_t set, __CPROVER_size_t idx, void *ptr, __CPROVER_size_t size)
	Inserts a snapshot of the range starting at `ptr` of size `size` at index `idx` in `set->contract_assigns`.

void	__CPROVER_contracts_write_set_insert_object_whole (__CPROVER_contracts_write_set_ptr_t set, __CPROVER_size_t idx, void *ptr)
	Inserts a snapshot of the range of bytes covering the whole object pointed to by `ptr` in `set->contact_assigns` at index `idx`.

void	__CPROVER_contracts_write_set_insert_object_from (__CPROVER_contracts_write_set_ptr_t set, __CPROVER_size_t idx, void *ptr)
	Inserts a snapshot of the range of bytes starting at `ptr` and extending to the end of the object in `set->contact_assigns` at index `idx`.

void	__CPROVER_contracts_write_set_insert_object_upto (__CPROVER_contracts_write_set_ptr_t set, __CPROVER_size_t idx, void *ptr, __CPROVER_size_t size)
	Inserts a snapshot of the range of bytes starting at `ptr` of `size` bytes in `set->contact_assigns` at index `idx`.

void	__CPROVER_contracts_write_set_add_freeable (__CPROVER_contracts_write_set_ptr_t set, void *ptr)
	Adds the freeable pointer `ptr` to `set->contract_frees`.

void	__CPROVER_contracts_write_set_add_allocated (__CPROVER_contracts_write_set_ptr_t set, void *ptr)
	Adds the dynamically allocated pointer `ptr` to `set->allocated`.

void	__CPROVER_contracts_write_set_add_decl (__CPROVER_contracts_write_set_ptr_t set, void *ptr)
	Adds the pointer `ptr` to `set->allocated`.

void	__CPROVER_contracts_write_set_record_dead (__CPROVER_contracts_write_set_ptr_t set, void *ptr)
	Records that an object is dead by removing the pointer `ptr` from `set->allocated`.

void	__CPROVER_contracts_write_set_record_deallocated (__CPROVER_contracts_write_set_ptr_t set, void *ptr)
	Records that an object is deallocated by adding the pointer `ptr` to `set->deallocated`.

__CPROVER_bool	__CPROVER_contracts_write_set_check_allocated_deallocated_is_empty (__CPROVER_contracts_write_set_ptr_t set)
	Returns true iff `set->deallocated` is empty.

__CPROVER_bool	__CPROVER_contracts_write_set_check_assignment (__CPROVER_contracts_write_set_ptr_t set, void *ptr, __CPROVER_size_t size)
	Checks if an assignment to the range of bytes starting at `ptr` and of `size` bytes is allowed according to `set`.

__CPROVER_bool	__CPROVER_contracts_write_set_check_array_set (__CPROVER_contracts_write_set_ptr_t set, void *dest)
	Checks if the operation `array_set(dest, ...)` is allowed according to `set`.

__CPROVER_bool	__CPROVER_contracts_write_set_check_array_copy (__CPROVER_contracts_write_set_ptr_t set, void *dest)
	Checks if the operation `array_copy(dest, ...)` is allowed according to `set`.

__CPROVER_bool	__CPROVER_contracts_write_set_check_array_replace (__CPROVER_contracts_write_set_ptr_t set, void dest, void src)
	Checks if the operation `array_replace(dest, src)` is allowed according to `set`.

__CPROVER_bool	__CPROVER_contracts_write_set_check_havoc_object (__CPROVER_contracts_write_set_ptr_t set, void *ptr)
	Checks if a `havoc_object(ptr)` is allowed according to `set`.

__CPROVER_bool	__CPROVER_contracts_write_set_check_deallocate (__CPROVER_contracts_write_set_ptr_t set, void *ptr)
	Checks if the deallocation of `ptr` is allowed according to `set`.

__CPROVER_bool	__CPROVER_contracts_write_set_check_assigns_clause_inclusion (__CPROVER_contracts_write_set_ptr_t reference, __CPROVER_contracts_write_set_ptr_t candidate)
	Checks the inclusion of the `candidate->contract_assigns` elements in `reference->contract_assigns` or `reference->allocated`.

__CPROVER_bool	__CPROVER_contracts_write_set_check_frees_clause_inclusion (__CPROVER_contracts_write_set_ptr_t reference, __CPROVER_contracts_write_set_ptr_t candidate)
	Checks the inclusion of the `candidate->contract_frees` elements in `reference->contract_frees` or `reference->allocated`.

__CPROVER_bool	__CPROVER_contracts_free (void *, __CPROVER_contracts_write_set_ptr_t)
	Models the instrumented version of the free function.

void	__CPROVER_contracts_write_set_deallocate_freeable (__CPROVER_contracts_write_set_ptr_t set, __CPROVER_contracts_write_set_ptr_t target)
	Non-deterministically call __CPROVER_contracts_free on all elements of `set->contract_frees`, and records the freed pointers in `target->deallocated`.

void	__CPROVER_contracts_link_ptr_pred_ctx (__CPROVER_contracts_write_set_ptr_t write_set, __CPROVER_contracts_ptr_pred_ctx_ptr_t ptr_pred_ctx)
	Links `is_fresh_set` to `write_set->linked_ptr_pred_ctx` to share evaluation context between requires and ensures clauses for separation checks.

void	__CPROVER_contracts_link_allocated (__CPROVER_contracts_write_set_ptr_t write_set_postconditions, __CPROVER_contracts_write_set_ptr_t write_set_to_link)
	Links `write_set_to_link->allocated` to `write_set_postconditions->linked_allocated` so that allocations performed by __CPROVER_contracts_is_fresh when evaluating ensures clauses are recorded in `write_set_to_link`.

void	__CPROVER_contracts_link_deallocated (__CPROVER_contracts_write_set_ptr_t write_set_postconditions, __CPROVER_contracts_write_set_ptr_t write_set_to_link)
	Links `write_set_to_link->deallocated` to `write_set_postconditions->linked_deallocated` so that deallocations performed by the function get recorded in `write_set_to_link->deallocated` and are later available to __CPROVER_contracts_was_freed predicate when evaluating ensures clauses.

void *	__CPROVER_contracts_malloc (__CPROVER_size_t, __CPROVER_contracts_write_set_ptr_t)
	Models the instrumented interface of the `malloc` function.

void	__CPROVER_contracts_make_invalid_pointer (void **ptr)
	Makes the given pointer invalid.

__CPROVER_bool	__CPROVER_contracts_pointer_equals (void *ptr1, void ptr2, __CPROVER_bool may_fail, __CPROVER_contracts_write_set_ptr_t write_set)
	Implementation of the `pointer_equals` front-end predicate.

__CPROVER_bool	__CPROVER_contracts_is_fresh (void **elem, __CPROVER_size_t size, __CPROVER_bool may_fail, __CPROVER_contracts_write_set_ptr_t write_set)
	Implementation of the `is_fresh` front-end predicate.

__CPROVER_bool	__CPROVER_contracts_pointer_in_range_dfcc (void lb, void ptr, void ub, __CPROVER_bool may_fail, __CPROVER_contracts_write_set_ptr_t write_set)
	Implementation of the `pointer_in_range_dfcc` front-end predicate.

void *	__CPROVER_contracts_write_set_havoc_get_assignable_target (__CPROVER_contracts_write_set_ptr_t set, __CPROVER_size_t idx)
	Returns the start address of the conditional address range found at index `idx` in `set->contract_assigns`.

void	__CPROVER_contracts_write_set_havoc_object_whole (__CPROVER_contracts_write_set_ptr_t set, __CPROVER_size_t idx)
	Havocs the whole object pointed to by the lower bound pointer of the element stored at index `idx` in `set->contract_assigns`, if it is writable.

void	__CPROVER_contracts_write_set_havoc_slice (__CPROVER_contracts_write_set_ptr_t set, __CPROVER_size_t idx)
	Havocs the range of bytes represented byt the element stored at index `idx` in `set->contract_assigns`, if it is writable.

__CPROVER_bool	__CPROVER_contracts_is_freeable (void *ptr, __CPROVER_contracts_write_set_ptr_t set)
	Implementation of the `is_freeable` front-end predicate.

__CPROVER_bool	__CPROVER_contracts_was_freed (void *ptr, __CPROVER_contracts_write_set_ptr_t set)
	Returns true iff the pointer `ptr` is found in `set->deallocated`.

void	__CPROVER_contracts_check_replace_ensures_was_freed_preconditions (void *ptr, __CPROVER_contracts_write_set_ptr_t set)
	Asserts that `ptr` is found in `set->contract_frees`.

__CPROVER_bool	__CPROVER_contracts_obeys_contract (void(*function_pointer)(void), void(contract)(void), __CPROVER_bool may_fail, __CPROVER_contracts_write_set_ptr_t set)
	Implementation of the `obeys_contract` front-end predicate.

Variables
const void *	__CPROVER_alloca_object = 0

const void *	__CPROVER_deallocated

const void *	__CPROVER_new_object = 0

const void *	__CPROVER_memory_leak

__CPROVER_bool	__CPROVER_malloc_is_new_array = 0

Detailed Description

Types and functions for dynamic frames instrumentation in contracts.

Definition in file cprover_contracts.c.

Macro Definition Documentation

◆ __CPROVER_contracts_library_defined

#define __CPROVER_contracts_library_defined

Definition at line 7 of file cprover_contracts.c.

Typedef Documentation

◆ __CPROVER_contracts_car_set_ptr_t

typedef __CPROVER_contracts_car_set_t* __CPROVER_contracts_car_set_ptr_t

Type of pointers to __CPROVER_contracts_car_set_t.

Definition at line 46 of file cprover_contracts.c.

◆ __CPROVER_contracts_obj_set_ptr_t

typedef __CPROVER_contracts_obj_set_t* __CPROVER_contracts_obj_set_ptr_t

Type of pointers to __CPROVER_contracts_obj_set_t.

Definition at line 68 of file cprover_contracts.c.

◆ __CPROVER_contracts_ptr_pred_ctx_ptr_t

typedef __CPROVER_contracts_ptr_pred_ctx_t* __CPROVER_contracts_ptr_pred_ctx_ptr_t

Type of pointers to __CPROVER_contracts_ptr_pred_ctx_t.

Definition at line 81 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_ptr_t

typedef __CPROVER_contracts_write_set_t* __CPROVER_contracts_write_set_ptr_t

Type of pointers to __CPROVER_contracts_write_set_t.

Definition at line 120 of file cprover_contracts.c.

Function Documentation

◆ __builtin_clzl()

int __builtin_clzl ( unsigned long )

◆ __CPROVER_contracts_car_create()

__CPROVER_contracts_car_t __CPROVER_contracts_car_create	(	void *	ptr,
		__CPROVER_size_t	size
	)

Creates a __CPROVER_car_t struct from ptr and size.

Parameters

[in]	ptr	Start address of the range
[in]	size	Size in bytes

Returns: A __CPROVER_contracts_car_t value

Definition at line 127 of file cprover_contracts.c.

◆ __CPROVER_contracts_car_set_contains()

__CPROVER_bool __CPROVER_contracts_car_set_contains	(	__CPROVER_contracts_car_set_ptr_t	set,
		__CPROVER_contracts_car_t	candidate
	)

Checks if candidate is included in one of set 's elements.

Parameters

[in]	set	Set to check inclusion in
[in]	candidate	A candidate __CPROVER_contracts_car_t

Returns: True iff an element of set contains candidate

Definition at line 219 of file cprover_contracts.c.

◆ __CPROVER_contracts_car_set_create()

void __CPROVER_contracts_car_set_create	(	__CPROVER_contracts_car_set_ptr_t	set,
		__CPROVER_size_t	max_elems
	)

Initialises a __CPROVER_contracts_car_set_ptr_t object.

Parameters

[in,out]	set	Pointer to the object to initialise
[in]	max_elems	Max number of elements to store in the set

Definition at line 147 of file cprover_contracts.c.

◆ __CPROVER_contracts_car_set_insert()

void __CPROVER_contracts_car_set_insert	(	__CPROVER_contracts_car_set_ptr_t	set,
		__CPROVER_size_t	idx,
		void *	ptr,
		__CPROVER_size_t	size
	)

Inserts a __CPROVER_contracts_car_t snapshotted from ptr and size into set at index idx.

Parameters

[in,out]	set	Set to insert into
[in]	idx	Insertion index
[in]	ptr	Pointer to the range of bytes
[in]	size	Size of the range in number of bytes

Definition at line 168 of file cprover_contracts.c.

◆ __CPROVER_contracts_car_set_remove()

void __CPROVER_contracts_car_set_remove	(	__CPROVER_contracts_car_set_ptr_t	set,
		void *	ptr
	)

Invalidates all cars in the set that point into the same object as the given ptr.

Parameters

[in,out]	set	Set to update
[in]	ptr	Pointer to the object to invalidate

Definition at line 197 of file cprover_contracts.c.

◆ __CPROVER_contracts_check_replace_ensures_was_freed_preconditions()

void __CPROVER_contracts_check_replace_ensures_was_freed_preconditions	(	void *	ptr,
		__CPROVER_contracts_write_set_ptr_t	set
	)

Asserts that ptr is found in set->contract_frees.

If proved, the assertion demonstrates that it is possible to assume that was_freed(ptr) holds as a post condition without causing a contradiction.

Definition at line 1680 of file cprover_contracts.c.

◆ __CPROVER_contracts_free()

__CPROVER_bool __CPROVER_contracts_free	(	void *	,
		__CPROVER_contracts_write_set_ptr_t
	)

Models the instrumented version of the free function.

Remarks: Uses of this function will be remapped to the instrumented version of the free found in the goto model.

◆ __CPROVER_contracts_is_freeable()

__CPROVER_bool __CPROVER_contracts_is_freeable	(	void *	ptr,
		__CPROVER_contracts_write_set_ptr_t	set
	)

Implementation of the is_freeable front-end predicate.

Returns: True iff a pointer satisfies the preconditions for the free function and can hence be safely deallocated using free.

If called in an assumption context, only basic conditions are checked: the pointer has offset 0 and points to a dynamic object. If called in an assertion context, extra conditions depending on nondeterministic CPROVER instrumentation variables are checked, yielding the full set of conditions checked by the CPROVER library implementation of free.

Definition at line 1622 of file cprover_contracts.c.

◆ __CPROVER_contracts_is_fresh()

__CPROVER_bool __CPROVER_contracts_is_fresh	(	void **	elem,
		__CPROVER_size_t	size,
		__CPROVER_bool	may_fail,
		__CPROVER_contracts_write_set_ptr_t	write_set
	)

Implementation of the is_fresh front-end predicate.

Parameters

elem	Pointer to the target pointer of the check
size	Size to check
may_fail	Allow predicate to fail in assume mode
write_set	Write set (carries assert/assume requires/ensures context flags, sets to allocated/seen objects for separation checks)

The behaviour is as follows:

In assume contexts, returns false if another pointer predicate is already assumed, otherwise, allocates a fresh object, mark *elem and elem as seen in the write set.
In assert contexts, returns false if another pointer predicate is already succesfully asserted, otherwise checks separation and size, mark *elem and elem as seen in the write set.

Definition at line 1290 of file cprover_contracts.c.

◆ __CPROVER_contracts_link_allocated()

void __CPROVER_contracts_link_allocated	(	__CPROVER_contracts_write_set_ptr_t	write_set_postconditions,
		__CPROVER_contracts_write_set_ptr_t	write_set_to_link
	)

Links write_set_to_link->allocated to write_set_postconditions->linked_allocated so that allocations performed by __CPROVER_contracts_is_fresh when evaluating ensures clauses are recorded in write_set_to_link.

Definition at line 1117 of file cprover_contracts.c.

◆ __CPROVER_contracts_link_deallocated()

void __CPROVER_contracts_link_deallocated	(	__CPROVER_contracts_write_set_ptr_t	write_set_postconditions,
		__CPROVER_contracts_write_set_ptr_t	write_set_to_link
	)

Links write_set_to_link->deallocated to write_set_postconditions->linked_deallocated so that deallocations performed by the function get recorded in write_set_to_link->deallocated and are later available to __CPROVER_contracts_was_freed predicate when evaluating ensures clauses.

Definition at line 1142 of file cprover_contracts.c.

◆ __CPROVER_contracts_link_ptr_pred_ctx()

void __CPROVER_contracts_link_ptr_pred_ctx	(	__CPROVER_contracts_write_set_ptr_t	write_set,
		__CPROVER_contracts_ptr_pred_ctx_ptr_t	ptr_pred_ctx
	)

Links is_fresh_set to write_set->linked_ptr_pred_ctx to share evaluation context between requires and ensures clauses for separation checks.

Definition at line 1095 of file cprover_contracts.c.

◆ __CPROVER_contracts_make_invalid_pointer()

void __CPROVER_contracts_make_invalid_pointer ( void ** ptr )

Makes the given pointer invalid.

Used to craft invalid pointers when pointer predicates return false in "assume" mode. We have two models for invalid pointers:

default: pointer is uninitialized (empty value set, nondet bit pattern).
simple: pointer is either null or pointing to a dead object of size zero. The simple model is activated by a CLI switch in goto-instrument.

Definition at line 1177 of file cprover_contracts.c.

◆ __CPROVER_contracts_malloc()

void * __CPROVER_contracts_malloc	(	__CPROVER_size_t	,
		__CPROVER_contracts_write_set_ptr_t
	)

Models the instrumented interface of the malloc function.

Remarks: Calls to this function will be remapped to the actual instrumented version of malloc found in the goto model.

◆ __CPROVER_contracts_obeys_contract()

__CPROVER_bool __CPROVER_contracts_obeys_contract	(	void(**)(void)	function_pointer,
		void(*)(void)	contract,
		__CPROVER_bool	may_fail,
		__CPROVER_contracts_write_set_ptr_t	set
	)

Implementation of the obeys_contract front-end predicate.

Returns: True iff a function pointer points to the specified contract.

If called in an assumption context, translates to an assignment function_pointer = contract. If called in an assertion context, translates to an function_pointer == contract. The function pointer is taken by reference to be able to update it using a side-effect in assumption contexts.

Definition at line 1715 of file cprover_contracts.c.

◆ __CPROVER_contracts_obj_set_add()

void __CPROVER_contracts_obj_set_add	(	__CPROVER_contracts_obj_set_ptr_t	set,
		void *	ptr
	)

Adds the ptr to set.

Precondition: set->indexed_by_object_id must be true.

Parameters

[in,out]	set	Set to add the pointer to
[in]	ptr	The pointer to add

Definition at line 321 of file cprover_contracts.c.

◆ __CPROVER_contracts_obj_set_append()

void __CPROVER_contracts_obj_set_append	(	__CPROVER_contracts_obj_set_ptr_t	set,
		void *	ptr
	)

Appends ptr to set.

Precondition: set->indexed_by_object_id must be false.

Parameters

[in,out]	set	The set to append to
[in]	ptr	The pointer to append

Definition at line 340 of file cprover_contracts.c.

◆ __CPROVER_contracts_obj_set_contains()

__CPROVER_bool __CPROVER_contracts_obj_set_contains	(	__CPROVER_contracts_obj_set_ptr_t	set,
		void *	ptr
	)

Checks if a pointer with the same object id as ptr is contained in set.

Parameters

[in,out]	set	The set to check membership in
	ptr	The pointer to check

Returns: True iff a pointer with the same object id exists in set

Definition at line 379 of file cprover_contracts.c.

◆ __CPROVER_contracts_obj_set_contains_exact()

__CPROVER_bool __CPROVER_contracts_obj_set_contains_exact	(	__CPROVER_contracts_obj_set_ptr_t	set,
		void *	ptr
	)

Checks if ptr is contained in set.

Parameters

[in,out]	set	The set to check membership in
	ptr	The pointer to check

Returns: True iff ptr exists in set

Definition at line 396 of file cprover_contracts.c.

◆ __CPROVER_contracts_obj_set_create_append()

void __CPROVER_contracts_obj_set_create_append	(	__CPROVER_contracts_obj_set_ptr_t	set,
		__CPROVER_size_t	max_elems
	)

Initialises a __CPROVER_contracts_obj_set_t object to use it in "append" mode for at most max_elems elements.

Parameters

[in,out]	set	Pointer to the object to initialise
[in,out]	max_elems	Maximum number of objects in the set.

Definition at line 285 of file cprover_contracts.c.

◆ __CPROVER_contracts_obj_set_create_indexed_by_object_id()

void __CPROVER_contracts_obj_set_create_indexed_by_object_id ( __CPROVER_contracts_obj_set_ptr_t set )

Initialises a __CPROVER_contracts_obj_set_t object to use it in "indexed by object id" mode.

The elements array is allocated to 2^OBJECT_BITS, where object bits is calculated as the number of leading zeroes in the __CPROVER_max_alloc_size constant.

Parameters

[in,out] set Pointer to the object to initialise

Definition at line 251 of file cprover_contracts.c.

◆ __CPROVER_contracts_obj_set_release()

void __CPROVER_contracts_obj_set_release ( __CPROVER_contracts_obj_set_ptr_t set )

Releases resources used by set.

Definition at line 305 of file cprover_contracts.c.

◆ __CPROVER_contracts_obj_set_remove()

void __CPROVER_contracts_obj_set_remove	(	__CPROVER_contracts_obj_set_ptr_t	set,
		void *	ptr
	)

Removes ptr form set if ptr exists in set, no-op otherwise.

Parameters

[in,out]	set	Set to update
[in]	ptr	Pointer to remove

Definition at line 359 of file cprover_contracts.c.

◆ __CPROVER_contracts_pointer_equals()

__CPROVER_bool __CPROVER_contracts_pointer_equals	(	void **	ptr1,
		void *	ptr2,
		__CPROVER_bool	may_fail,
		__CPROVER_contracts_write_set_ptr_t	write_set
	)

Implementation of the pointer_equals front-end predicate.

Parameters

ptr1	First argument of the `pointer_equals` predicate
ptr2	Second argument of the `pointer_equals` predicate
may_fail	Allow predicate to fail in assume mode
write_set	Write set which conveys the invocation context (requires/ensures clause, assert/assume context);

The behaviour is as follows: When set->assume_requires_ctx or set->assume_ensures_ctx is true, the predicate nondeterministically invalidates *ptr1 and returns false, or checks that ptr2 is either NULL or valid, and assigns *ptr1 to ptr2. When set->assert_requires_ctx or set->assert_ensures_ctx is true, the predicate checks that both *ptr1 and ptr2 are either NULL or valid, and returns the value of (*ptr1 == ptr2).

Definition at line 1210 of file cprover_contracts.c.

◆ __CPROVER_contracts_pointer_in_range_dfcc()

__CPROVER_bool __CPROVER_contracts_pointer_in_range_dfcc	(	void *	lb,
		void **	ptr,
		void *	ub,
		__CPROVER_bool	may_fail,
		__CPROVER_contracts_write_set_ptr_t	write_set
	)

Implementation of the pointer_in_range_dfcc front-end predicate.

The behaviour depends on the boolean flags carried by write_set which reflect the invocation context: checking vs. replacing a contract, in a requires or an ensures clause context.

Parameters

lb	Lower bound pointer
ptr	Target pointer of the predicate
ub	Upper bound pointer
may_fail	Allow predicate to fail in assume mode
write_set	Write set in which seen/allocated objects are recorded;

The behaviour is as follows:

When set->assume_requires_ctx or set->assume_ensures_ctx is true, the predicate checks that lb and ub are valid, into the same object, ordered, and checks that ptr is between lb and ub.
When set->assert_requires_ctx or set->assert_ensures_ctx is true, the predicate checks that lb and ub are valid, into the same object, ordered, and assigns ptr to some nondet offset between lb and ub.

Definition at line 1491 of file cprover_contracts.c.

◆ __CPROVER_contracts_ptr_pred_ctx_init()

void __CPROVER_contracts_ptr_pred_ctx_init ( __CPROVER_contracts_ptr_pred_ctx_ptr_t set )

Resets the nondet tracker for pointer predicates in set.

Invoked between requires and ensures clauses evaluation to allow ensures clauses to establish different pointer predicates on the same pointers.

Definition at line 412 of file cprover_contracts.c.

◆ __CPROVER_contracts_ptr_pred_ctx_reset()

void __CPROVER_contracts_ptr_pred_ctx_reset ( __CPROVER_contracts_ptr_pred_ctx_ptr_t set )

Resets the nondet tracker for pointer predicates in set.

Invoked right between requires and ensures clauses to allow ensures clauses to establish a different pointer predicates on the same pointers.

Definition at line 424 of file cprover_contracts.c.

◆ __CPROVER_contracts_was_freed()

__CPROVER_bool __CPROVER_contracts_was_freed	(	void *	ptr,
		__CPROVER_contracts_write_set_ptr_t	set
	)

Returns true iff the pointer ptr is found in set->deallocated.

Definition at line 1654 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_add_allocated()

void __CPROVER_contracts_write_set_add_allocated	(	__CPROVER_contracts_write_set_ptr_t	set,
		void *	ptr
	)

Adds the dynamically allocated pointer ptr to set->allocated.

Parameters

[in,out]	set	The set to update
[in]	ptr	Pointer to a dynamic object `x = __CPROVER_allocate(...)`.

Definition at line 633 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_add_decl()

void __CPROVER_contracts_write_set_add_decl	(	__CPROVER_contracts_write_set_ptr_t	set,
		void *	ptr
	)

Adds the pointer ptr to set->allocated.

Parameters

[in,out]	set	The set to update
[in]	ptr	Pointer to an object declared using `DECL x`.

Definition at line 655 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_add_freeable()

void __CPROVER_contracts_write_set_add_freeable	(	__CPROVER_contracts_write_set_ptr_t	set,
		void *	ptr
	)

Adds the freeable pointer ptr to set->contract_frees.

Parameters

[in,out]	set	The set to update
[in]	ptr	The pointer to add

Definition at line 597 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_check_allocated_deallocated_is_empty()

__CPROVER_bool __CPROVER_contracts_write_set_check_allocated_deallocated_is_empty ( __CPROVER_contracts_write_set_ptr_t set )

Returns true iff set->deallocated is empty.

Parameters

[in] set The set to be checked for emptiness

Returns: True iff set->deallocated is empty

Definition at line 759 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_check_array_copy()

__CPROVER_bool __CPROVER_contracts_write_set_check_array_copy	(	__CPROVER_contracts_write_set_ptr_t	set,
		void *	dest
	)

Checks if the operation array_copy(dest, ...) is allowed according to set.

Remarks: The array_copy operation updates all of *dest (possibly using nondet values), even when *src is smaller.

Parameters

[in]	set	Write set to check the `array_copy` operation against
[in]	dest	The destination pointer

Returns: True iff the range of bytes starting at dest and of __CPROVER_OBJECT_SIZE(dest) - __CPROVER_POINTER_OFFSET(dest) bytes is contained in set->allocated or set->contract_assigns.

Definition at line 886 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_check_array_replace()

__CPROVER_bool __CPROVER_contracts_write_set_check_array_replace	(	__CPROVER_contracts_write_set_ptr_t	set,
		void *	dest,
		void *	src
	)

Checks if the operation array_replace(dest, src) is allowed according to set.

Remarks: The array_replace operation updates at most size-of-*src bytes in *dest, i.e. it replaces MIN(size-of-*dest, size-of-*src) bytes in *dest.

Parameters

[in]	set	Write set to check the `array_replace` operation against
[in]	dest	The destination pointer
[in]	src	The source pointer

Returns: True iff the range of bytes starting at dest and extending for MIN(__CPROVER_OBJECT_SIZE(dest) - __CPROVER_POINTER_OFFSET(dest), __CPROVER_OBJECT_SIZE(src) - __CPROVER_POINTER_OFFSET(src)) bytes is contained in set->allocated or set->contract_assigns.

Definition at line 909 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_check_array_set()

__CPROVER_bool __CPROVER_contracts_write_set_check_array_set	(	__CPROVER_contracts_write_set_ptr_t	set,
		void *	dest
	)

Checks if the operation array_set(dest, ...) is allowed according to set.

Remarks: The array_set operation updates all bytes of the object starting from dest.

Parameters

[in]	set	Write set to check the array_set operation against
[in]	dest	The destination pointer

Returns: True iff the range of bytes starting at dest and of __CPROVER_OBJECT_SIZE(dest) - __CPROVER_POINTER_OFFSET(dest) bytes is contained in set->allocated or set->contract_assigns.

Definition at line 866 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_check_assignment()

__CPROVER_bool __CPROVER_contracts_write_set_check_assignment	(	__CPROVER_contracts_write_set_ptr_t	set,
		void *	ptr,
		__CPROVER_size_t	size
	)

Checks if an assignment to the range of bytes starting at ptr and of size bytes is allowed according to set.

Parameters

[in]	set	Write set to check the assignment against
[in]	ptr	Start address of the assigned range
[in]	size	Size of the assigned range in bytes

Returns: True iff the range of bytes starting at ptr of size bytes is contained in set->allocated or set->contract_assigns.

Definition at line 774 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_check_assigns_clause_inclusion()

__CPROVER_bool __CPROVER_contracts_write_set_check_assigns_clause_inclusion	(	__CPROVER_contracts_write_set_ptr_t	reference,
		__CPROVER_contracts_write_set_ptr_t	candidate
	)

Checks the inclusion of the candidate->contract_assigns elements in reference->contract_assigns or reference->allocated.

Precondition: candidate->allocated must be empty.

Parameters

[in]	reference	Reference write set from a caller
[in]	candidate	Candidate write set from a contract being replaced

Returns: True iff all elements of candidate->contract_assigns are included in some element of reference->contract_assigns or reference->allocated

Definition at line 981 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_check_deallocate()

__CPROVER_bool __CPROVER_contracts_write_set_check_deallocate	(	__CPROVER_contracts_write_set_ptr_t	set,
		void *	ptr
	)

Checks if the deallocation of ptr is allowed according to set.

Precondition: The pointer ptr is involved in the GOTO instruction CALL __CPROVER_deallocate(ptr);

Parameters

[in]	set	Write set to check the deallocation against
[in]	ptr	Deallocated pointer to check set to check the deallocation against

Returns: True iff deallocation is allowed and ptr is contained in set->contract_frees or set->allocated.

Definition at line 952 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_check_frees_clause_inclusion()

__CPROVER_bool __CPROVER_contracts_write_set_check_frees_clause_inclusion	(	__CPROVER_contracts_write_set_ptr_t	reference,
		__CPROVER_contracts_write_set_ptr_t	candidate
	)

Checks the inclusion of the candidate->contract_frees elements in reference->contract_frees or reference->allocated.

Precondition: candidate->allocated must be empty.

Parameters

[in]	reference	Reference write set from a caller
[in]	candidate	Candidate write set from a contract being replaced

Returns: True iff all elements of candidate->contract_frees are included in some element of reference->contract_frees or reference->allocated

Definition at line 1012 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_check_havoc_object()

__CPROVER_bool __CPROVER_contracts_write_set_check_havoc_object	(	__CPROVER_contracts_write_set_ptr_t	set,
		void *	ptr
	)

Checks if a havoc_object(ptr) is allowed according to set.

Parameters

[in]	set	The write set to check the operation against
[in]	ptr	Pointer to the havoced object

Returns: True iff the range of bytes starting at (char *)ptr - __CPROVER_POINTER_OFFSET(ptr) and of size __CPROVER_OBJECT_SIZE(ptr) is contained in set->contract_assigns or set->allocated.

Definition at line 931 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_create()

void __CPROVER_contracts_write_set_create	(	__CPROVER_contracts_write_set_ptr_t	set,
		__CPROVER_size_t	contract_assigns_size,
		__CPROVER_size_t	contract_frees_size,
		__CPROVER_bool	assume_requires_ctx,
		__CPROVER_bool	assert_requires_ctx,
		__CPROVER_bool	assume_ensures_ctx,
		__CPROVER_bool	assert_ensures_ctx,
		__CPROVER_bool	allow_allocate,
		__CPROVER_bool	allow_deallocate
	)

Initialises a __CPROVER_contracts_write_set_t object.

Parameters

[in,out]	set	Pointer to the object to initialise
[in]	contract_assigns_size	Max size of the assigns clause
[in]	contract_frees_size	Max size of the frees clause
[in]	assume_requires_ctx	True iff this write set is used to check side effects in a requires clause in contract checking mode
[in]	assert_requires_ctx	True iff this write set is used to check side effects in a requires clause in contract replacement mode
[in]	assume_ensures_ctx	True iff this write set is used to check for side effects in an ensures clause in contract replacement mode
[in]	assert_ensures_ctx	True iff this write set is used to check for side effects in an ensures clause in contract checking mode
[in]	allow_allocate	True iff the context gobally allows dynamic allocation.
[in]	allow_deallocate	True iff the context gobally allows dynamic deallocation.

Definition at line 447 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_deallocate_freeable()

void __CPROVER_contracts_write_set_deallocate_freeable	(	__CPROVER_contracts_write_set_ptr_t	set,
		__CPROVER_contracts_write_set_ptr_t	target
	)

Non-deterministically call __CPROVER_contracts_free on all elements of set->contract_frees, and records the freed pointers in target->deallocated.

Parameters

[in]	set	Write set to free
[out]	target	Write set to record deallocations in

Definition at line 1057 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_havoc_get_assignable_target()

void * __CPROVER_contracts_write_set_havoc_get_assignable_target	(	__CPROVER_contracts_write_set_ptr_t	set,
		__CPROVER_size_t	idx
	)

Returns the start address of the conditional address range found at index idx in set->contract_assigns.

Definition at line 1567 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_havoc_object_whole()

void __CPROVER_contracts_write_set_havoc_object_whole	(	__CPROVER_contracts_write_set_ptr_t	set,
		__CPROVER_size_t	idx
	)

Havocs the whole object pointed to by the lower bound pointer of the element stored at index idx in set->contract_assigns, if it is writable.

Definition at line 1586 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_havoc_slice()

void __CPROVER_contracts_write_set_havoc_slice	(	__CPROVER_contracts_write_set_ptr_t	set,
		__CPROVER_size_t	idx
	)

Havocs the range of bytes represented byt the element stored at index idx in set->contract_assigns, if it is writable.

Definition at line 1599 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_insert_assignable()

void __CPROVER_contracts_write_set_insert_assignable	(	__CPROVER_contracts_write_set_ptr_t	set,
		__CPROVER_size_t	idx,
		void *	ptr,
		__CPROVER_size_t	size
	)

Inserts a snapshot of the range starting at ptr of size size at index idx in set->contract_assigns.

Parameters

[in,out]	set	The set to update
[in]	idx	Insertion index
[in]	ptr	Start of the range of bytes
[in]	size	Size of the range in bytes

Definition at line 521 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_insert_object_from()

void __CPROVER_contracts_write_set_insert_object_from	(	__CPROVER_contracts_write_set_ptr_t	set,
		__CPROVER_size_t	idx,
		void *	ptr
	)

Inserts a snapshot of the range of bytes starting at ptr and extending to the end of the object in set->contact_assigns at index idx.

The start address is ptr
The size in bytes is __CPROVER_OBJECT_SIZE(ptr) - __CPROVER_POINTER_OFFSET(ptr)

Parameters

[in,out]	set	The set to update
[in]	idx	Insertion index
[in]	ptr	Pointer to the start of the range

Definition at line 565 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_insert_object_upto()

void __CPROVER_contracts_write_set_insert_object_upto	(	__CPROVER_contracts_write_set_ptr_t	set,
		__CPROVER_size_t	idx,
		void *	ptr,
		__CPROVER_size_t	size
	)

Inserts a snapshot of the range of bytes starting at ptr of size bytes in set->contact_assigns at index idx.

Parameters

[in,out]	set	The set to update
[in]	idx	Insertion index
[in]	ptr	Pointer to the start of the range
[in]	size	Size of the range in bytes

Definition at line 584 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_insert_object_whole()

void __CPROVER_contracts_write_set_insert_object_whole	(	__CPROVER_contracts_write_set_ptr_t	set,
		__CPROVER_size_t	idx,
		void *	ptr
	)

Inserts a snapshot of the range of bytes covering the whole object pointed to by ptr in set->contact_assigns at index idx.

The start address is ptr - __CPROVER_POINTER_OFFSET(ptr)
The size in bytes is __CPROVER_OBJECT_SIZE(ptr)

at index idx in set.

Parameters

[in,out]	set	The set to update
[in]	idx	Insertion index
[in]	ptr	Pointer to the object

Definition at line 541 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_record_dead()

void __CPROVER_contracts_write_set_record_dead	(	__CPROVER_contracts_write_set_ptr_t	set,
		void *	ptr
	)

Records that an object is dead by removing the pointer ptr from set->allocated.

Precondition: ptr is the start address &x of an object declared as 'DEAD x'.

Parameters

[in,out]	set	The set to update
[in]	ptr	Pointer to the dead object

Definition at line 680 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_record_deallocated()

void __CPROVER_contracts_write_set_record_deallocated	(	__CPROVER_contracts_write_set_ptr_t	set,
		void *	ptr
	)

Records that an object is deallocated by adding the pointer ptr to set->deallocated.

Precondition: ptr was deallocated with a call to __CPROVER_deallocate(ptr).

Parameters

[in,out]	set	The set to update
[in]	ptr	Pointer to the deallocated object

Definition at line 705 of file cprover_contracts.c.

◆ __CPROVER_contracts_write_set_release()

void __CPROVER_contracts_write_set_release ( __CPROVER_contracts_write_set_ptr_t set )

Releases resources used by set.

Definition at line 484 of file cprover_contracts.c.

◆ __VERIFIER_nondet___CPROVER_bool()

__CPROVER_bool __VERIFIER_nondet___CPROVER_bool ( void )

◆ __VERIFIER_nondet_size()

__CPROVER_size_t __VERIFIER_nondet_size ( void )

Variable Documentation

◆ __CPROVER_alloca_object

const void * __CPROVER_alloca_object = 0

Definition at line 10 of file cprover_contracts.c.

◆ __CPROVER_deallocated

const void* __CPROVER_deallocated

extern

◆ __CPROVER_malloc_is_new_array

__CPROVER_bool __CPROVER_malloc_is_new_array = 0

Definition at line 14 of file cprover_contracts.c.

◆ __CPROVER_memory_leak

const void* __CPROVER_memory_leak

extern

◆ __CPROVER_new_object

const void * __CPROVER_new_object = 0

Definition at line 12 of file cprover_contracts.c.

Classes

Macros

Typedefs

Functions

Variables

Detailed Description

Macro Definition Documentation

◆ __CPROVER_contracts_library_defined

Typedef Documentation

◆ __CPROVER_contracts_car_set_ptr_t

◆ __CPROVER_contracts_obj_set_ptr_t

◆ __CPROVER_contracts_ptr_pred_ctx_ptr_t

◆ __CPROVER_contracts_write_set_ptr_t

Function Documentation

◆ __builtin_clzl()

◆ __CPROVER_contracts_car_create()

◆ __CPROVER_contracts_car_set_contains()

◆ __CPROVER_contracts_car_set_create()

◆ __CPROVER_contracts_car_set_insert()

◆ __CPROVER_contracts_car_set_remove()

◆ __CPROVER_contracts_check_replace_ensures_was_freed_preconditions()

◆ __CPROVER_contracts_free()

◆ __CPROVER_contracts_is_freeable()

◆ __CPROVER_contracts_is_fresh()

◆ __CPROVER_contracts_link_allocated()

◆ __CPROVER_contracts_link_deallocated()

◆ __CPROVER_contracts_link_ptr_pred_ctx()

◆ __CPROVER_contracts_make_invalid_pointer()

◆ __CPROVER_contracts_malloc()

◆ __CPROVER_contracts_obeys_contract()

◆ __CPROVER_contracts_obj_set_add()

◆ __CPROVER_contracts_obj_set_append()

◆ __CPROVER_contracts_obj_set_contains()

◆ __CPROVER_contracts_obj_set_contains_exact()

◆ __CPROVER_contracts_obj_set_create_append()

◆ __CPROVER_contracts_obj_set_create_indexed_by_object_id()

◆ __CPROVER_contracts_obj_set_release()

◆ __CPROVER_contracts_obj_set_remove()

◆ __CPROVER_contracts_pointer_equals()

◆ __CPROVER_contracts_pointer_in_range_dfcc()

◆ __CPROVER_contracts_ptr_pred_ctx_init()

◆ __CPROVER_contracts_ptr_pred_ctx_reset()

◆ __CPROVER_contracts_was_freed()

◆ __CPROVER_contracts_write_set_add_allocated()

◆ __CPROVER_contracts_write_set_add_decl()

◆ __CPROVER_contracts_write_set_add_freeable()

◆ __CPROVER_contracts_write_set_check_allocated_deallocated_is_empty()

◆ __CPROVER_contracts_write_set_check_array_copy()

◆ __CPROVER_contracts_write_set_check_array_replace()

◆ __CPROVER_contracts_write_set_check_array_set()

◆ __CPROVER_contracts_write_set_check_assignment()

◆ __CPROVER_contracts_write_set_check_assigns_clause_inclusion()

◆ __CPROVER_contracts_write_set_check_deallocate()

◆ __CPROVER_contracts_write_set_check_frees_clause_inclusion()

◆ __CPROVER_contracts_write_set_check_havoc_object()

◆ __CPROVER_contracts_write_set_create()

◆ __CPROVER_contracts_write_set_deallocate_freeable()

◆ __CPROVER_contracts_write_set_havoc_get_assignable_target()

◆ __CPROVER_contracts_write_set_havoc_object_whole()

◆ __CPROVER_contracts_write_set_havoc_slice()

◆ __CPROVER_contracts_write_set_insert_assignable()

◆ __CPROVER_contracts_write_set_insert_object_from()

◆ __CPROVER_contracts_write_set_insert_object_upto()

◆ __CPROVER_contracts_write_set_insert_object_whole()

◆ __CPROVER_contracts_write_set_record_dead()

◆ __CPROVER_contracts_write_set_record_deallocated()

◆ __CPROVER_contracts_write_set_release()

◆ __VERIFIER_nondet___CPROVER_bool()

◆ __VERIFIER_nondet_size()

Variable Documentation

◆ __CPROVER_alloca_object

◆ __CPROVER_deallocated

◆ __CPROVER_malloc_is_new_array

◆ __CPROVER_memory_leak

◆ __CPROVER_new_object