Skip to content

Commit e48f079

Browse files
author
Remi Delmas
committed
CONTRACTS: Add --dfcc-debug-lib CLI switch
1 parent 97c8624 commit e48f079

File tree

7 files changed

+62
-38
lines changed

7 files changed

+62
-38
lines changed

‎doc/man/cbmc.1‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -334,6 +334,9 @@ set malloc failure mode to return null
334334
\fB\-\-string\-abstraction\fR
335335
track C string lengths and zero\-termination
336336
.TP
337+
\fB\-\-dfcc\-debug\-lib\fR
338+
enable debug assertions in the cprover contracts library
339+
.TP
337340
\fB\-\-reachability\-slice\fR
338341
remove instructions that cannot appear on a trace
339342
from entry point to a property

‎doc/man/goto-analyzer.1‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -585,6 +585,9 @@ set malloc failure mode to return null
585585
.TP
586586
\fB\-\-string\-abstraction\fR
587587
track C string lengths and zero\-termination
588+
.TP
589+
\fB\-\-dfcc\-debug\-lib\fR
590+
enable debug assertions in the cprover contracts library
588591
.SS "Standard Checks"
589592
From version \fB6.0\fR onwards, \fBcbmc\fR, \fBgoto-analyzer\fR and some other tools
590593
apply some checks to the program by default (called the "standard checks"), with the

‎doc/man/goto-instrument.1‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -706,6 +706,9 @@ do not allow malloc calls to fail by default
706706
\fB\-\-string\-abstraction\fR
707707
track C string lengths and zero\-termination
708708
.TP
709+
\fB\-\-dfcc\-debug\-lib\fR
710+
enable debug assertions in the cprover contracts library
711+
.TP
709712
\fB\-\-model\-argc\-argv\fR \fIn\fR
710713
Create up to \fIn\fR non-deterministic C strings as entries to \fIargv\fR and
711714
set \fIargc\fR accordingly. In absence of such modelling, \fIargv\fR is left

