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_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. More...

typedef __CPROVER_contracts_obj_set_t *	__CPROVER_contracts_obj_set_ptr_t
	Type of pointers to __CPROVER_contracts_car_set_t. More...

typedef __CPROVER_contracts_write_set_t *	__CPROVER_contracts_write_set_ptr_t
	Type of pointers to __CPROVER_contracts_write_set_t. More...

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`. More...

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. More...

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`. More...

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`. More...

__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. More...

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. More...

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. More...

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

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

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

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. More...

__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`. More...

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

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. More...

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

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`. More...

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`. More...

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`. More...

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`. More...

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`. More...

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`. More...

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

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`. More...

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`. More...

__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. More...

__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`. More...

__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`. More...

__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`. More...

__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`. More...

__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`. More...

__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`. More...

__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`. More...

__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`. More...

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

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`. More...

void	__CPROVER_contracts_link_is_fresh (__CPROVER_contracts_write_set_ptr_t write_set, __CPROVER_contracts_obj_set_ptr_t is_fresh_set)
	Links `is_fresh_set` to `write_set->linked_is_fresh` so that the is_fresh predicates can be evaluated in requires and ensures clauses. More...

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`. More...

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. More...

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

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

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

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`. More...

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. More...

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. More...

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

__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`. More...

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`. More...

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

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_car_set_t.

Definition at line 68 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 107 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 114 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 206 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 134 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 155 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 184 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 1496 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 1438 of file cprover_contracts.c.

◆ __CPROVER_contracts_is_fresh()

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

Implementation of the is_fresh front-end predicate.

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

Parameters

elem	First argument of the `is_fresh` predicate
size	Second argument of the `is_fresh` predicate
write_set	Write set in which seen/allocated objects are recorded;

The behaviour is as follows:

When set->assume_requires_ctx is true, the predicate allocates a new object, records the object in set->linked_is_fresh, updates *elem to point to the fresh object and returns true;
When set->assume_ensures_ctx is true, the predicate allocates a new object, records the object in set->linked_allocated, updates *elem to point to the fresh object and returns true;
When set->assert_requires_ctx or set->assert_ensures_ctx is true, the predicate first computes wether *elem is in set->linked_is_fresh and returns false if it is. Otherwise it records the object in set->linked_is_fresh and returns the value of r_ok(*elem, size).

Definition at line 1159 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 1087 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 1112 of file cprover_contracts.c.

◆ __CPROVER_contracts_link_is_fresh()

void __CPROVER_contracts_link_is_fresh	(	__CPROVER_contracts_write_set_ptr_t	write_set,
		__CPROVER_contracts_obj_set_ptr_t	is_fresh_set
	)

Links is_fresh_set to write_set->linked_is_fresh so that the is_fresh predicates can be evaluated in requires and ensures clauses.

Definition at line 1065 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_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 1531 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 308 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 327 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 366 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 383 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 272 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 238 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 292 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 346 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_contracts_write_set_ptr_t	write_set
	)

Definition at line 1336 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 1470 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 603 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 625 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 565 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 729 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 856 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 879 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 836 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 744 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 951 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 922 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 982 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 901 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 412 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 1027 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 1383 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 1402 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 1415 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 486 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 530 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.

The start address is ptr
The size in bytes is size

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 552 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 506 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 650 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 675 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 449 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_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_is_fresh()

◆ __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_in_range_dfcc()

◆ __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