6#ifndef __CPROVER_contracts_library_defined
7#define __CPROVER_contracts_library_defined
16#if defined(_WIN32) && defined(_M_X64)
120 "ptr NULL or writable up to size");
123 "CAR size is less than __CPROVER_max_malloc_size");
127 "no offset bits overflow on CAR upper bound computation");
129 .is_writable = ptr != 0, .size = size, .lb = ptr, .ub = (
char *)ptr + size};
168 "ptr NULL or writable up to size");
171 "CAR size is less than __CPROVER_max_malloc_size");
175 "no offset bits overflow on CAR upper bound computation");
178 .is_writable = ptr != 0, .size = size, .lb = ptr, .ub = (
char *)ptr + size};
197 elem->is_writable = 0;
252#if defined(_WIN32) && defined(_M_X64)
264 .indexed_by_object_id = 1,
288 .indexed_by_object_id = 0,
460 "contract_assigns writable");
463 "contract_frees writable");
466 "contract_frees_append writable");
718 elem->is_writable = 0;
755 "ptr NULL or writable up to size");
773# pragma CPROVER check push
774# pragma CPROVER check disable "pointer"
775# pragma CPROVER check disable "pointer-primitive"
776# pragma CPROVER check disable "unsigned-overflow"
777# pragma CPROVER check disable "signed-overflow"
778# pragma CPROVER check disable "undefined-shift"
779# pragma CPROVER check disable "conversion"
782 "ptr NULL or writable up to size");
799 "CAR size is less than __CPROVER_max_malloc_size");
805 "no offset bits overflow on CAR upper bound computation");
806 void *ub = (
void *)((
char *)ptr + size);
822# pragma CPROVER check pop
933 "set->contract_frees is indexed by object id");
936 "set->allocated is indexed by object id");
966 reference, current->
lb, current->
size);
991 "reference->contract_frees is indexed by object id");
994 "reference->allocated is indexed by object id");
997 void **current =
candidate->contract_frees_append.elems;
1003 void *ptr = *current;
1038 void *ptr = *current;
1074 if((is_fresh_set != 0))
1076 write_set->linked_is_fresh = is_fresh_set;
1171 "__CPROVER_is_fresh is used only in requires or ensures clauses");
1177 write_set->linked_is_fresh,
"set->linked_is_fresh is not NULL");
1186 "only one context flag at a time");
1205 "__CPROVER_is_fresh max allocation size exceeded");
1231 :
write_set->linked_is_fresh->nof_elems + 1;
1233 write_set->linked_is_fresh->is_empty = 0;
1244 "only one context flag at a time");
1259 "__CPROVER_is_fresh requires size <= __CPROVER_max_malloc_size");
1282 write_set->linked_allocated->nof_elems =
1284 ?
write_set->linked_allocated->nof_elems
1285 :
write_set->linked_allocated->nof_elems + 1;
1287 write_set->linked_allocated->is_empty = 0;
1297 "only one context flag at a time");
1331 0,
"__CPROVER_is_fresh is only called in requires or ensures clauses");
1349 "__CPROVER_pointer_in_range_dfcc is used only in requires or ensures "
1355 "lb and ub pointers must have the same object");
1371 *ptr = (
char *)lb + offset;
1448 "__CPROVER_is_freeable is used only in requires or ensures clauses");
1479 "__CPROVER_was_freed is used only in ensures clauses");
1504 "__CPROVER_was_freed is used only in ensures clauses");
1512 "assuming __CPROVER_was_freed(ptr) requires ptr to always exist in the "
1513 "contract's frees clause");
1518 "assuming __CPROVER_was_freed(ptr) requires ptr to always exist in the "
1519 "contract's frees clause");
1542 "__CPROVER_obeys_contract is used only in requires or ensures clauses");
int __CPROVER_malloc_failure_mode
int __CPROVER_malloc_failure_mode_return_null
void * __CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero)
__CPROVER_bool __CPROVER_w_ok(const void *,...)
void __CPROVER_deallocate(void *)
int __CPROVER_malloc_failure_mode_assert_then_assume
__CPROVER_bool __CPROVER_rw_ok(const void *,...)
__CPROVER_bool __CPROVER_r_ok(const void *,...)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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 dealloca...
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_...
void __CPROVER_contracts_obj_set_release(__CPROVER_contracts_obj_set_ptr_t set)
Releases resources used by set.
__CPROVER_contracts_car_t __CPROVER_contracts_car_create(void *ptr, __CPROVER_size_t size)
Creates a __CPROVER_car_t struct from ptr and size.
__CPROVER_size_t __VERIFIER_nondet_size(void)
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_havoc_object(__CPROVER_contracts_write_set_ptr_t set, void *ptr)
Checks if a havoc_object(ptr) is allowed according to set.
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_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_obj_set_remove(__CPROVER_contracts_obj_set_ptr_t set, void *ptr)
Removes ptr form set if ptr exists in set, no-op otherwise.
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_check_replace_ensures_was_freed_preconditions(void *ptr, __CPROVER_contracts_write_set_ptr_t set)
Asserts that ptr is found in set->contract_frees.
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_assign...
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.
__CPROVER_contracts_car_set_t * __CPROVER_contracts_car_set_ptr_t
Type of pointers to __CPROVER_contracts_car_set_t.
__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.
int __builtin_clzl(unsigned long)
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,...
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 s...
__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.
const void * __CPROVER_deallocated
void __CPROVER_contracts_write_set_add_decl(__CPROVER_contracts_write_set_ptr_t set, void *ptr)
Adds the pointer ptr to set->allocated.
const void * __CPROVER_new_object
void __CPROVER_contracts_write_set_release(__CPROVER_contracts_write_set_ptr_t set)
Releases resources used by set.
__CPROVER_bool __CPROVER_contracts_free(void *, __CPROVER_contracts_write_set_ptr_t)
Models the instrumented version of the free function.
__CPROVER_bool __CPROVER_contracts_obj_set_contains_exact(__CPROVER_contracts_obj_set_ptr_t set, void *ptr)
Checks if ptr is contained in 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.
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.
__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.
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,...
void __CPROVER_contracts_obj_set_append(__CPROVER_contracts_obj_set_ptr_t set, void *ptr)
Appends ptr to set.
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 e...
__CPROVER_size_t __CPROVER_max_malloc_size
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void)
__CPROVER_contracts_write_set_t * __CPROVER_contracts_write_set_ptr_t
Type of pointers to __CPROVER_contracts_write_set_t.
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.
__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.
__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.
__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_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 re...
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_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 ...
const void * __CPROVER_memory_leak
__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.
void __CPROVER_contracts_obj_set_add(__CPROVER_contracts_obj_set_ptr_t set, void *ptr)
Adds the ptr to set.
const void * __CPROVER_alloca_object
__CPROVER_contracts_obj_set_t * __CPROVER_contracts_obj_set_ptr_t
Type of pointers to __CPROVER_contracts_car_set_t.
__CPROVER_bool __CPROVER_malloc_is_new_array
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.
__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 refere...
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 ind...
__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.
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 ...
__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.
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 ...
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 se...
__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_add_allocated(__CPROVER_contracts_write_set_ptr_t set, void *ptr)
Adds the dynamically allocated pointer ptr to set->allocated.
void * __CPROVER_contracts_malloc(__CPROVER_size_t, __CPROVER_contracts_write_set_ptr_t)
Models the instrumented interface of the malloc function.
__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.
A set of __CPROVER_contracts_car_t.
__CPROVER_size_t max_elems
Maximum number of elements that can be stored in the set.
__CPROVER_contracts_car_t * elems
An array of car_t of size max_elems.
A conditionally writable range of bytes.
__CPROVER_size_t size
Size of the range in bytes.
void * lb
Lower bound address of the range.
__CPROVER_bool is_writable
True iff __CPROVER_w_ok(lb, size) holds at creation.
void * ub
Upper bound address of the range.
__CPROVER_bool is_empty
True iff nof_elems is 0.
void ** elems
Array of void *pointers, indexed by their object ID or some other order.
__CPROVER_bool indexed_by_object_id
True iff elems is indexed by the object id of the pointers.
__CPROVER_size_t watermark
next usable index in elems if less than max_elems (1 + greatest used index in elems)
__CPROVER_size_t nof_elems
Number of elements currently in the elems array.
__CPROVER_size_t max_elems
Maximum number of elements that can be stored in the set.
Runtime representation of a write set.
__CPROVER_contracts_obj_set_ptr_t linked_allocated
Object set recording the is_fresh allocations in post conditions.
__CPROVER_bool allow_deallocate
True iff dynamic deallocation is allowed (default: true)
__CPROVER_contracts_obj_set_t contract_frees
Set of freeable pointers derived from the contract (indexed mode)
__CPROVER_contracts_obj_set_t deallocated
Set of objects deallocated by the function under analysis (indexed mode)
__CPROVER_contracts_obj_set_ptr_t linked_deallocated
Object set recording the deallocations (used by was_freed)
__CPROVER_contracts_obj_set_ptr_t linked_is_fresh
Pointer to object set supporting the is_fresh predicate checks (indexed mode)
__CPROVER_contracts_car_set_t contract_assigns
Set of car derived from the contract.
__CPROVER_bool assert_requires_ctx
True iff the write set checks requires clauses in an assertion ctx.
__CPROVER_bool assume_requires_ctx
True iff the write set checks requires clauses in an assumption ctx.
__CPROVER_bool assert_ensures_ctx
True iff this write set checks ensures clauses in an assertion ctx.
__CPROVER_contracts_obj_set_t allocated
Set of objects allocated by the function under analysis (indexed mode)
__CPROVER_bool assume_ensures_ctx
True iff the write set checks ensures clauses in an assumption ctx.
__CPROVER_bool allow_allocate
True iff dynamic allocation is allowed (default: true)
__CPROVER_contracts_obj_set_t contract_frees_append
Set of freeable pointers derived from the contract (append mode)