We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 4c9e03a commit 0262ae1Copy full SHA for 0262ae1
src/ansi-c/library/cprover_contracts.c
@@ -1308,7 +1308,6 @@ __CPROVER_HIDE:;
1308
// __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
1309
// __CPROVER_memory_leak = record_may_leak ? ptr : __CPROVER_memory_leak;
1310
1311
- // record fresh object in the object set
1312
#ifdef __CPROVER_DFCC_DEBUG_LIB
1313
// manually inlined below
1314
__CPROVER_contracts_obj_set_add(write_set->linked_is_fresh, ptr);
src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp
@@ -17,6 +17,7 @@ Date: Jan 2025
17
#include <util/std_code.h>
18
#include <util/std_expr.h>
19
#include <util/symbol.h>
20
+
21
#include "dfcc_cfg_info.h"
22
#include "dfcc_library.h"
23
0 commit comments