‎src/ansi-c/cprover_library.cpp‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,9 @@ static std::string get_cprover_library_text(
4545
if(config.ansi_c.string_abstraction)
4646
library_text << "#define " CPROVER_PREFIX "STRING_ABSTRACTION\n";
4747

48+
if(config.ansi_c.dfcc_debug_lib)
49+
library_text << "#define " CPROVER_PREFIX "DFCC_DEBUG_LIB\n";
50+
4851
// cprover_library.inc may not have been generated when running Doxygen, thus
4952
// make Doxygen skip this part
5053
/// \cond

‎src/ansi-c/library/cprover_contracts.c‎

Lines changed: 36 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -136,7 +136,7 @@ void __CPROVER_contracts_car_set_create(
136136
__CPROVER_size_t max_elems)
137137
{
138138
__CPROVER_HIDE:;
139-
#ifdef DFCC_DEBUG
139+
#ifdef __CPROVER_DFCC_DEBUG_LIB
140140
__CPROVER_assert(
141141
__CPROVER_rw_ok(set, sizeof(__CPROVER_contracts_car_set_t)),
142142
"set writable");
@@ -159,7 +159,7 @@ void __CPROVER_contracts_car_set_insert(
159159
__CPROVER_size_t size)
160160
{
161161
__CPROVER_HIDE:;
162-
#ifdef DFCC_DEBUG
162+
#ifdef __CPROVER_DFCC_DEBUG_LIB
163163
__CPROVER_assert((set != 0) & (idx < set->max_elems), "no OOB access");
164164
#endif
165165
__CPROVER_assert(
@@ -239,7 +239,7 @@ void __CPROVER_contracts_obj_set_create_indexed_by_object_id(
239239
__CPROVER_contracts_obj_set_ptr_t set)
240240
{
241241
__CPROVER_HIDE:;
242-
#ifdef DFCC_DEBUG
242+
#ifdef __CPROVER_DFCC_DEBUG_LIB
243243
__CPROVER_assert(
244244
__CPROVER_rw_ok(set, sizeof(__CPROVER_contracts_obj_set_t)),
245245
"set writable");
@@ -274,7 +274,7 @@ void __CPROVER_contracts_obj_set_create_append(
274274
__CPROVER_size_t max_elems)
275275
{
276276
__CPROVER_HIDE:;
277-
#ifdef DFCC_DEBUG
277+
#ifdef __CPROVER_DFCC_DEBUG_LIB
278278
__CPROVER_assert(
279279
__CPROVER_rw_ok(set, sizeof(__CPROVER_contracts_obj_set_t)),
280280
"set writable");
@@ -292,7 +292,7 @@ __CPROVER_HIDE:;
292292
void __CPROVER_contracts_obj_set_release(__CPROVER_contracts_obj_set_ptr_t set)
293293
{
294294
__CPROVER_HIDE:;
295-
#ifdef DFCC_DEBUG
295+
#ifdef __CPROVER_DFCC_DEBUG_LIB
296296
__CPROVER_assert(
297297
__CPROVER_rw_ok(set, sizeof(__CPROVER_contracts_obj_set_t)),
298298
"set readable");
@@ -311,7 +311,7 @@ void __CPROVER_contracts_obj_set_add(
311311
{
312312
__CPROVER_HIDE:;
313313
__CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
314-
#ifdef DFCC_DEBUG
314+
#ifdef __CPROVER_DFCC_DEBUG_LIB
315315
__CPROVER_assert(set->indexed_by_object_id, "indexed by object id");
316316
__CPROVER_assert(object_id < set->max_elems, "no OOB access");
317317
#endif
@@ -329,7 +329,7 @@ void __CPROVER_contracts_obj_set_append(
329329
void *ptr)
330330
{
331331
__CPROVER_HIDE:;
332-
#ifdef DFCC_DEBUG
332+
#ifdef __CPROVER_DFCC_DEBUG_LIB
333333
__CPROVER_assert(!(set->indexed_by_object_id), "not indexed by object id");
334334
__CPROVER_assert(set->watermark < set->max_elems, "no OOB access");
335335
#endif
@@ -349,7 +349,7 @@ void __CPROVER_contracts_obj_set_remove(
349349
{
350350
__CPROVER_HIDE:;
351351
__CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
352-
#ifdef DFCC_DEBUG
352+
#ifdef __CPROVER_DFCC_DEBUG_LIB
353353
__CPROVER_assert(set->indexed_by_object_id, "indexed by object id");
354354
__CPROVER_assert(object_id < set->max_elems, "no OOB access");
355355
#endif
@@ -369,7 +369,7 @@ __CPROVER_bool __CPROVER_contracts_obj_set_contains(
369369
{
370370
__CPROVER_HIDE:;
371371
__CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
372-
#ifdef DFCC_DEBUG
372+
#ifdef __CPROVER_DFCC_DEBUG_LIB
373373
__CPROVER_assert(set->indexed_by_object_id, "indexed by object id");
374374
__CPROVER_assert(object_id < set->max_elems, "no OOB access");
375375
#endif
@@ -386,7 +386,7 @@ __CPROVER_bool __CPROVER_contracts_obj_set_contains_exact(
386386
{
387387
__CPROVER_HIDE:;
388388
__CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
389-
#ifdef DFCC_DEBUG
389+
#ifdef __CPROVER_DFCC_DEBUG_LIB
390390
__CPROVER_assert(set->indexed_by_object_id, "indexed by object id");
391391
__CPROVER_assert(object_id < set->max_elems, "no OOB access");
392392
#endif
@@ -421,7 +421,7 @@ void __CPROVER_contracts_write_set_create(
421421
__CPROVER_bool allow_deallocate)
422422
{
423423
__CPROVER_HIDE:;
424-
#ifdef DFCC_DEBUG
424+
#ifdef __CPROVER_DFCC_DEBUG_LIB
425425
__CPROVER_assert(
426426
__CPROVER_w_ok(set, sizeof(__CPROVER_contracts_write_set_t)),
427427
"set writable");
@@ -450,7 +450,7 @@ void __CPROVER_contracts_write_set_release(
450450
__CPROVER_contracts_write_set_ptr_t set)
451451
{
452452
__CPROVER_HIDE:;
453-
#ifdef DFCC_DEBUG
453+
#ifdef __CPROVER_DFCC_DEBUG_LIB
454454
__CPROVER_assert(
455455
__CPROVER_rw_ok(set, sizeof(__CPROVER_contracts_write_set_t)),
456456
"set readable");
@@ -574,7 +574,7 @@ __CPROVER_HIDE:;
574574

575575
// store pointer
576576
__CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
577-
#ifdef DFCC_DEBUG
577+
#ifdef __CPROVER_DFCC_DEBUG_LIB
578578
// manually inlined below
579579
__CPROVER_contracts_obj_set_add(&(set->contract_frees), ptr);
580580
__CPROVER_assert(object_id < set->contract_frees.max_elems, "no OOB access");
@@ -587,7 +587,7 @@ __CPROVER_HIDE:;
587587
#endif
588588

589589
// append pointer if available
590-
#ifdef DFCC_DEBUG
590+
#ifdef __CPROVER_DFCC_DEBUG_LIB
591591
__CPROVER_contracts_obj_set_append(&(set->contract_frees_append), ptr);
592592
#else
593593
set->contract_frees_append.nof_elems = set->contract_frees_append.watermark;
@@ -606,7 +606,7 @@ void __CPROVER_contracts_write_set_add_allocated(
606606
{
607607
__CPROVER_HIDE:;
608608
__CPROVER_assert(set->allow_allocate, "dynamic allocation is allowed");
609-
#if DFCC_DEBUG
609+
#if __CPROVER_DFCC_DEBUG_LIB
610610
// call inlined below
611611
__CPROVER_contracts_obj_set_add(&(set->allocated), ptr);
612612
#else
@@ -627,7 +627,7 @@ void __CPROVER_contracts_write_set_add_decl(
627627
void *ptr)
628628
{
629629
__CPROVER_HIDE:;
630-
#if DFCC_DEBUG
630+
#if __CPROVER_DFCC_DEBUG_LIB
631631
// call inlined below
632632
__CPROVER_contracts_obj_set_add(&(set->allocated), ptr);
633633
#else
@@ -652,7 +652,7 @@ void __CPROVER_contracts_write_set_record_dead(
652652
void *ptr)
653653
{
654654
__CPROVER_HIDE:;
655-
#ifdef DFCC_DEBUG
655+
#ifdef __CPROVER_DFCC_DEBUG_LIB
656656
// manually inlined below
657657
__CPROVER_contracts_obj_set_remove(&(set->allocated), ptr);
658658
#else
@@ -677,7 +677,7 @@ void __CPROVER_contracts_write_set_record_deallocated(
677677
void *ptr)
678678
{
679679
__CPROVER_HIDE:;
680-
#if DFCC_DEBUG
680+
#if __CPROVER_DFCC_DEBUG_LIB
681681
// we record the deallocation to be able to evaluate was_freed post conditions
682682
__CPROVER_contracts_obj_set_add(&(set->deallocated), ptr);
683683
__CPROVER_contracts_obj_set_remove(&(set->allocated), ptr);
@@ -745,7 +745,7 @@ __CPROVER_bool __CPROVER_contracts_write_set_check_assignment(
745745
__CPROVER_contracts_write_set_ptr_t set,
746746
void *ptr,
747747
__CPROVER_size_t size)
748-
#if DFCC_DEBUG
748+
#if __CPROVER_DFCC_DEBUG_LIB
749749
// manually inlined below
750750
{
751751
__CPROVER_HIDE:;
@@ -926,7 +926,7 @@ __CPROVER_bool __CPROVER_contracts_write_set_check_deallocate(
926926
__CPROVER_HIDE:;
927927
__CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
928928

929-
#ifdef DFCC_DEBUG
929+
#ifdef __CPROVER_DFCC_DEBUG_LIB
930930
__CPROVER_assert(
931931
set->contract_frees.indexed_by_object_id,
932932
"set->contract_frees is indexed by object id");
@@ -984,7 +984,7 @@ __CPROVER_bool __CPROVER_contracts_write_set_check_frees_clause_inclusion(
984984
__CPROVER_contracts_write_set_ptr_t candidate)
985985
{
986986
__CPROVER_HIDE:;
987-
#ifdef DFCC_DEBUG
987+
#ifdef __CPROVER_DFCC_DEBUG_LIB
988988
__CPROVER_assert(
989989
reference->contract_frees.indexed_by_object_id,
990990
"reference->contract_frees is indexed by object id");
@@ -1067,7 +1067,7 @@ void __CPROVER_contracts_link_is_fresh(
10671067
__CPROVER_contracts_obj_set_ptr_t is_fresh_set)
10681068
{
10691069
__CPROVER_HIDE:;
1070-
#ifdef DFCC_DEBUG
1070+
#ifdef __CPROVER_DFCC_DEBUG_LIB
10711071
__CPROVER_assert(write_set != 0, "write_set not NULL");
10721072
#endif
10731073
if((is_fresh_set != 0))
@@ -1089,7 +1089,7 @@ void __CPROVER_contracts_link_allocated(
10891089
__CPROVER_contracts_write_set_ptr_t write_set_to_link)
10901090
{
10911091
__CPROVER_HIDE:;
1092-
#ifdef DFCC_DEBUG
1092+
#ifdef __CPROVER_DFCC_DEBUG_LIB
10931093
__CPROVER_assert(
10941094
write_set_postconditions != 0, "write_set_postconditions not NULL");
10951095
#endif
@@ -1114,7 +1114,7 @@ void __CPROVER_contracts_link_deallocated(
11141114
__CPROVER_contracts_write_set_ptr_t write_set_to_link)
11151115
{
11161116
__CPROVER_HIDE:;
1117-
#ifdef DFCC_DEBUG
1117+
#ifdef __CPROVER_DFCC_DEBUG_LIB
11181118
__CPROVER_assert(
11191119
write_set_postconditions != 0, "write_set_postconditions not NULL");
11201120
#endif
@@ -1168,7 +1168,7 @@ __CPROVER_HIDE:;
11681168
(write_set->assume_ensures_ctx == 1) |
11691169
(write_set->assert_ensures_ctx == 1)),
11701170
"__CPROVER_is_fresh is used only in requires or ensures clauses");
1171-
#ifdef DFCC_DEBUG
1171+
#ifdef __CPROVER_DFCC_DEBUG_LIB
11721172
__CPROVER_assert(
11731173
__CPROVER_rw_ok(write_set, sizeof(__CPROVER_contracts_write_set_t)),
11741174
"set readable");
@@ -1177,7 +1177,7 @@ __CPROVER_HIDE:;
11771177
#endif
11781178
if(write_set->assume_requires_ctx)
11791179
{
1180-
#ifdef DFCC_DEBUG
1180+
#ifdef __CPROVER_DFCC_DEBUG_LIB
11811181
__CPROVER_assert(
11821182
(write_set->assert_requires_ctx == 0) &
11831183
(write_set->assume_ensures_ctx == 0) &
@@ -1219,7 +1219,7 @@ __CPROVER_HIDE:;
12191219
// __CPROVER_memory_leak = record_may_leak ? ptr : __CPROVER_memory_leak;
12201220

12211221
// record fresh object in the object set
1222-
#ifdef DFCC_DEBUG
1222+
#ifdef __CPROVER_DFCC_DEBUG_LIB
12231223
// manually inlined below
12241224
__CPROVER_contracts_obj_set_add(write_set->linked_is_fresh, ptr);
12251225
#else
@@ -1235,7 +1235,7 @@ __CPROVER_HIDE:;
12351235
}
12361236
else if(write_set->assume_ensures_ctx)
12371237
{
1238-
#ifdef DFCC_DEBUG
1238+
#ifdef __CPROVER_DFCC_DEBUG_LIB
12391239
__CPROVER_assert(
12401240
(write_set->assume_requires_ctx == 0) &
12411241
(write_set->assert_requires_ctx == 0) &
@@ -1274,7 +1274,7 @@ __CPROVER_HIDE:;
12741274
__CPROVER_memory_leak = record_may_leak ? ptr : __CPROVER_memory_leak;
12751275

12761276
// record fresh object in the caller's write set
1277-
#ifdef DFCC_DEBUG
1277+
#ifdef __CPROVER_DFCC_DEBUG_LIB
12781278
__CPROVER_contracts_obj_set_add(write_set->linked_allocated, ptr);
12791279
#else
12801280
__CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
@@ -1289,7 +1289,7 @@ __CPROVER_HIDE:;
12891289
}
12901290
else if(write_set->assert_requires_ctx | write_set->assert_ensures_ctx)
12911291
{
1292-
#ifdef DFCC_DEBUG
1292+
#ifdef __CPROVER_DFCC_DEBUG_LIB
12931293
__CPROVER_assert(
12941294
(write_set->assume_requires_ctx == 0) &
12951295
(write_set->assume_ensures_ctx == 0),
@@ -1298,7 +1298,7 @@ __CPROVER_HIDE:;
12981298
__CPROVER_contracts_obj_set_ptr_t seen = write_set->linked_is_fresh;
12991299
void *ptr = *elem;
13001300
// null pointers or already seen pointers are not fresh
1301-
#ifdef DFCC_DEBUG
1301+
#ifdef __CPROVER_DFCC_DEBUG_LIB
13021302
// manually inlined below
13031303
if((ptr == 0) || (__CPROVER_contracts_obj_set_contains(seen, ptr)))
13041304
return 0;
@@ -1312,7 +1312,7 @@ __CPROVER_HIDE:;
13121312
return 0;
13131313
#endif
13141314
// record fresh object in the object set
1315-
#ifdef DFCC_DEBUG
1315+
#ifdef __CPROVER_DFCC_DEBUG_LIB
13161316
// manually inlined below
13171317
__CPROVER_contracts_obj_set_add(seen, ptr);
13181318
#else
@@ -1385,7 +1385,7 @@ void *__CPROVER_contracts_write_set_havoc_get_assignable_target(
13851385
__CPROVER_size_t idx)
13861386
{
13871387
__CPROVER_HIDE:;
1388-
#ifdef DFCC_DEBUG
1388+
#ifdef __CPROVER_DFCC_DEBUG_LIB
13891389
__CPROVER_assert(write_set != 0, "write_set not NULL");
13901390
#endif
13911391

@@ -1417,7 +1417,7 @@ void __CPROVER_contracts_write_set_havoc_slice(
14171417
__CPROVER_size_t idx)
14181418
{
14191419
__CPROVER_HIDE:;
1420-
#ifdef DFCC_DEBUG
1420+
#ifdef __CPROVER_DFCC_DEBUG_LIB
14211421
__CPROVER_assert(idx < set->contract_assigns.max_elems, "no OOB access");
14221422
#endif
14231423
__CPROVER_contracts_car_t car = set->contract_assigns.elems[idx];
@@ -1478,7 +1478,7 @@ __CPROVER_HIDE:;
14781478
"__CPROVER_was_freed is used only in ensures clauses");
14791479
__CPROVER_assert(
14801480
(set->linked_deallocated != 0), "linked_deallocated is not null");
1481-
#ifdef DFCC_DEBUG
1481+
#ifdef __CPROVER_DFCC_DEBUG_LIB
14821482
// manually inlined below
14831483
return __CPROVER_contracts_obj_set_contains_exact(
14841484
set->linked_deallocated, ptr);
@@ -1504,7 +1504,7 @@ __CPROVER_HIDE:;
15041504

15051505
if(set->assume_ensures_ctx)
15061506
{
1507-
#ifdef DFCC_DEBUG
1507+
#ifdef __CPROVER_DFCC_DEBUG_LIB
15081508
// manually inlined below
15091509
__CPROVER_assert(
15101510
__CPROVER_contracts_obj_set_contains_exact(&(set->contract_frees), ptr),

‎src/util/config.cpp‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1164,6 +1164,11 @@ bool configt::set(const cmdlinet &cmdline)
11641164
else
11651165
ansi_c.string_abstraction=false;
11661166

1167+
if(cmdline.isset("dfcc-debug-lib"))
1168+
ansi_c.dfcc_debug_lib = true;
1169+
else
1170+
ansi_c.dfcc_debug_lib = false;
1171+
11671172
if(cmdline.isset("no-library"))
11681173
ansi_c.lib=configt::ansi_ct::libt::LIB_NONE;
11691174

0 commit comments

Comments
 (0)