cprover
Loading...
Searching...
No Matches
cprover_contracts.c
Go to the documentation of this file.
1
3
4/* FUNCTION: __CPROVER_contracts_library */
5
6#ifndef __CPROVER_contracts_library_defined
7#define __CPROVER_contracts_library_defined
8
9// external dependencies
10extern __CPROVER_size_t __CPROVER_max_malloc_size;
12extern const void *__CPROVER_deallocated;
13const void *__CPROVER_new_object = 0;
14extern const void *__CPROVER_memory_leak;
16#if defined(_WIN32) && defined(_M_X64)
17int __builtin_clzll(unsigned long long);
18#else
19int __builtin_clzl(unsigned long);
20#endif
22__CPROVER_size_t __VERIFIER_nondet_size(void);
23
25typedef struct
26{
28 __CPROVER_bool is_writable;
30 __CPROVER_size_t size;
32 void *lb;
34 void *ub;
36
45
48
50typedef struct
51{
53 __CPROVER_size_t max_elems;
56 __CPROVER_size_t watermark;
58 __CPROVER_size_t nof_elems;
60 __CPROVER_bool is_empty;
62 __CPROVER_bool indexed_by_object_id;
65 void **elems;
67
70
106
109
115__CPROVER_contracts_car_create(void *ptr, __CPROVER_size_t size)
116{
117__CPROVER_HIDE:;
119 ((ptr == 0) | __CPROVER_rw_ok(ptr, size)),
120 "ptr NULL or writable up to size");
123 "CAR size is less than __CPROVER_max_malloc_size");
124 __CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(ptr);
126 !(offset > 0) | (offset + size <= __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};
130}
131
137 __CPROVER_size_t max_elems)
138{
139__CPROVER_HIDE:;
140#ifdef DFCC_DEBUG
143 "set writable");
144#endif
145 set->max_elems = max_elems;
146 set->elems =
147 __CPROVER_allocate(max_elems * sizeof(__CPROVER_contracts_car_t), 1);
148}
149
158 __CPROVER_size_t idx,
159 void *ptr,
160 __CPROVER_size_t size)
161{
162__CPROVER_HIDE:;
163#ifdef DFCC_DEBUG
164 __CPROVER_assert((set != 0) & (idx < set->max_elems), "no OOB access");
165#endif
167 ((ptr == 0) | __CPROVER_rw_ok(ptr, size)),
168 "ptr NULL or writable up to size");
171 "CAR size is less than __CPROVER_max_malloc_size");
172 __CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(ptr);
174 !(offset > 0) | (offset + size <= __CPROVER_max_malloc_size),
175 "no offset bits overflow on CAR upper bound computation");
176 __CPROVER_contracts_car_t *elem = set->elems + idx;
178 .is_writable = ptr != 0, .size = size, .lb = ptr, .ub = (char *)ptr + size};
179}
180
187 void *ptr)
188{
189__CPROVER_HIDE:;
190 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
191 __CPROVER_size_t idx = set->max_elems;
192 __CPROVER_contracts_car_t *elem = set->elems;
193CAR_SET_REMOVE_LOOP:
194 while(idx != 0)
195 {
196 if(object_id == __CPROVER_POINTER_OBJECT(elem->lb))
197 elem->is_writable = 0;
198 ++elem;
199 --idx;
200 }
201}
202
210{
211__CPROVER_HIDE:;
212 __CPROVER_bool incl = 0;
213 __CPROVER_size_t idx = set->max_elems;
214 __CPROVER_contracts_car_t *elem = set->elems;
215CAR_SET_CONTAINS_LOOP:
216 while(idx != 0)
217 {
218 incl |= (int)candidate.is_writable & (int)elem->is_writable &
219 (int)__CPROVER_same_object(elem->lb, candidate.lb) &
221 __CPROVER_POINTER_OFFSET(candidate.lb)) &
222 (__CPROVER_POINTER_OFFSET(candidate.ub) <=
224 ++elem;
225 --idx;
226 }
227
228 return incl;
229}
230
241{
242__CPROVER_HIDE:;
243#ifdef DFCC_DEBUG
246 "set writable");
247#endif
248 // compute the maximum number of objects that can exist in the
249 // symex state from the number of object_bits/offset_bits
250 // the number of object bits is determined by counting the number of leading
251 // zeroes of the built-in constant __CPROVER_max_malloc_size;
252#if defined(_WIN32) && defined(_M_X64)
254 __CPROVER_size_t nof_objects = 1ULL << object_bits;
255#else
256 int object_bits = __builtin_clzl(__CPROVER_max_malloc_size);
257 __CPROVER_size_t nof_objects = 1UL << object_bits;
258#endif
260 .max_elems = nof_objects,
261 .watermark = 0,
262 .nof_elems = 0,
263 .is_empty = 1,
264 .indexed_by_object_id = 1,
265 .elems = __CPROVER_allocate(nof_objects * sizeof(*(set->elems)), 1)};
266}
267
275 __CPROVER_size_t max_elems)
276{
277__CPROVER_HIDE:;
278#ifdef DFCC_DEBUG
281 "set writable");
282#endif
284 .max_elems = max_elems,
285 .watermark = 0,
286 .nof_elems = 0,
287 .is_empty = 1,
288 .indexed_by_object_id = 0,
289 .elems = __CPROVER_allocate(max_elems * sizeof(*(set->elems)), 1)};
290}
291
294{
295__CPROVER_HIDE:;
296#ifdef DFCC_DEBUG
299 "set readable");
300 __CPROVER_assert(__CPROVER_rw_ok(&(set->elems), 0), "set->elems writable");
301#endif
303}
304
311 void *ptr)
312{
313__CPROVER_HIDE:;
314 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
315#ifdef DFCC_DEBUG
316 __CPROVER_assert(set->indexed_by_object_id, "indexed by object id");
317 __CPROVER_assert(object_id < set->max_elems, "no OOB access");
318#endif
319 set->nof_elems = set->elems[object_id] ? set->nof_elems : set->nof_elems + 1;
320 set->elems[object_id] = ptr;
321 set->is_empty = 0;
322}
323
330 void *ptr)
331{
332__CPROVER_HIDE:;
333#ifdef DFCC_DEBUG
334 __CPROVER_assert(!(set->indexed_by_object_id), "not indexed by object id");
335 __CPROVER_assert(set->watermark < set->max_elems, "no OOB access");
336#endif
337 set->nof_elems = set->watermark;
338 set->elems[set->watermark] = ptr;
339 set->watermark += 1;
340 set->is_empty = 0;
341}
342
349 void *ptr)
350{
351__CPROVER_HIDE:;
352 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
353#ifdef DFCC_DEBUG
354 __CPROVER_assert(set->indexed_by_object_id, "indexed by object id");
355 __CPROVER_assert(object_id < set->max_elems, "no OOB access");
356#endif
357 set->nof_elems = set->elems[object_id] ? set->nof_elems - 1 : set->nof_elems;
358 set->is_empty = set->nof_elems == 0;
359 set->elems[object_id] = 0;
360}
361
369 void *ptr)
370{
371__CPROVER_HIDE:;
372 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
373#ifdef DFCC_DEBUG
374 __CPROVER_assert(set->indexed_by_object_id, "indexed by object id");
375 __CPROVER_assert(object_id < set->max_elems, "no OOB access");
376#endif
377 return set->elems[object_id] != 0;
378}
379
386 void *ptr)
387{
388__CPROVER_HIDE:;
389 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
390#ifdef DFCC_DEBUG
391 __CPROVER_assert(set->indexed_by_object_id, "indexed by object id");
392 __CPROVER_assert(object_id < set->max_elems, "no OOB access");
393#endif
394 return set->elems[object_id] == ptr;
395}
396
415 __CPROVER_size_t contract_assigns_size,
416 __CPROVER_size_t contract_frees_size,
417 __CPROVER_bool assume_requires_ctx,
418 __CPROVER_bool assert_requires_ctx,
419 __CPROVER_bool assume_ensures_ctx,
420 __CPROVER_bool assert_ensures_ctx,
421 __CPROVER_bool allow_allocate,
422 __CPROVER_bool allow_deallocate)
423{
424__CPROVER_HIDE:;
425#ifdef DFCC_DEBUG
428 "set writable");
429#endif
431 &(set->contract_assigns), contract_assigns_size);
433 &(set->contract_frees));
435 &(set->contract_frees_append), contract_frees_size);
438 set->linked_is_fresh = 0;
439 set->linked_allocated = 0;
440 set->linked_deallocated = 0;
441 set->assume_requires_ctx = assume_requires_ctx;
442 set->assert_requires_ctx = assert_requires_ctx;
443 set->assume_ensures_ctx = assume_ensures_ctx;
444 set->assert_ensures_ctx = assert_ensures_ctx;
445 set->allow_allocate = allow_allocate;
446 set->allow_deallocate = allow_deallocate;
447}
448
452{
453__CPROVER_HIDE:;
454#ifdef DFCC_DEBUG
457 "set readable");
460 "contract_assigns writable");
463 "contract_frees writable");
466 "contract_frees_append writable");
468 __CPROVER_rw_ok(&(set->allocated.elems), 0), "allocated writable");
470 __CPROVER_rw_ok(&(set->deallocated.elems), 0), "deallocated writable");
471#endif
477 // do not free set->linked_is_fresh->elems or set->deallocated_linked->elems
478 // since they are owned by someone else.
479}
480
489 __CPROVER_size_t idx,
490 void *ptr,
491 __CPROVER_size_t size)
492{
493__CPROVER_HIDE:;
495}
496
509 __CPROVER_size_t idx,
510 void *ptr)
511{
512__CPROVER_HIDE:;
514 &(set->contract_assigns),
515 idx,
516 ((char *)ptr) - __CPROVER_POINTER_OFFSET(ptr),
518}
519
533 __CPROVER_size_t idx,
534 void *ptr)
535{
537 &(set->contract_assigns),
538 idx,
539 ptr,
541}
542
555 __CPROVER_size_t idx,
556 void *ptr,
557 __CPROVER_size_t size)
558{
559__CPROVER_HIDE:;
561}
562
568 void *ptr)
569{
570__CPROVER_HIDE:;
571 // we don't check yet that the pointer satisfies
572 // the __CPROVER_contracts_is_freeable as precondition.
573 // preconditions will be checked if there is an actual attempt
574 // to free the pointer.
575
576 // store pointer
577 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
578#ifdef DFCC_DEBUG
579 // manually inlined below
581 __CPROVER_assert(object_id < set->contract_frees.max_elems, "no OOB access");
582#else
583 set->contract_frees.nof_elems = (set->contract_frees.elems[object_id] != 0)
585 : set->contract_frees.nof_elems + 1;
586 set->contract_frees.elems[object_id] = ptr;
587 set->contract_frees.is_empty = 0;
588#endif
589
590 // append pointer if available
591#ifdef DFCC_DEBUG
593#else
598#endif
599}
600
606 void *ptr)
607{
608__CPROVER_HIDE:;
609 __CPROVER_assert(set->allow_allocate, "dynamic allocation is allowed");
610#if DFCC_DEBUG
611 // call inlined below
613#else
614 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
615 set->allocated.nof_elems = (set->allocated.elems[object_id] != 0)
616 ? set->allocated.nof_elems
617 : set->allocated.nof_elems + 1;
618 set->allocated.elems[object_id] = ptr;
619 set->allocated.is_empty = 0;
620#endif
621}
622
628 void *ptr)
629{
630__CPROVER_HIDE:;
631#if DFCC_DEBUG
632 // call inlined below
634#else
635 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
636 set->allocated.nof_elems = (set->allocated.elems[object_id] != 0)
637 ? set->allocated.nof_elems
638 : set->allocated.nof_elems + 1;
639 set->allocated.elems[object_id] = ptr;
640 set->allocated.is_empty = 0;
641#endif
642}
643
653 void *ptr)
654{
655__CPROVER_HIDE:;
656#ifdef DFCC_DEBUG
657 // manually inlined below
659#else
660 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
661 set->allocated.nof_elems = set->allocated.elems[object_id]
662 ? set->allocated.nof_elems - 1
663 : set->allocated.nof_elems;
664 set->allocated.is_empty = set->allocated.nof_elems == 0;
665 set->allocated.elems[object_id] = 0;
666#endif
667}
668
678 void *ptr)
679{
680__CPROVER_HIDE:;
681#if DFCC_DEBUG
682 // we record the deallocation to be able to evaluate was_freed post conditions
687 // Manually inlined below
688#else
689 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
690
691 // __CPROVER_contracts_obj_set_add
692 set->deallocated.nof_elems = set->deallocated.elems[object_id]
694 : set->deallocated.nof_elems + 1;
695 set->deallocated.elems[object_id] = ptr;
696 set->deallocated.is_empty = 0;
697
698 // __CPROVER_contracts_obj_set_remove
699 set->allocated.nof_elems = set->allocated.elems[object_id]
700 ? set->allocated.nof_elems - 1
701 : set->allocated.nof_elems;
702 set->allocated.is_empty = set->allocated.nof_elems == 0;
703 set->allocated.elems[object_id] = 0;
704
705 // __CPROVER_contracts_obj_set_remove
706 set->contract_frees.nof_elems = set->contract_frees.elems[object_id]
707 ? set->contract_frees.nof_elems - 1
710 set->contract_frees.elems[object_id] = 0;
711
712 // __CPROVER_contracts_car_set_remove
713 __CPROVER_size_t idx = set->contract_assigns.max_elems;
715 while(idx != 0)
716 {
717 if(object_id == __CPROVER_POINTER_OBJECT(elem->lb))
718 elem->is_writable = 0;
719 ++elem;
720 --idx;
721 }
722#endif
723}
724
729__CPROVER_bool
736
747 void *ptr,
748 __CPROVER_size_t size)
749#if DFCC_DEBUG
750// manually inlined below
751{
752__CPROVER_HIDE:;
754 ((ptr == 0) | __CPROVER_rw_ok(ptr, size)),
755 "ptr NULL or writable up to size");
756
758 (ptr == 0) | (__CPROVER_POINTER_OBJECT(ptr) < set->allocated.max_elems),
759 "no OOB access");
760
762 if(!car.is_writable)
763 return 0;
764
765 if(set->allocated.elems[__CPROVER_POINTER_OBJECT(ptr)] != 0)
766 return 1;
767
769}
770#else
771{
772__CPROVER_HIDE:;
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"
781 ((ptr == 0) | __CPROVER_rw_ok(ptr, size)),
782 "ptr NULL or writable up to size");
783
784 // the range is not writable
785 if(ptr == 0)
786 return 0;
787
788 // is ptr pointing within some a locally allocated object ?
789 if(set->allocated.elems[__CPROVER_POINTER_OBJECT(ptr)] != 0)
790 return 1;
791
792 // don't even drive symex into the rest of the function if the set is empty
793 if(set->contract_assigns.max_elems == 0)
794 return 0;
795
796 // Compute the upper bound, perform inclusion check against contract-assigns
799 "CAR size is less than __CPROVER_max_malloc_size");
800
801 __CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(ptr);
802
804 !(offset > 0) | (offset + size <= __CPROVER_max_malloc_size),
805 "no offset bits overflow on CAR upper bound computation");
806 void *ub = (void *)((char *)ptr + size);
808 __CPROVER_size_t idx = set->contract_assigns.max_elems;
809 __CPROVER_bool incl = 0;
810
811SET_CHECK_ASSIGNMENT_LOOP:
812 while(idx != 0)
813 {
814 incl |=
815 (int)elem->is_writable & (int)__CPROVER_same_object(elem->lb, ptr) &
816 (__CPROVER_POINTER_OFFSET(elem->lb) <= offset) &
818 ++elem;
819 --idx;
820 }
821 return incl;
822# pragma CPROVER check pop
823}
824#endif
825
839 void *dest)
840{
841__CPROVER_HIDE:;
843 set, dest, __CPROVER_OBJECT_SIZE(dest) - __CPROVER_POINTER_OFFSET(dest));
844}
845
859 void *dest)
860{
861__CPROVER_HIDE:;
863 set, dest, __CPROVER_OBJECT_SIZE(dest) - __CPROVER_POINTER_OFFSET(dest));
864}
865
882 void *dest,
883 void *src)
884{
885__CPROVER_HIDE:;
886 __CPROVER_size_t src_size =
888 __CPROVER_size_t dest_size =
890 __CPROVER_size_t size = dest_size < src_size ? dest_size : src_size;
892}
893
904 void *ptr)
905{
906__CPROVER_HIDE:;
908 set,
909 (char *)ptr - __CPROVER_POINTER_OFFSET(ptr),
911}
912
925 void *ptr)
926{
927__CPROVER_HIDE:;
928 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
929
930#ifdef DFCC_DEBUG
933 "set->contract_frees is indexed by object id");
936 "set->allocated is indexed by object id");
937#endif
938 return (set->allow_deallocate) &
939 ((ptr == 0) | (set->contract_frees.elems[object_id] == ptr) |
940 (set->allocated.elems[object_id] == ptr));
941}
942
955{
956__CPROVER_HIDE:;
957 __CPROVER_bool incl = 1;
959 __CPROVER_size_t idx = candidate->contract_assigns.max_elems;
960SET_CHECK_ASSIGNS_CLAUSE_INCLUSION_LOOP:
961 while(idx != 0)
962 {
963 if(current->is_writable)
964 {
966 reference, current->lb, current->size);
967 }
968 --idx;
969 ++current;
970 }
971 return incl;
972}
973
986{
987__CPROVER_HIDE:;
988#ifdef DFCC_DEBUG
991 "reference->contract_frees is indexed by object id");
994 "reference->allocated is indexed by object id");
995#endif
996 __CPROVER_bool all_incl = 1;
997 void **current = candidate->contract_frees_append.elems;
998 __CPROVER_size_t idx = candidate->contract_frees_append.max_elems;
999
1000SET_CHECK_FREES_CLAUSE_INCLUSION_LOOP:
1001 while(idx != 0)
1002 {
1003 void *ptr = *current;
1004 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
1005 all_incl &= (ptr == 0) |
1006 (reference->contract_frees.elems[object_id] == ptr) |
1007 (reference->allocated.elems[object_id] == ptr);
1008 --idx;
1009 ++current;
1010 }
1011
1012 return all_incl;
1013}
1014
1019__CPROVER_bool
1021
1031{
1032__CPROVER_HIDE:;
1033 void **current = set->contract_frees_append.elems;
1034 __CPROVER_size_t idx = set->contract_frees_append.max_elems;
1035SET_DEALLOCATE_FREEABLE_LOOP:
1036 while(idx != 0)
1037 {
1038 void *ptr = *current;
1039
1040 // call free only iff the pointer is valid preconditions are met
1041 // skip checks on r_ok, dynamic_object and pointer_offset
1042 __CPROVER_bool preconditions =
1043 (ptr == 0) |
1044 ((int)__CPROVER_r_ok(ptr, 0) & (int)__CPROVER_DYNAMIC_OBJECT(ptr) &
1045 (__CPROVER_POINTER_OFFSET(ptr) == 0));
1046 // If there is aliasing between the pointers in the freeable set,
1047 // and we attempt to free again one of the already freed pointers,
1048 // the r_ok condition above will fail, preventing us to deallocate
1049 // the same pointer twice
1050 if((ptr != 0) & preconditions & __VERIFIER_nondet___CPROVER_bool())
1051 {
1054 // also record effects in the caller write set
1055 if(target != 0)
1057 }
1058 --idx;
1059 ++current;
1060 }
1061}
1062
1069{
1070__CPROVER_HIDE:;
1071#ifdef DFCC_DEBUG
1072 __CPROVER_assert(write_set != 0, "write_set not NULL");
1073#endif
1074 if((is_fresh_set != 0))
1075 {
1076 write_set->linked_is_fresh = is_fresh_set;
1077 }
1078 else
1079 {
1080 write_set->linked_is_fresh = 0;
1081 }
1082}
1083
1089 __CPROVER_contracts_write_set_ptr_t write_set_postconditions,
1090 __CPROVER_contracts_write_set_ptr_t write_set_to_link)
1091{
1092__CPROVER_HIDE:;
1093#ifdef DFCC_DEBUG
1095 write_set_postconditions != 0, "write_set_postconditions not NULL");
1096#endif
1097 if((write_set_to_link != 0))
1098 {
1099 write_set_postconditions->linked_allocated =
1100 &(write_set_to_link->allocated);
1101 }
1102 else
1103 {
1104 write_set_postconditions->linked_allocated = 0;
1105 }
1106}
1107
1114 __CPROVER_contracts_write_set_ptr_t write_set_postconditions,
1115 __CPROVER_contracts_write_set_ptr_t write_set_to_link)
1116{
1117__CPROVER_HIDE:;
1118#ifdef DFCC_DEBUG
1120 write_set_postconditions != 0, "write_set_postconditions not NULL");
1121#endif
1122 if((write_set_to_link != 0))
1123 {
1124 write_set_postconditions->linked_deallocated =
1125 &(write_set_to_link->deallocated);
1126 }
1127 else
1128 {
1129 write_set_postconditions->linked_deallocated = 0;
1130 }
1131}
1132
1137 __CPROVER_size_t,
1139
1161 void **elem,
1162 __CPROVER_size_t size,
1164{
1165__CPROVER_HIDE:;
1167 (write_set != 0) & ((write_set->assume_requires_ctx == 1) |
1168 (write_set->assert_requires_ctx == 1) |
1169 (write_set->assume_ensures_ctx == 1) |
1170 (write_set->assert_ensures_ctx == 1)),
1171 "__CPROVER_is_fresh is used only in requires or ensures clauses");
1172#ifdef DFCC_DEBUG
1175 "set readable");
1177 write_set->linked_is_fresh, "set->linked_is_fresh is not NULL");
1178#endif
1179 if(write_set->assume_requires_ctx)
1180 {
1181#ifdef DFCC_DEBUG
1183 (write_set->assert_requires_ctx == 0) &
1184 (write_set->assume_ensures_ctx == 0) &
1185 (write_set->assert_ensures_ctx == 0),
1186 "only one context flag at a time");
1187#endif
1188 if(
1191 {
1192 // When --malloc-may-fail --malloc-fail-null
1193 // add implicit assumption that the size is capped
1195 }
1196 else if(
1199 {
1200 // When --malloc-may-fail --malloc-fail-assert
1201 // check if max allocation size is exceeded and
1202 // add implicit assumption that the size is capped
1205 "__CPROVER_is_fresh max allocation size exceeded");
1207 }
1208
1209 void *ptr = __CPROVER_allocate(size, 0);
1210 *elem = ptr;
1211
1212 // record the object size for non-determistic bounds checking
1213 __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
1215 record_malloc ? 0 : __CPROVER_malloc_is_new_array;
1216
1217 // do not detect memory leaks when assuming a precondition of a contract
1218 // for contract checking
1219 // __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
1220 // __CPROVER_memory_leak = record_may_leak ? ptr : __CPROVER_memory_leak;
1221
1222 // record fresh object in the object set
1223#ifdef DFCC_DEBUG
1224 // manually inlined below
1226#else
1227 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
1228 write_set->linked_is_fresh->nof_elems =
1229 (write_set->linked_is_fresh->elems[object_id] != 0)
1230 ? write_set->linked_is_fresh->nof_elems
1231 : write_set->linked_is_fresh->nof_elems + 1;
1232 write_set->linked_is_fresh->elems[object_id] = ptr;
1233 write_set->linked_is_fresh->is_empty = 0;
1234#endif
1235 return 1;
1236 }
1237 else if(write_set->assume_ensures_ctx)
1238 {
1239#ifdef DFCC_DEBUG
1241 (write_set->assume_requires_ctx == 0) &
1242 (write_set->assert_requires_ctx == 0) &
1243 (write_set->assert_ensures_ctx == 0),
1244 "only one context flag at a time");
1245#endif
1246 // fail if size is too big
1247 if(
1250 {
1252 }
1253 else if(
1256 {
1259 "__CPROVER_is_fresh requires size <= __CPROVER_max_malloc_size");
1261 }
1262
1263 void *ptr = __CPROVER_allocate(size, 0);
1264 *elem = ptr;
1265
1266 // record the object size for non-determistic bounds checking
1267 __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
1269 record_malloc ? 0 : __CPROVER_malloc_is_new_array;
1270
1271 // detect memory leaks when is_fresh is assumed in a post condition
1272 // of a replaced contract to model a malloc performed by the function
1273 // being abstracted by the contract
1274 __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
1275 __CPROVER_memory_leak = record_may_leak ? ptr : __CPROVER_memory_leak;
1276
1277 // record fresh object in the caller's write set
1278#ifdef DFCC_DEBUG
1280#else
1281 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
1282 write_set->linked_allocated->nof_elems =
1283 (write_set->linked_allocated->elems[object_id] != 0)
1284 ? write_set->linked_allocated->nof_elems
1285 : write_set->linked_allocated->nof_elems + 1;
1286 write_set->linked_allocated->elems[object_id] = ptr;
1287 write_set->linked_allocated->is_empty = 0;
1288#endif
1289 return 1;
1290 }
1291 else if(write_set->assert_requires_ctx | write_set->assert_ensures_ctx)
1292 {
1293#ifdef DFCC_DEBUG
1295 (write_set->assume_requires_ctx == 0) &
1296 (write_set->assume_ensures_ctx == 0),
1297 "only one context flag at a time");
1298#endif
1300 void *ptr = *elem;
1301 // null pointers or already seen pointers are not fresh
1302#ifdef DFCC_DEBUG
1303 // manually inlined below
1304 if((ptr == 0) || (__CPROVER_contracts_obj_set_contains(seen, ptr)))
1305 return 0;
1306#else
1307 if(ptr == 0)
1308 return 0;
1309
1310 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
1311
1312 if(seen->elems[object_id] != 0)
1313 return 0;
1314#endif
1315 // record fresh object in the object set
1316#ifdef DFCC_DEBUG
1317 // manually inlined below
1319#else
1320 seen->nof_elems =
1321 (seen->elems[object_id] != 0) ? seen->nof_elems : seen->nof_elems + 1;
1322 seen->elems[object_id] = ptr;
1323 seen->is_empty = 0;
1324#endif
1325 // check size
1326 return __CPROVER_r_ok(ptr, size);
1327 }
1328 else
1329 {
1331 0, "__CPROVER_is_fresh is only called in requires or ensures clauses");
1333 return 0; // to silence libcheck
1334 }
1335}
1336
1338 void *lb,
1339 void **ptr,
1340 void *ub,
1342{
1343__CPROVER_HIDE:;
1345 (write_set != 0) & ((write_set->assume_requires_ctx == 1) |
1346 (write_set->assert_requires_ctx == 1) |
1347 (write_set->assume_ensures_ctx == 1) |
1348 (write_set->assert_ensures_ctx == 1)),
1349 "__CPROVER_pointer_in_range_dfcc is used only in requires or ensures "
1350 "clauses");
1351 __CPROVER_assert(__CPROVER_r_ok(lb, 0), "lb pointer must be valid");
1352 __CPROVER_assert(__CPROVER_r_ok(ub, 0), "ub pointer must be valid");
1354 __CPROVER_same_object(lb, ub),
1355 "lb and ub pointers must have the same object");
1356 __CPROVER_size_t lb_offset = __CPROVER_POINTER_OFFSET(lb);
1357 __CPROVER_size_t ub_offset = __CPROVER_POINTER_OFFSET(ub);
1359 lb_offset <= ub_offset, "lb and ub pointers must be ordered");
1360 if(write_set->assume_requires_ctx | write_set->assume_ensures_ctx)
1361 {
1363 return 0;
1364
1365 // add nondet offset
1366 __CPROVER_size_t offset = __VERIFIER_nondet_size();
1367
1368 // this cast is safe because we prove that ub and lb are ordered
1369 __CPROVER_size_t max_offset = ub_offset - lb_offset;
1370 __CPROVER_assume(offset <= max_offset);
1371 *ptr = (char *)lb + offset;
1372 return 1;
1373 }
1374 else /* write_set->assert_requires_ctx | write_set->assert_ensures_ctx */
1375 {
1376 __CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(*ptr);
1377 return __CPROVER_same_object(lb, *ptr) && lb_offset <= offset &&
1378 offset <= ub_offset;
1379 }
1380}
1381
1386 __CPROVER_size_t idx)
1387{
1388__CPROVER_HIDE:;
1389#ifdef DFCC_DEBUG
1390 __CPROVER_assert(write_set != 0, "write_set not NULL");
1391#endif
1392
1394 if(car.is_writable)
1395 return car.lb;
1396 else
1397 return (void *)0;
1398}
1399
1405 __CPROVER_size_t idx)
1406{
1407__CPROVER_HIDE:;
1408 __CPROVER_assert(idx < set->contract_assigns.max_elems, "no OOB access");
1410 if(car.is_writable)
1412}
1413
1418 __CPROVER_size_t idx)
1419{
1420__CPROVER_HIDE:;
1421#ifdef DFCC_DEBUG
1422 __CPROVER_assert(idx < set->contract_assigns.max_elems, "no OOB access");
1423#endif
1425 if(car.is_writable)
1426 __CPROVER_havoc_slice(car.lb, car.size);
1427}
1428
1440 void *ptr,
1442{
1443__CPROVER_HIDE:;
1445 (set != 0) &
1446 ((set->assume_requires_ctx == 1) | (set->assert_requires_ctx == 1) |
1447 (set->assume_ensures_ctx == 1) | (set->assert_ensures_ctx == 1)),
1448 "__CPROVER_is_freeable is used only in requires or ensures clauses");
1449
1450 // These are all the preconditions checked by `free` of the CPROVER library
1451 __CPROVER_bool is_dynamic_object = (ptr == 0) | __CPROVER_DYNAMIC_OBJECT(ptr);
1452 __CPROVER_bool has_offset_zero =
1453 (ptr == 0) | (__CPROVER_POINTER_OFFSET(ptr) == 0);
1454
1455 if((set->assume_requires_ctx == 1) || (set->assume_ensures_ctx == 1))
1456 return is_dynamic_object & has_offset_zero;
1457
1458 // these conditions cannot be used in assumptions since they involve
1459 // demonic non-determinism
1460 __CPROVER_bool is_null_or_valid_pointer = (ptr == 0) | __CPROVER_r_ok(ptr, 0);
1461 __CPROVER_bool is_not_deallocated =
1462 (ptr == 0) | (__CPROVER_deallocated != ptr);
1463 __CPROVER_bool is_not_alloca = (ptr == 0) | (__CPROVER_alloca_object != ptr);
1464 __CPROVER_bool is_not_array = (ptr == 0) | (__CPROVER_new_object != ptr) |
1466 return is_null_or_valid_pointer & is_dynamic_object & has_offset_zero &
1467 is_not_deallocated & is_not_alloca & is_not_array;
1468}
1469
1472 void *ptr,
1474{
1475__CPROVER_HIDE:;
1477 (set != 0) &
1478 ((set->assume_ensures_ctx == 1) | (set->assert_ensures_ctx == 1)),
1479 "__CPROVER_was_freed is used only in ensures clauses");
1481 (set->linked_deallocated != 0), "linked_deallocated is not null");
1482#ifdef DFCC_DEBUG
1483 // manually inlined below
1485 set->linked_deallocated, ptr);
1486#else
1487 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
1488 return set->linked_deallocated->elems[object_id] == ptr;
1489#endif
1490}
1491
1498 void *ptr,
1500{
1501__CPROVER_HIDE:;
1503 set && ((set->assume_ensures_ctx == 1) | (set->assert_ensures_ctx == 1)),
1504 "__CPROVER_was_freed is used only in ensures clauses");
1505
1506 if(set->assume_ensures_ctx)
1507 {
1508#ifdef DFCC_DEBUG
1509 // manually inlined below
1512 "assuming __CPROVER_was_freed(ptr) requires ptr to always exist in the "
1513 "contract's frees clause");
1514#else
1515 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
1517 set->contract_frees.elems[object_id] == ptr,
1518 "assuming __CPROVER_was_freed(ptr) requires ptr to always exist in the "
1519 "contract's frees clause");
1520#endif
1521 }
1522}
1523
1533 void (**function_pointer)(void),
1534 void (*contract)(void),
1536{
1537__CPROVER_HIDE:;
1539 (set != 0) &
1540 ((set->assume_requires_ctx == 1) | (set->assert_requires_ctx == 1) |
1541 (set->assume_ensures_ctx == 1) | (set->assert_ensures_ctx == 1)),
1542 "__CPROVER_obeys_contract is used only in requires or ensures clauses");
1543 if((set->assume_requires_ctx == 1) | (set->assume_ensures_ctx == 1))
1544 {
1545 // decide if predicate must hold
1547 return 0;
1548
1549 // must hold, assign the function pointer to the contract function
1550 *function_pointer = contract;
1551 return 1;
1552 }
1553 else
1554 {
1555 // in assumption contexts, the pointer gets checked for equality
1556 return *function_pointer == contract;
1557 }
1558}
1559#endif // __CPROVER_contracts_library_defined
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 *,...)
__CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *)
void __CPROVER_assert(__CPROVER_bool assertion, const char *description)
void __CPROVER_havoc_slice(void *, __CPROVER_size_t)
__CPROVER_size_t __CPROVER_POINTER_OFFSET(const void *)
__CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *)
__CPROVER_bool __CPROVER_same_object(const void *, const void *)
__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *)
void __CPROVER_assume(__CPROVER_bool assumption)
void __CPROVER_havoc_object(void *)
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.
int __builtin_clzll(unsigned long long)
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)