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
11extern const void *__CPROVER_deallocated;
12const void *__CPROVER_new_object = 0;
13extern const void *__CPROVER_memory_leak;
15#if defined(_WIN32) && defined(_M_X64)
16int __builtin_clzll(unsigned long long);
17#else
18int __builtin_clzl(unsigned long);
19#endif
21__CPROVER_size_t __VERIFIER_nondet_size(void);
22
24typedef struct
25{
27 unsigned char is_writable;
29 __CPROVER_size_t size;
31 void *lb;
33 void *ub;
35
44
47
49typedef struct
50{
52 __CPROVER_size_t max_elems;
55 __CPROVER_size_t watermark;
57 __CPROVER_size_t nof_elems;
59 unsigned char is_empty;
61 unsigned char indexed_by_object_id;
64 void **elems;
66
69
105
108
114__CPROVER_contracts_car_create(void *ptr, __CPROVER_size_t size)
115{
116__CPROVER_HIDE:;
118 ((ptr == 0) | __CPROVER_rw_ok(ptr, size)),
119 "ptr NULL or writable up to size");
122 "CAR size is less than __CPROVER_max_malloc_size");
123 __CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(ptr);
125 !(offset > 0) | (offset + size <= __CPROVER_max_malloc_size),
126 "no offset bits overflow on CAR upper bound computation");
128 .is_writable = ptr != 0, .size = size, .lb = ptr, .ub = (char *)ptr + size};
129}
130
136 __CPROVER_size_t max_elems)
137{
138__CPROVER_HIDE:;
139#ifdef DFCC_DEBUG
142 "set writable");
143#endif
144 set->max_elems = max_elems;
145 set->elems =
146 __CPROVER_allocate(max_elems * sizeof(__CPROVER_contracts_car_t), 1);
147}
148
157 __CPROVER_size_t idx,
158 void *ptr,
159 __CPROVER_size_t size)
160{
161__CPROVER_HIDE:;
162#ifdef DFCC_DEBUG
163 __CPROVER_assert((set != 0) & (idx < set->max_elems), "no OOB access");
164#endif
166 ((ptr == 0) | __CPROVER_rw_ok(ptr, size)),
167 "ptr NULL or writable up to size");
170 "CAR size is less than __CPROVER_max_malloc_size");
171 __CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(ptr);
173 !(offset > 0) | (offset + size <= __CPROVER_max_malloc_size),
174 "no offset bits overflow on CAR upper bound computation");
175 __CPROVER_contracts_car_t *elem = set->elems + idx;
177 .is_writable = ptr != 0, .size = size, .lb = ptr, .ub = (char *)ptr + size};
178}
179
186 void *ptr)
187{
188__CPROVER_HIDE:;
189 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
190 __CPROVER_size_t idx = set->max_elems;
191 __CPROVER_contracts_car_t *elem = set->elems;
192CAR_SET_REMOVE_LOOP:
193 while(idx != 0)
194 {
195 if(object_id == __CPROVER_POINTER_OBJECT(elem->lb))
196 elem->is_writable = 0;
197 ++elem;
198 --idx;
199 }
200}
201
209{
210__CPROVER_HIDE:;
211 __CPROVER_bool incl = 0;
212 __CPROVER_size_t idx = set->max_elems;
213 __CPROVER_contracts_car_t *elem = set->elems;
214CAR_SET_CONTAINS_LOOP:
215 while(idx != 0)
216 {
217 incl |= (int)candidate.is_writable & (int)elem->is_writable &
218 (int)__CPROVER_same_object(elem->lb, candidate.lb) &
220 __CPROVER_POINTER_OFFSET(candidate.lb)) &
221 (__CPROVER_POINTER_OFFSET(candidate.ub) <=
223 ++elem;
224 --idx;
225 }
226
227 return incl;
228}
229
240{
241__CPROVER_HIDE:;
242#ifdef DFCC_DEBUG
245 "set writable");
246#endif
247 // compute the maximum number of objects that can exist in the
248 // symex state from the number of object_bits/offset_bits
249 // the number of object bits is determined by counting the number of leading
250 // zeroes of the built-in constant __CPROVER_max_malloc_size;
251#if defined(_WIN32) && defined(_M_X64)
253 __CPROVER_size_t nof_objects = 1ULL << object_bits;
254#else
255 int object_bits = __builtin_clzl(__CPROVER_max_malloc_size);
256 __CPROVER_size_t nof_objects = 1UL << object_bits;
257#endif
259 .max_elems = nof_objects,
260 .watermark = 0,
261 .nof_elems = 0,
262 .is_empty = 1,
263 .indexed_by_object_id = 1,
264 .elems = __CPROVER_allocate(nof_objects * sizeof(*(set->elems)), 1)};
265}
266
274 __CPROVER_size_t max_elems)
275{
276__CPROVER_HIDE:;
277#ifdef DFCC_DEBUG
280 "set writable");
281#endif
283 .max_elems = max_elems,
284 .watermark = 0,
285 .nof_elems = 0,
286 .is_empty = 1,
287 .indexed_by_object_id = 0,
288 .elems = __CPROVER_allocate(max_elems * sizeof(*(set->elems)), 1)};
289}
290
293{
294__CPROVER_HIDE:;
295#ifdef DFCC_DEBUG
298 "set readable");
299 __CPROVER_assert(__CPROVER_rw_ok(&(set->elems), 0), "set->elems writable");
300#endif
302}
303
310 void *ptr)
311{
312__CPROVER_HIDE:;
313 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
314#ifdef DFCC_DEBUG
315 __CPROVER_assert(set->indexed_by_object_id, "indexed by object id");
316 __CPROVER_assert(object_id < set->max_elems, "no OOB access");
317#endif
318 set->nof_elems = set->elems[object_id] ? set->nof_elems : set->nof_elems + 1;
319 set->elems[object_id] = ptr;
320 set->is_empty = 0;
321}
322
329 void *ptr)
330{
331__CPROVER_HIDE:;
332#ifdef DFCC_DEBUG
333 __CPROVER_assert(!(set->indexed_by_object_id), "not indexed by object id");
334 __CPROVER_assert(set->watermark < set->max_elems, "no OOB access");
335#endif
336 set->nof_elems = set->watermark;
337 set->elems[set->watermark] = ptr;
338 set->watermark += 1;
339 set->is_empty = 0;
340}
341
348 void *ptr)
349{
350__CPROVER_HIDE:;
351 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
352#ifdef DFCC_DEBUG
353 __CPROVER_assert(set->indexed_by_object_id, "indexed by object id");
354 __CPROVER_assert(object_id < set->max_elems, "no OOB access");
355#endif
356 set->nof_elems = set->elems[object_id] ? set->nof_elems - 1 : set->nof_elems;
357 set->is_empty = set->nof_elems == 0;
358 set->elems[object_id] = 0;
359}
360
368 void *ptr)
369{
370__CPROVER_HIDE:;
371 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
372#ifdef DFCC_DEBUG
373 __CPROVER_assert(set->indexed_by_object_id, "indexed by object id");
374 __CPROVER_assert(object_id < set->max_elems, "no OOB access");
375#endif
376 return set->elems[object_id] != 0;
377}
378
385 void *ptr)
386{
387__CPROVER_HIDE:;
388 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
389#ifdef DFCC_DEBUG
390 __CPROVER_assert(set->indexed_by_object_id, "indexed by object id");
391 __CPROVER_assert(object_id < set->max_elems, "no OOB access");
392#endif
393 return set->elems[object_id] == ptr;
394}
395
414 __CPROVER_size_t contract_assigns_size,
415 __CPROVER_size_t contract_frees_size,
416 __CPROVER_bool assume_requires_ctx,
417 __CPROVER_bool assert_requires_ctx,
418 __CPROVER_bool assume_ensures_ctx,
419 __CPROVER_bool assert_ensures_ctx,
420 __CPROVER_bool allow_allocate,
421 __CPROVER_bool allow_deallocate)
422{
423__CPROVER_HIDE:;
424#ifdef DFCC_DEBUG
427 "set writable");
428#endif
430 &(set->contract_assigns), contract_assigns_size);
432 &(set->contract_frees));
434 &(set->contract_frees_append), contract_frees_size);
437 set->linked_is_fresh = 0;
438 set->linked_allocated = 0;
439 set->linked_deallocated = 0;
440 set->assume_requires_ctx = assume_requires_ctx;
441 set->assert_requires_ctx = assert_requires_ctx;
442 set->assume_ensures_ctx = assume_ensures_ctx;
443 set->assert_ensures_ctx = assert_ensures_ctx;
444 set->allow_allocate = allow_allocate;
445 set->allow_deallocate = allow_deallocate;
446}
447
451{
452__CPROVER_HIDE:;
453#ifdef DFCC_DEBUG
456 "set readable");
459 "contract_assigns writable");
462 "contract_frees writable");
465 "contract_frees_append writable");
467 __CPROVER_rw_ok(&(set->allocated.elems), 0), "allocated writable");
469 __CPROVER_rw_ok(&(set->deallocated.elems), 0), "deallocated writable");
470#endif
476 // do not free set->linked_is_fresh->elems or set->deallocated_linked->elems
477 // since they are owned by someone else.
478}
479
488 __CPROVER_size_t idx,
489 void *ptr,
490 __CPROVER_size_t size)
491{
492__CPROVER_HIDE:;
494}
495
508 __CPROVER_size_t idx,
509 void *ptr)
510{
511__CPROVER_HIDE:;
513 &(set->contract_assigns),
514 idx,
515 ((char *)ptr) - __CPROVER_POINTER_OFFSET(ptr),
517}
518
532 __CPROVER_size_t idx,
533 void *ptr)
534{
536 &(set->contract_assigns),
537 idx,
538 ptr,
540}
541
554 __CPROVER_size_t idx,
555 void *ptr,
556 __CPROVER_size_t size)
557{
558__CPROVER_HIDE:;
560}
561
567 void *ptr)
568{
569__CPROVER_HIDE:;
570 // we don't check yet that the pointer satisfies
571 // the __CPROVER_contracts_is_freeable as precondition.
572 // preconditions will be checked if there is an actual attempt
573 // to free the pointer.
574
575 // store pointer
576 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
577#ifdef DFCC_DEBUG
578 // manually inlined below
580 __CPROVER_assert(object_id < set->contract_frees.max_elems, "no OOB access");
581#else
582 set->contract_frees.nof_elems = (set->contract_frees.elems[object_id] != 0)
584 : set->contract_frees.nof_elems + 1;
585 set->contract_frees.elems[object_id] = ptr;
586 set->contract_frees.is_empty = 0;
587#endif
588
589 // append pointer if available
590#ifdef DFCC_DEBUG
592#else
597#endif
598}
599
605 void *ptr)
606{
607__CPROVER_HIDE:;
608 __CPROVER_assert(set->allow_allocate, "dynamic allocation is allowed");
609#if DFCC_DEBUG
610 // call inlined below
612#else
613 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
614 set->allocated.nof_elems = (set->allocated.elems[object_id] != 0)
615 ? set->allocated.nof_elems
616 : set->allocated.nof_elems + 1;
617 set->allocated.elems[object_id] = ptr;
618 set->allocated.is_empty = 0;
619#endif
620}
621
627 void *ptr)
628{
629__CPROVER_HIDE:;
630#if DFCC_DEBUG
631 // call inlined below
633#else
634 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
635 set->allocated.nof_elems = (set->allocated.elems[object_id] != 0)
636 ? set->allocated.nof_elems
637 : set->allocated.nof_elems + 1;
638 set->allocated.elems[object_id] = ptr;
639 set->allocated.is_empty = 0;
640#endif
641}
642
652 void *ptr)
653{
654__CPROVER_HIDE:;
655#ifdef DFCC_DEBUG
656 // manually inlined below
658#else
659 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
660 set->allocated.nof_elems = set->allocated.elems[object_id]
661 ? set->allocated.nof_elems - 1
662 : set->allocated.nof_elems;
663 set->allocated.is_empty = set->allocated.nof_elems == 0;
664 set->allocated.elems[object_id] = 0;
665#endif
666}
667
677 void *ptr)
678{
679__CPROVER_HIDE:;
680#if DFCC_DEBUG
681 // we record the deallocation to be able to evaluate was_freed post conditions
686 // Manually inlined below
687#else
688 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
689
690 // __CPROVER_contracts_obj_set_add
691 set->deallocated.nof_elems = set->deallocated.elems[object_id]
693 : set->deallocated.nof_elems + 1;
694 set->deallocated.elems[object_id] = ptr;
695 set->deallocated.is_empty = 0;
696
697 // __CPROVER_contracts_obj_set_remove
698 set->allocated.nof_elems = set->allocated.elems[object_id]
699 ? set->allocated.nof_elems - 1
700 : set->allocated.nof_elems;
701 set->allocated.is_empty = set->allocated.nof_elems == 0;
702 set->allocated.elems[object_id] = 0;
703
704 // __CPROVER_contracts_obj_set_remove
705 set->contract_frees.nof_elems = set->contract_frees.elems[object_id]
706 ? set->contract_frees.nof_elems - 1
709 set->contract_frees.elems[object_id] = 0;
710
711 // __CPROVER_contracts_car_set_remove
712 __CPROVER_size_t idx = set->contract_assigns.max_elems;
714 while(idx != 0)
715 {
716 if(object_id == __CPROVER_POINTER_OBJECT(elem->lb))
717 elem->is_writable = 0;
718 ++elem;
719 --idx;
720 }
721#endif
722}
723
728__CPROVER_bool
735
746 void *ptr,
747 __CPROVER_size_t size)
748#if DFCC_DEBUG
749// manually inlined below
750{
751__CPROVER_HIDE:;
753 ((ptr == 0) | __CPROVER_rw_ok(ptr, size)),
754 "ptr NULL or writable up to size");
755
757 (ptr == 0) | (__CPROVER_POINTER_OBJECT(ptr) < set->allocated.max_elems),
758 "no OOB access");
759
761 if(!car.is_writable)
762 return 0;
763
764 if(set->allocated.elems[__CPROVER_POINTER_OBJECT(ptr)] != 0)
765 return 1;
766
768}
769#else
770{
771__CPROVER_HIDE:;
772# pragma CPROVER check push
773# pragma CPROVER check disable "pointer"
774# pragma CPROVER check disable "pointer-primitive"
775# pragma CPROVER check disable "unsigned-overflow"
776# pragma CPROVER check disable "signed-overflow"
777# pragma CPROVER check disable "undefined-shift"
778# pragma CPROVER check disable "conversion"
780 ((ptr == 0) | __CPROVER_rw_ok(ptr, size)),
781 "ptr NULL or writable up to size");
782
783 // the range is not writable
784 if(ptr == 0)
785 return 0;
786
787 // is ptr pointing within some a locally allocated object ?
788 if(set->allocated.elems[__CPROVER_POINTER_OBJECT(ptr)] != 0)
789 return 1;
790
791 // don't even drive symex into the rest of the function if the set is empty
792 if(set->contract_assigns.max_elems == 0)
793 return 0;
794
795 // Compute the upper bound, perform inclusion check against contract-assigns
798 "CAR size is less than __CPROVER_max_malloc_size");
799
800 __CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(ptr);
801
803 !(offset > 0) | (offset + size <= __CPROVER_max_malloc_size),
804 "no offset bits overflow on CAR upper bound computation");
805 void *ub = (void *)((char *)ptr + size);
807 __CPROVER_size_t idx = set->contract_assigns.max_elems;
808 __CPROVER_bool incl = 0;
809
810SET_CHECK_ASSIGNMENT_LOOP:
811 while(idx != 0)
812 {
813 incl |=
814 (int)elem->is_writable & (int)__CPROVER_same_object(elem->lb, ptr) &
815 (__CPROVER_POINTER_OFFSET(elem->lb) <= offset) &
817 ++elem;
818 --idx;
819 }
820 return incl;
821# pragma CPROVER check pop
822}
823#endif
824
838 void *dest)
839{
840__CPROVER_HIDE:;
842 set, dest, __CPROVER_OBJECT_SIZE(dest) - __CPROVER_POINTER_OFFSET(dest));
843}
844
858 void *dest)
859{
860__CPROVER_HIDE:;
862 set, dest, __CPROVER_OBJECT_SIZE(dest) - __CPROVER_POINTER_OFFSET(dest));
863}
864
881 void *dest,
882 void *src)
883{
884__CPROVER_HIDE:;
885 __CPROVER_size_t src_size =
887 __CPROVER_size_t dest_size =
889 __CPROVER_size_t size = dest_size < src_size ? dest_size : src_size;
891}
892
903 void *ptr)
904{
905__CPROVER_HIDE:;
907 set,
908 (char *)ptr - __CPROVER_POINTER_OFFSET(ptr),
910}
911
924 void *ptr)
925{
926__CPROVER_HIDE:;
927 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
928
929#ifdef DFCC_DEBUG
932 "set->contract_frees is indexed by object id");
935 "set->allocated is indexed by object id");
936#endif
937 return (set->allow_deallocate) &
938 ((ptr == 0) | (set->contract_frees.elems[object_id] == ptr) |
939 (set->allocated.elems[object_id] == ptr));
940}
941
954{
955__CPROVER_HIDE:;
956 __CPROVER_bool incl = 1;
958 __CPROVER_size_t idx = candidate->contract_assigns.max_elems;
959SET_CHECK_ASSIGNS_CLAUSE_INCLUSION_LOOP:
960 while(idx != 0)
961 {
962 if(current->is_writable)
963 {
965 reference, current->lb, current->size);
966 }
967 --idx;
968 ++current;
969 }
970 return incl;
971}
972
985{
986__CPROVER_HIDE:;
987#ifdef DFCC_DEBUG
990 "reference->contract_frees is indexed by object id");
993 "reference->allocated is indexed by object id");
994#endif
995 __CPROVER_bool all_incl = 1;
996 void **current = candidate->contract_frees_append.elems;
997 __CPROVER_size_t idx = candidate->contract_frees_append.max_elems;
998
999SET_CHECK_FREES_CLAUSE_INCLUSION_LOOP:
1000 while(idx != 0)
1001 {
1002 void *ptr = *current;
1003 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
1004 all_incl &= (ptr == 0) |
1005 (reference->contract_frees.elems[object_id] == ptr) |
1006 (reference->allocated.elems[object_id] == ptr);
1007 --idx;
1008 ++current;
1009 }
1010
1011 return all_incl;
1012}
1013
1018__CPROVER_bool
1020
1030{
1031__CPROVER_HIDE:;
1032 void **current = set->contract_frees_append.elems;
1033 __CPROVER_size_t idx = set->contract_frees_append.max_elems;
1034SET_DEALLOCATE_FREEABLE_LOOP:
1035 while(idx != 0)
1036 {
1037 void *ptr = *current;
1038
1039 // call free only iff the pointer is valid preconditions are met
1040 // skip checks on r_ok, dynamic_object and pointer_offset
1041 __CPROVER_bool preconditions =
1042 (ptr == 0) |
1043 ((int)__CPROVER_r_ok(ptr, 0) & (int)__CPROVER_DYNAMIC_OBJECT(ptr) &
1044 (__CPROVER_POINTER_OFFSET(ptr) == 0));
1045 // If there is aliasing between the pointers in the freeable set,
1046 // and we attempt to free again one of the already freed pointers,
1047 // the r_ok condition above will fail, preventing us to deallocate
1048 // the same pointer twice
1049 if((ptr != 0) & preconditions & __VERIFIER_nondet___CPROVER_bool())
1050 {
1053 // also record effects in the caller write set
1054 if(target != 0)
1056 }
1057 --idx;
1058 ++current;
1059 }
1060}
1061
1068{
1069__CPROVER_HIDE:;
1070#ifdef DFCC_DEBUG
1071 __CPROVER_assert(write_set != 0, "write_set not NULL");
1072#endif
1073 if((is_fresh_set != 0))
1074 {
1075 write_set->linked_is_fresh = is_fresh_set;
1076 }
1077 else
1078 {
1079 write_set->linked_is_fresh = 0;
1080 }
1081}
1082
1088 __CPROVER_contracts_write_set_ptr_t write_set_postconditions,
1089 __CPROVER_contracts_write_set_ptr_t write_set_to_link)
1090{
1091__CPROVER_HIDE:;
1092#ifdef DFCC_DEBUG
1094 write_set_postconditions != 0, "write_set_postconditions not NULL");
1095#endif
1096 if((write_set_to_link != 0))
1097 {
1098 write_set_postconditions->linked_allocated =
1099 &(write_set_to_link->allocated);
1100 }
1101 else
1102 {
1103 write_set_postconditions->linked_allocated = 0;
1104 }
1105}
1106
1113 __CPROVER_contracts_write_set_ptr_t write_set_postconditions,
1114 __CPROVER_contracts_write_set_ptr_t write_set_to_link)
1115{
1116__CPROVER_HIDE:;
1117#ifdef DFCC_DEBUG
1119 write_set_postconditions != 0, "write_set_postconditions not NULL");
1120#endif
1121 if((write_set_to_link != 0))
1122 {
1123 write_set_postconditions->linked_deallocated =
1124 &(write_set_to_link->deallocated);
1125 }
1126 else
1127 {
1128 write_set_postconditions->linked_deallocated = 0;
1129 }
1130}
1131
1136 __CPROVER_size_t,
1138
1160 void **elem,
1161 __CPROVER_size_t size,
1163{
1164__CPROVER_HIDE:;
1166 (write_set != 0) & ((write_set->assume_requires_ctx == 1) |
1167 (write_set->assert_requires_ctx == 1) |
1168 (write_set->assume_ensures_ctx == 1) |
1169 (write_set->assert_ensures_ctx == 1)),
1170 "__CPROVER_is_fresh is used only in requires or ensures clauses");
1171#ifdef DFCC_DEBUG
1174 "set readable");
1176 write_set->linked_is_fresh, "set->linked_is_fresh is not NULL");
1177#endif
1178 if(write_set->assume_requires_ctx)
1179 {
1180#ifdef DFCC_DEBUG
1182 (write_set->assert_requires_ctx == 0) &
1183 (write_set->assume_ensures_ctx == 0) &
1184 (write_set->assert_ensures_ctx == 0),
1185 "only one context flag at a time");
1186#endif
1187 if(
1190 {
1191 // When --malloc-may-fail --malloc-fail-null
1192 // add implicit assumption that the size is capped
1194 }
1195 else if(
1198 {
1199 // When --malloc-may-fail --malloc-fail-assert
1200 // check if max allocation size is exceeded and
1201 // add implicit assumption that the size is capped
1204 "__CPROVER_is_fresh max allocation size exceeded");
1206 }
1207
1208 void *ptr = __CPROVER_allocate(size, 0);
1209 *elem = ptr;
1210
1211 // record the object size for non-determistic bounds checking
1212 __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
1214 record_malloc ? 0 : __CPROVER_malloc_is_new_array;
1215
1216 // do not detect memory leaks when assuming a precondition of a contract
1217 // for contract checking
1218 // __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
1219 // __CPROVER_memory_leak = record_may_leak ? ptr : __CPROVER_memory_leak;
1220
1221 // record fresh object in the object set
1222#ifdef DFCC_DEBUG
1223 // manually inlined below
1225#else
1226 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
1227 write_set->linked_is_fresh->nof_elems =
1228 (write_set->linked_is_fresh->elems[object_id] != 0)
1229 ? write_set->linked_is_fresh->nof_elems
1230 : write_set->linked_is_fresh->nof_elems + 1;
1231 write_set->linked_is_fresh->elems[object_id] = ptr;
1232 write_set->linked_is_fresh->is_empty = 0;
1233#endif
1234 return 1;
1235 }
1236 else if(write_set->assume_ensures_ctx)
1237 {
1238#ifdef DFCC_DEBUG
1240 (write_set->assume_requires_ctx == 0) &
1241 (write_set->assert_requires_ctx == 0) &
1242 (write_set->assert_ensures_ctx == 0),
1243 "only one context flag at a time");
1244#endif
1245 // fail if size is too big
1246 if(
1249 {
1251 }
1252 else if(
1255 {
1258 "__CPROVER_is_fresh requires size <= __CPROVER_max_malloc_size");
1260 }
1261
1262 void *ptr = __CPROVER_allocate(size, 0);
1263 *elem = ptr;
1264
1265 // record the object size for non-determistic bounds checking
1266 __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
1268 record_malloc ? 0 : __CPROVER_malloc_is_new_array;
1269
1270 // detect memory leaks when is_fresh is assumed in a post condition
1271 // of a replaced contract to model a malloc performed by the function
1272 // being abstracted by the contract
1273 __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
1274 __CPROVER_memory_leak = record_may_leak ? ptr : __CPROVER_memory_leak;
1275
1276 // record fresh object in the caller's write set
1277#ifdef DFCC_DEBUG
1279#else
1280 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
1281 write_set->linked_allocated->nof_elems =
1282 (write_set->linked_allocated->elems[object_id] != 0)
1283 ? write_set->linked_allocated->nof_elems
1284 : write_set->linked_allocated->nof_elems + 1;
1285 write_set->linked_allocated->elems[object_id] = ptr;
1286 write_set->linked_allocated->is_empty = 0;
1287#endif
1288 return 1;
1289 }
1290 else if(write_set->assert_requires_ctx | write_set->assert_ensures_ctx)
1291 {
1292#ifdef DFCC_DEBUG
1294 (write_set->assume_requires_ctx == 0) &
1295 (write_set->assume_ensures_ctx == 0),
1296 "only one context flag at a time");
1297#endif
1299 void *ptr = *elem;
1300 // null pointers or already seen pointers are not fresh
1301#ifdef DFCC_DEBUG
1302 // manually inlined below
1303 if((ptr == 0) || (__CPROVER_contracts_obj_set_contains(seen, ptr)))
1304 return 0;
1305#else
1306 if(ptr == 0)
1307 return 0;
1308
1309 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
1310
1311 if(seen->elems[object_id] != 0)
1312 return 0;
1313#endif
1314 // record fresh object in the object set
1315#ifdef DFCC_DEBUG
1316 // manually inlined below
1318#else
1319 seen->nof_elems =
1320 (seen->elems[object_id] != 0) ? seen->nof_elems : seen->nof_elems + 1;
1321 seen->elems[object_id] = ptr;
1322 seen->is_empty = 0;
1323#endif
1324 // check size
1325 return __CPROVER_r_ok(ptr, size);
1326 }
1327 else
1328 {
1330 0, "__CPROVER_is_fresh is only called in requires or ensures clauses");
1332 return 0; // to silence libcheck
1333 }
1334}
1335
1337 void *lb,
1338 void **ptr,
1339 void *ub,
1341{
1342__CPROVER_HIDE:;
1344 (write_set != 0) & ((write_set->assume_requires_ctx == 1) |
1345 (write_set->assert_requires_ctx == 1) |
1346 (write_set->assume_ensures_ctx == 1) |
1347 (write_set->assert_ensures_ctx == 1)),
1348 "__CPROVER_pointer_in_range_dfcc is used only in requires or ensures "
1349 "clauses");
1350 __CPROVER_assert(__CPROVER_r_ok(lb, 0), "lb pointer must be valid");
1351 __CPROVER_assert(__CPROVER_r_ok(ub, 0), "ub pointer must be valid");
1353 __CPROVER_same_object(lb, ub),
1354 "lb and ub pointers must have the same object");
1355 __CPROVER_size_t lb_offset = __CPROVER_POINTER_OFFSET(lb);
1356 __CPROVER_size_t ub_offset = __CPROVER_POINTER_OFFSET(ub);
1358 lb_offset <= ub_offset, "lb and ub pointers must be ordered");
1359 if(write_set->assume_requires_ctx | write_set->assume_ensures_ctx)
1360 {
1362 return 0;
1363
1364 // add nondet offset
1365 __CPROVER_size_t offset = __VERIFIER_nondet_size();
1366
1367 // this cast is safe because we prove that ub and lb are ordered
1368 __CPROVER_size_t max_offset = ub_offset - lb_offset;
1369 __CPROVER_assume(offset <= max_offset);
1370 *ptr = (char *)lb + offset;
1371 return 1;
1372 }
1373 else /* write_set->assert_requires_ctx | write_set->assert_ensures_ctx */
1374 {
1375 __CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(*ptr);
1376 return __CPROVER_same_object(lb, *ptr) && lb_offset <= offset &&
1377 offset <= ub_offset;
1378 }
1379}
1380
1385 __CPROVER_size_t idx)
1386{
1387__CPROVER_HIDE:;
1388#ifdef DFCC_DEBUG
1389 __CPROVER_assert(write_set != 0, "write_set not NULL");
1390#endif
1391
1393 if(car.is_writable)
1394 return car.lb;
1395 else
1396 return (void *)0;
1397}
1398
1404 __CPROVER_size_t idx)
1405{
1406__CPROVER_HIDE:;
1407 __CPROVER_assert(idx < set->contract_assigns.max_elems, "no OOB access");
1409 if(car.is_writable)
1411}
1412
1417 __CPROVER_size_t idx)
1418{
1419__CPROVER_HIDE:;
1420#ifdef DFCC_DEBUG
1421 __CPROVER_assert(idx < set->contract_assigns.max_elems, "no OOB access");
1422#endif
1424 if(car.is_writable)
1425 __CPROVER_havoc_slice(car.lb, car.size);
1426}
1427
1439 void *ptr,
1441{
1442__CPROVER_HIDE:;
1444 (set != 0) &
1445 ((set->assume_requires_ctx == 1) | (set->assert_requires_ctx == 1) |
1446 (set->assume_ensures_ctx == 1) | (set->assert_ensures_ctx == 1)),
1447 "__CPROVER_is_freeable is used only in requires or ensures clauses");
1448
1449 // These are all the preconditions checked by `free` of the CPROVER library
1450 __CPROVER_bool is_dynamic_object = (ptr == 0) | __CPROVER_DYNAMIC_OBJECT(ptr);
1451 __CPROVER_bool has_offset_zero =
1452 (ptr == 0) | (__CPROVER_POINTER_OFFSET(ptr) == 0);
1453
1454 if((set->assume_requires_ctx == 1) || (set->assume_ensures_ctx == 1))
1455 return is_dynamic_object & has_offset_zero;
1456
1457 // these conditions cannot be used in assumptions since they involve
1458 // demonic non-determinism
1459 __CPROVER_bool is_null_or_valid_pointer = (ptr == 0) | __CPROVER_r_ok(ptr, 0);
1460 __CPROVER_bool is_not_deallocated =
1461 (ptr == 0) | (__CPROVER_deallocated != ptr);
1462 __CPROVER_bool is_not_alloca = (ptr == 0) | (__CPROVER_alloca_object != ptr);
1463 __CPROVER_bool is_not_array = (ptr == 0) | (__CPROVER_new_object != ptr) |
1465 return is_null_or_valid_pointer & is_dynamic_object & has_offset_zero &
1466 is_not_deallocated & is_not_alloca & is_not_array;
1467}
1468
1471 void *ptr,
1473{
1474__CPROVER_HIDE:;
1476 (set != 0) &
1477 ((set->assume_ensures_ctx == 1) | (set->assert_ensures_ctx == 1)),
1478 "__CPROVER_was_freed is used only in ensures clauses");
1480 (set->linked_deallocated != 0), "linked_deallocated is not null");
1481#ifdef DFCC_DEBUG
1482 // manually inlined below
1484 set->linked_deallocated, ptr);
1485#else
1486 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
1487 return set->linked_deallocated->elems[object_id] == ptr;
1488#endif
1489}
1490
1497 void *ptr,
1499{
1500__CPROVER_HIDE:;
1502 set && ((set->assume_ensures_ctx == 1) | (set->assert_ensures_ctx == 1)),
1503 "__CPROVER_was_freed is used only in ensures clauses");
1504
1505 if(set->assume_ensures_ctx)
1506 {
1507#ifdef DFCC_DEBUG
1508 // manually inlined below
1511 "assuming __CPROVER_was_freed(ptr) requires ptr to always exist in the "
1512 "contract's frees clause");
1513#else
1514 __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
1516 set->contract_frees.elems[object_id] == ptr,
1517 "assuming __CPROVER_was_freed(ptr) requires ptr to always exist in the "
1518 "contract's frees clause");
1519#endif
1520 }
1521}
1522
1532 void (**function_pointer)(void),
1533 void (*contract)(void),
1535{
1536__CPROVER_HIDE:;
1538 (set != 0) &
1539 ((set->assume_requires_ctx == 1) | (set->assert_requires_ctx == 1) |
1540 (set->assume_ensures_ctx == 1) | (set->assert_ensures_ctx == 1)),
1541 "__CPROVER_obeys_contract is used only in requires or ensures clauses");
1542 if((set->assume_requires_ctx == 1) | (set->assume_ensures_ctx == 1))
1543 {
1544 // decide if predicate must hold
1546 return 0;
1547
1548 // must hold, assign the function pointer to the contract function
1549 *function_pointer = contract;
1550 return 1;
1551 }
1552 else
1553 {
1554 // in assumption contexts, the pointer gets checked for equality
1555 return *function_pointer == contract;
1556 }
1557}
1558#endif // __CPROVER_contracts_library_defined
__CPROVER_thread_local __CPROVER_size_t __CPROVER_max_malloc_size
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_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.
void * ub
Upper bound address of the range.
unsigned char is_writable
True iff __CPROVER_w_ok(lb, size) holds at creation.
void ** elems
Array of void *pointers, indexed by their object ID or some other order.
unsigned char is_empty
True iff nof_elems is 0.
__CPROVER_size_t watermark
next usable index in elems if less than max_elems (1 + greatest used index in elems)
unsigned char indexed_by_object_id
True iff elems is indexed by the object id of the pointers.
__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.
unsigned char assume_ensures_ctx
True iff the write set checks ensures clauses in an assumption ctx.
__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)
unsigned char assume_requires_ctx
True iff the write set checks requires clauses in an assumption ctx.
__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.
unsigned char assert_ensures_ctx
True iff this write set checks ensures clauses in an assertion ctx.
unsigned char assert_requires_ctx
True iff the write set checks requires clauses in an assertion ctx.
unsigned char allow_deallocate
True iff dynamic deallocation is allowed (default: true)
__CPROVER_contracts_obj_set_t allocated
Set of objects allocated by the function under analysis (indexed mode)
unsigned char 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)