diff --git a/doc/cprover-manual/contracts-requires-and-ensures.md b/doc/cprover-manual/contracts-requires-and-ensures.md deleted file mode 100644 index 1fc15dd9f5c..00000000000 --- a/doc/cprover-manual/contracts-requires-and-ensures.md +++ /dev/null @@ -1,136 +0,0 @@ -[CPROVER Manual TOC](../../) - -# Requires \& Ensures Clauses - - -### Syntax - -```c -__CPROVER_requires(bool cond) -``` - -A _requires_ clause specifies a precondition for a function, i.e., a property that must hold to properly execute the operation. Developers may see the _requires_ clauses of a function as obligations on the caller when invoking the function. The precondition of a function is the conjunction of the _requires_ clauses, or `true` if none are specified. - -```c -__CPROVER_ensures(bool cond) -``` - -An _ensures_ clause specifies a postcondition for a function, i.e., a property over arguments or global variables that the function guarantees at the end of the operation. Developers may see the _ensures_ clauses of a function as the obligations of that function to the caller. The postcondition of a function is the conjunction of the _ensures_ clauses, or `true` if none are specified. - - -### Parameters - -A _requires_ clause takes a Boolean expression over the arguments of -a function and/or global variables, including CBMC primitive functions (e.g., -[Memory Predicates](../../contracts/memory-predicates/)). Similarly, _ensures_ clauses also accept Boolean -expressions and CBMC primitives, but also [History Variables](../../contracts/history-variables/) and `__CPROVER_return_value`. - -**Important.** Developers may call functions inside _requires_ and _ensures_ -clauses to better write larger specifications (e.g., predicates). However, at -this point CBMC does not enforce such functions to be without side effects -(i.e., do not modify any global state). This will be checked in future -versions. - - -### Semantics - -The semantics of _ensures_ and _requires_ clauses can be understood in two -contexts: enforcement and replacement. To illustrate these two perspectives, -consider the following implementation of the `sum` function. - -```c -int sum(const uint32_t a, const uint32_t b, uint32_t* out) -/* Precondition */ -__CPROVER_requires(__CPROVER_is_fresh(out, sizeof(*out))) -/* Postconditions */ -__CPROVER_ensures(__CPROVER_return_value == SUCCESS || __CPROVER_return_value == FAILURE) -__CPROVER_ensures((__CPROVER_return_value == SUCCESS) ==> (*out == (a + b))) -{ - const uint64_t result = ((uint64_t) a) + ((uint64_t) b); - if (result > UINT32_MAX) return FAILURE; - *out = (uint32_t) result; - return SUCCESS; -} -``` - -#### Enforcement - -In order to determine whether _requires_ and _ensures_ clauses are a sound -abstraction of the behavior of a function *f*, CBMC will try to check them -as follows: - -1. Considers all arguments and global variables as non-deterministic values; -2. Assumes all preconditions specified in the `__CPROVER_requires` clauses; -4. Calls the implementation of function *f*; -5. Asserts all postconditions described in the `__CPROVER_ensures` clauses. - -In our example, the `sum` function will be instrumented as follows: - -```c -/* Function Contract Enforcement */ -int sum(uint32_t a, uint32_t b, uint32_t* out) -{ - __CPROVER_assume(__CPROVER_is_fresh(out, sizeof(*out))); - - int return_value_sum = __CPROVER_contracts_original_sum(a, b, out); - - __CPROVER_assert(return_value_sum == SUCCESS || return_value_sum == FAILURE, "Check ensures clause"); - __CPROVER_assert((return_value_sum == SUCCESS) ==> (*out == (a + b)), "Check ensures clause"); - - return return_value_sum; -} -``` - -#### Replacement - -Assuming _requires_ and _ensures_ clauses are a sound abstraction of the -behavior of the function *f*, CBMC will use the function contract in place of -the function implementation as follows: - -1. Adds assertions for all preconditions specified in the `__CPROVER_requires` - clauses; -2. Adds non-deterministic assignments for each symbol listed in the - `__CPROVER_assigns` clause (see [Assigns Clause](../../contracts/assigns/) -for details); -3. Assumes all postconditions described in the `__CPROVER_ensures` clauses; - -In our example, consider that a function `foo` may call `sum`. - -```c -int foo() -{ - uint32_t a; - uint32_t b; - uint32_t out; - int rval = sum(a, b, &out); - if (rval == SUCCESS) - return out; - return rval; -} -``` - -CBMC will use the function contract in place of the function implementation -wherever the function is called. - -```c -int foo() -{ - uint32_t a; - uint32_t b; - uint32_t out; - - /* Function Contract Replacement */ - /* Precondition */ - __CPROVER_assert(__CPROVER_is_fresh(out, sizeof(*out)), "Check requires clause"); - - /* Postconditions */ - int return_value_sum = nondet_int(); - __CPROVER_assume(return_value_sum == SUCCESS || return_value_sum == FAILURE); - __CPROVER_assume((return_value_sum == SUCCESS) ==> (*out == (*a + *b))); - - int rval = return_value_sum; - if (rval == SUCCESS) - return out; - return rval; -} -``` diff --git a/regression/contracts/assigns-enforce-malloc-zero/main.c b/regression/contracts/assigns-enforce-malloc-zero/main.c index 9592997ddd5..eeb6a4d06ae 100644 --- a/regression/contracts/assigns-enforce-malloc-zero/main.c +++ b/regression/contracts/assigns-enforce-malloc-zero/main.c @@ -6,7 +6,7 @@ int foo(char *a, int size) // clang-format off __CPROVER_requires(0 <= size && size <= __CPROVER_max_malloc_size) __CPROVER_requires(a == NULL || __CPROVER_is_fresh(a, size)) - __CPROVER_assigns(a: __CPROVER_POINTER_OBJECT(a)) + __CPROVER_assigns(a: __CPROVER_whole_object(a)) __CPROVER_ensures( a && __CPROVER_return_value >= 0 ==> a[__CPROVER_return_value] == 0) // clang-format on diff --git a/regression/contracts/assigns-enforce-malloc-zero/test.desc b/regression/contracts/assigns-enforce-malloc-zero/test.desc index eefba72ce5b..7d82f4cf938 100644 --- a/regression/contracts/assigns-enforce-malloc-zero/test.desc +++ b/regression/contracts/assigns-enforce-malloc-zero/test.desc @@ -1,7 +1,6 @@ CORE main.c ---enforce-contract foo _ --malloc-may-fail --malloc-fail-null -^\[foo.assigns.\d+\] line 9 Check that POINTER_OBJECT\(\(const void \*\)a\) is valid when a != \(\(char \*\)NULL\): SUCCESS$ +--dfcc main --enforce-contract foo _ --malloc-may-fail --malloc-fail-null ^\[foo.assigns.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns-local-composite/test.desc b/regression/contracts/assigns-local-composite/test.desc index 1e4b211e77d..261546f1591 100644 --- a/regression/contracts/assigns-local-composite/test.desc +++ b/regression/contracts/assigns-local-composite/test.desc @@ -1,12 +1,12 @@ CORE main.c ---enforce-contract foo +--dfcc main --enforce-contract foo ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -- -Checks that assigns clause checking explicitly checks assignments to locally +Checks that assigns clause checking explicitly checks assignments to locally declared symbols with composite types, when they are dirty. -Out of bounds accesses to locally declared arrays, structs, etc. +Out of bounds accesses to locally declared arrays, structs, etc. will be detected by assigns clause checking. diff --git a/regression/contracts/assigns-replace-ignored-return-value/test.desc b/regression/contracts/assigns-replace-ignored-return-value/test.desc index c362aba98fd..92d57115adf 100644 --- a/regression/contracts/assigns-replace-ignored-return-value/test.desc +++ b/regression/contracts/assigns-replace-ignored-return-value/test.desc @@ -1,6 +1,6 @@ CORE main.c ---replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo +--dfcc main --replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts/assigns-replace-malloc-zero/main.c b/regression/contracts/assigns-replace-malloc-zero/main.c index 14c34366a18..1877cf0fa48 100644 --- a/regression/contracts/assigns-replace-malloc-zero/main.c +++ b/regression/contracts/assigns-replace-malloc-zero/main.c @@ -6,7 +6,7 @@ int foo(char *a, int size) // clang-format off __CPROVER_requires(0 <= size && size <= __CPROVER_max_malloc_size) __CPROVER_requires(a == NULL || __CPROVER_rw_ok(a, size)) -__CPROVER_assigns(__CPROVER_POINTER_OBJECT(a)) +__CPROVER_assigns(__CPROVER_whole_object(a)) __CPROVER_ensures( a && __CPROVER_return_value >= 0 ==> a[__CPROVER_return_value] == 0) // clang-format on diff --git a/regression/contracts/assigns-replace-malloc-zero/test.desc b/regression/contracts/assigns-replace-malloc-zero/test.desc index 6b265418f9b..2e410cec503 100644 --- a/regression/contracts/assigns-replace-malloc-zero/test.desc +++ b/regression/contracts/assigns-replace-malloc-zero/test.desc @@ -1,6 +1,6 @@ CORE main.c ---replace-call-with-contract foo _ --malloc-may-fail --malloc-fail-null +--dfcc main --replace-call-with-contract foo _ --malloc-may-fail --malloc-fail-null ^EXIT=0$ ^SIGNAL=0$ \[main\.assertion\.1\] line 35 expecting SUCCESS: SUCCESS$ diff --git a/regression/contracts/assigns-slice-targets/main-enforce.c b/regression/contracts/assigns-slice-targets/main-enforce.c index 7f39d6f06cd..aa1c5a4070d 100644 --- a/regression/contracts/assigns-slice-targets/main-enforce.c +++ b/regression/contracts/assigns-slice-targets/main-enforce.c @@ -7,11 +7,14 @@ struct st int c; }; -void foo(struct st *s) +void foo(struct st *s, struct st *ss) // clang-format off __CPROVER_requires(__CPROVER_is_fresh(s, sizeof(*s))) - __CPROVER_assigns(__CPROVER_object_slice(s->arr1, 5)) - __CPROVER_assigns(__CPROVER_object_from(s->arr2 + 5)) + __CPROVER_assigns( + __CPROVER_object_upto(s->arr1, 5); + __CPROVER_object_from(s->arr2 + 5); + __CPROVER_whole_object(ss); +) // clang-format on { // PASS @@ -41,13 +44,24 @@ void foo(struct st *s) s->arr2[7] = 0; s->arr2[8] = 0; s->arr2[9] = 0; + + // PASS + ss->a = 0; + ss->arr1[0] = 0; + ss->arr1[7] = 0; + ss->arr1[9] = 0; + ss->b = 0; + ss->arr2[6] = 0; + ss->arr2[8] = 0; + ss->c = 0; } int main() { struct st s; + struct st ss; - foo(&s); + foo(&s, &ss); return 0; } diff --git a/regression/contracts/assigns-slice-targets/main-replace.c b/regression/contracts/assigns-slice-targets/main-replace.c index 5f21100ee7c..975d43b8606 100644 --- a/regression/contracts/assigns-slice-targets/main-replace.c +++ b/regression/contracts/assigns-slice-targets/main-replace.c @@ -7,11 +7,14 @@ struct st int c; }; -void foo(struct st *s) +void foo(struct st *s, struct st *ss) // clang-format off __CPROVER_requires(__CPROVER_is_fresh(s, sizeof(*s))) - __CPROVER_assigns(__CPROVER_object_slice(s->arr1, 5)) - __CPROVER_assigns(__CPROVER_object_from(s->arr2 + 5)) + __CPROVER_assigns( + __CPROVER_object_upto(s->arr1, 5); + __CPROVER_object_from(s->arr2 + 5); + __CPROVER_whole_object(ss); + ) // clang-format on { s->arr1[0] = 0; @@ -54,7 +57,32 @@ int main() s.arr2[9] = 0; s.c = 0; - foo(&s); + struct st ss; + ss.a = 0; + ss.arr1[0] = 0; + ss.arr1[1] = 0; + ss.arr1[2] = 0; + ss.arr1[3] = 0; + ss.arr1[4] = 0; + ss.arr1[5] = 0; + ss.arr1[6] = 0; + ss.arr1[7] = 0; + ss.arr1[8] = 0; + ss.arr1[9] = 0; + + ss.arr2[0] = 0; + ss.arr2[1] = 0; + ss.arr2[2] = 0; + ss.arr2[3] = 0; + ss.arr2[4] = 0; + ss.arr2[5] = 0; + ss.arr2[6] = 0; + ss.arr2[7] = 0; + ss.arr2[8] = 0; + ss.arr2[9] = 0; + ss.c = 0; + + foo(&s, &ss); // PASS assert(s.a == 0); @@ -92,5 +120,31 @@ int main() // PASS assert(s.c == 0); + + // FAIL + assert(ss.a == 0); + assert(ss.arr1[0] == 0); + assert(ss.arr1[1] == 0); + assert(ss.arr1[2] == 0); + assert(ss.arr1[3] == 0); + assert(ss.arr1[4] == 0); + assert(ss.arr1[5] == 0); + assert(ss.arr1[6] == 0); + assert(ss.arr1[7] == 0); + assert(ss.arr1[8] == 0); + assert(ss.arr1[9] == 0); + assert(ss.b == 0); + assert(ss.arr2[0] == 0); + assert(ss.arr2[1] == 0); + assert(ss.arr2[2] == 0); + assert(ss.arr2[3] == 0); + assert(ss.arr2[4] == 0); + assert(ss.arr2[5] == 0); + assert(ss.arr2[6] == 0); + assert(ss.arr2[7] == 0); + assert(ss.arr2[8] == 0); + assert(ss.arr2[9] == 0); + assert(ss.c == 0); + return 0; } diff --git a/regression/contracts/assigns-slice-targets/test-enforce.desc b/regression/contracts/assigns-slice-targets/test-enforce.desc index 5b8f4fe5f58..e1df873e83e 100644 --- a/regression/contracts/assigns-slice-targets/test-enforce.desc +++ b/regression/contracts/assigns-slice-targets/test-enforce.desc @@ -1,8 +1,6 @@ CORE main-enforce.c ---enforce-contract foo -^\[foo.assigns.\d+\].* Check that __CPROVER_object_slice\(\(void \*\)s->arr1, \(.*\)5\) is valid: SUCCESS$ -^\[foo.assigns.\d+\].* Check that __CPROVER_object_from\(\(void \*\)\(s->arr2 \+ \(.*\)5\)\) is valid: SUCCESS$ +--dfcc main --enforce-contract foo ^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)0\] is assignable: SUCCESS$ ^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)1\] is assignable: SUCCESS$ ^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)2\] is assignable: SUCCESS$ @@ -23,6 +21,14 @@ main-enforce.c ^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)7\] is assignable: SUCCESS$ ^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)8\] is assignable: SUCCESS$ ^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)9\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that ss->a is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)0\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)7\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)9\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that ss->b is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that ss->arr2\[\(.*\)6\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that ss->arr2\[\(.*\)8\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that ss->c is assignable: SUCCESS$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns-slice-targets/test-replace.desc b/regression/contracts/assigns-slice-targets/test-replace.desc index 1f23fb0ae7e..b1eeafd252c 100644 --- a/regression/contracts/assigns-slice-targets/test-replace.desc +++ b/regression/contracts/assigns-slice-targets/test-replace.desc @@ -1,6 +1,6 @@ CORE main-replace.c ---replace-call-with-contract foo +--dfcc main --replace-call-with-contract foo ^\[main.assertion.\d+\].*assertion s.a == 0: SUCCESS$ ^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)0\] == 0: FAILURE$ ^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)1\] == 0: FAILURE$ @@ -24,6 +24,29 @@ main-replace.c ^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)8\] == 0: FAILURE$ ^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)9\] == 0: FAILURE$ ^\[main.assertion.\d+\].*assertion s.c == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion ss.a == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)0\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)1\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)2\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)3\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)4\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)5\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)6\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)7\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)8\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)9\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion ss.b == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)0\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)1\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)2\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)3\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)4\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)5\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)6\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)7\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)8\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)9\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion ss.c == 0: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_01/test.desc b/regression/contracts/assigns_enforce_01/test.desc index d3774ec5dfa..1dd64604f87 100644 --- a/regression/contracts/assigns_enforce_01/test.desc +++ b/regression/contracts/assigns_enforce_01/test.desc @@ -1,6 +1,6 @@ CORE main.c ---enforce-contract foo +--dfcc main --enforce-contract foo ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts/assigns_enforce_02/test.desc b/regression/contracts/assigns_enforce_02/test.desc index 2abca0b8bd1..9b05008a350 100644 --- a/regression/contracts/assigns_enforce_02/test.desc +++ b/regression/contracts/assigns_enforce_02/test.desc @@ -1,7 +1,6 @@ CORE main.c ---enforce-contract foo -^\[foo.assigns.\d+\] line 3 Check that z is valid: SUCCESS$ +--dfcc main --enforce-contract foo ^\[foo.assigns.\d+\] line 6 Check that \*x is assignable: FAILURE$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_03/test.desc b/regression/contracts/assigns_enforce_03/test.desc index 4b342024cc9..39067aa46f6 100644 --- a/regression/contracts/assigns_enforce_03/test.desc +++ b/regression/contracts/assigns_enforce_03/test.desc @@ -1,15 +1,6 @@ CORE main.c ---enforce-contract f1 --enforce-contract f2 --enforce-contract f3 -^\[f1.assigns.\d+\] line 1 Check that \*x1 is valid: SUCCESS$ -^\[f1.assigns.\d+\] line 1 Check that \*y1 is valid: SUCCESS$ -^\[f1.assigns.\d+\] line 1 Check that \*z1 is valid: SUCCESS$ -^\[f2.assigns.\d+\] line 6 Check that \*x2 is valid: SUCCESS$ -^\[f2.assigns.\d+\] line 6 Check that \*y2 is valid: SUCCESS$ -^\[f2.assigns.\d+\] line 6 Check that \*z2 is valid: SUCCESS$ -^\[f3.assigns.\d+\] line 11 Check that \*x3 is valid: SUCCESS$ -^\[f3.assigns.\d+\] line 11 Check that \*y3 is valid: SUCCESS$ -^\[f3.assigns.\d+\] line 12 Check that \*z3 is valid: SUCCESS$ +--dfcc main --enforce-contract f1 ^\[f3.assigns.\d+\] line 14 Check that \*x3 is assignable: SUCCESS$ ^\[f3.assigns.\d+\] line 15 Check that \*y3 is assignable: SUCCESS$ ^\[f3.assigns.\d+\] line 16 Check that \*z3 is assignable: SUCCESS$ @@ -18,4 +9,5 @@ main.c ^SIGNAL=0$ -- -- -This test checks that verification succeeds when assigns clauses are respected through multiple function calls. +This test checks that verification succeeds when assigns clauses are respected +through multiple function calls. diff --git a/regression/contracts/assigns_enforce_04/test.desc b/regression/contracts/assigns_enforce_04/test.desc index 35a898dd382..dd4edf44d7c 100644 --- a/regression/contracts/assigns_enforce_04/test.desc +++ b/regression/contracts/assigns_enforce_04/test.desc @@ -1,9 +1,6 @@ CORE main.c ---enforce-contract f1 -^\[f1.assigns.\d+\] line 1 Check that \*x1 is valid: SUCCESS$ -^\[f1.assigns.\d+\] line 1 Check that \*y1 is valid: SUCCESS$ -^\[f1.assigns.\d+\] line 1 Check that \*z1 is valid: SUCCESS$ +--dfcc main --enforce-contract f1 ^\[f3.assigns.\d+\] line 13 Check that \*x3 is assignable: SUCCESS$ ^\[f3.assigns.\d+\] line 14 Check that \*y3 is assignable: SUCCESS$ ^\[f3.assigns.\d+\] line 15 Check that \*z3 is assignable: SUCCESS$ diff --git a/regression/contracts/assigns_enforce_05/test.desc b/regression/contracts/assigns_enforce_05/test.desc index 97352a948f2..4432da69532 100644 --- a/regression/contracts/assigns_enforce_05/test.desc +++ b/regression/contracts/assigns_enforce_05/test.desc @@ -1,6 +1,6 @@ CORE main.c ---enforce-contract f1 --enforce-contract f2 --enforce-contract f3 +--dfcc main --enforce-contract f1 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts/assigns_enforce_06/main.c b/regression/contracts/assigns_enforce_06/main.c index e4d12d140f6..5987494a45e 100644 --- a/regression/contracts/assigns_enforce_06/main.c +++ b/regression/contracts/assigns_enforce_06/main.c @@ -1,41 +1,44 @@ -void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1) +void f1(int *x, int *y, int *z) __CPROVER_assigns(*x, *y, *z) { - f2(x1, y1, z1); + f2(x, y, z); } -void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2) +void f2(int *x, int *y, int *z) __CPROVER_assigns(*x, *y, *z) { - f3(x2, y2, z2); + f3(x, y, z); } -void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*x3, *y3, *z3) +void f3(int *x, int *y, int *z) __CPROVER_assigns(*x, *y, *z) { - *x3 = *x3 + 1; - *y3 = *y3 + 1; - *z3 = *z3 + 1; + *x = *x + 1; + *y = *y + 1; + *z = *z + 1; } -int main() +void f(int *x, int *y, int *z) __CPROVER_assigns(*x, *y, *z) { - int p = 1; - int q = 2; - int r = 3; - for(int i = 0; i < 3; ++i) { if(i == 0) { - f1(&p, &q, &r); + f1(x, y, z); } if(i == 1) { - f2(&p, &q, &r); + f2(x, y, z); } if(i == 2) { - f3(&p, &q, &r); + f3(x, y, z); } } +} +int main() +{ + int p = 1; + int q = 2; + int r = 3; + f(&p, &q, &r); return 0; } diff --git a/regression/contracts/assigns_enforce_06/test.desc b/regression/contracts/assigns_enforce_06/test.desc index 255dd3a361c..db14528b092 100644 --- a/regression/contracts/assigns_enforce_06/test.desc +++ b/regression/contracts/assigns_enforce_06/test.desc @@ -1,9 +1,10 @@ CORE main.c ---enforce-contract f1 --enforce-contract f2 --enforce-contract f3 +--dfcc main --enforce-contract f ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -- -This test checks that verification succeeds when functions with assigns clauses are called from within a loop. +This test checks that verification succeeds when functions +are called from within a loop. diff --git a/regression/contracts/assigns_enforce_07/main.c b/regression/contracts/assigns_enforce_07/main.c index 384807e6218..4d513625106 100644 --- a/regression/contracts/assigns_enforce_07/main.c +++ b/regression/contracts/assigns_enforce_07/main.c @@ -1,41 +1,46 @@ -void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1) +void f1(int *x, int *y, int *z) __CPROVER_assigns(*x, *y) { - f2(x1, y1, z1); + *x = *x + 1; + *y = *y + 1; } -void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2) +void f2(int *x, int *y, int *z) __CPROVER_assigns(*x, *y) { - f3(x2, y2, z2); + *x = *x + 1; + *y = *y + 1; } -void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*y3, *z3) +void f3(int *x, int *y, int *z) __CPROVER_assigns(*x, *y, *z) { - *x3 = *x3 + 1; - *y3 = *y3 + 1; - *z3 = *z3 + 1; + *x = *x + 1; + *y = *y + 1; + *z = *z + 1; } -int main() +void f(int *x, int *y, int *z) __CPROVER_assigns(*x, *y) { - int p = 1; - int q = 2; - int r = 3; - for(int i = 0; i < 3; ++i) { if(i == 0) { - f1(&p, &q, &r); + f1(x, y, z); } if(i == 1) { - f2(&p, &q, &r); + f2(x, y, z); } if(i == 2) { - f3(&p, &q, &r); + f3(x, y, z); } } +} +int main() +{ + int p = 1; + int q = 2; + int r = 3; + f(&p, &q, &r); return 0; } diff --git a/regression/contracts/assigns_enforce_07/test.desc b/regression/contracts/assigns_enforce_07/test.desc index cdf7220a8a1..e9f2d4f52df 100644 --- a/regression/contracts/assigns_enforce_07/test.desc +++ b/regression/contracts/assigns_enforce_07/test.desc @@ -1,6 +1,6 @@ CORE main.c ---enforce-contract f1 --enforce-contract f2 --enforce-contract f3 +--dfcc main --enforce-contract f ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/assigns_enforce_address_of/test.desc b/regression/contracts/assigns_enforce_address_of/test.desc index 7500be4b1e4..9b717247265 100644 --- a/regression/contracts/assigns_enforce_address_of/test.desc +++ b/regression/contracts/assigns_enforce_address_of/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$ +^.*error: assigns clause target must be an lvalue or a call to __CPROVER_POINTER_OBJECT or to a function returning __CPROVER_assignable_t$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc b/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc index 2a9141844c9..dd48913cefd 100644 --- a/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc +++ b/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc @@ -1,7 +1,7 @@ CORE main.c --enforce-contract foo -^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$ +^.*error: assigns clause target must be an lvalue or a call to __CPROVER_POINTER_OBJECT or to a function returning __CPROVER_assignable_t$ ^CONVERSION ERROR ^EXIT=(1|64)$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc b/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc index 2a9141844c9..dd48913cefd 100644 --- a/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc +++ b/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc @@ -1,7 +1,7 @@ CORE main.c --enforce-contract foo -^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$ +^.*error: assigns clause target must be an lvalue or a call to __CPROVER_POINTER_OBJECT or to a function returning __CPROVER_assignable_t$ ^CONVERSION ERROR ^EXIT=(1|64)$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_function_calls/test.desc b/regression/contracts/assigns_enforce_function_calls/test.desc index 5f482125c08..a8e3b382646 100644 --- a/regression/contracts/assigns_enforce_function_calls/test.desc +++ b/regression/contracts/assigns_enforce_function_calls/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: function calls in assigns clause targets must be to __CPROVER_object_from, __CPROVER_object_slice$ +^.*error: expecting __CPROVER_assignable_t return type for function bar called in assigns clause$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_literal/test.desc b/regression/contracts/assigns_enforce_literal/test.desc index 74d1d576235..d1952cdfe3c 100644 --- a/regression/contracts/assigns_enforce_literal/test.desc +++ b/regression/contracts/assigns_enforce_literal/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$ +^.*error: assigns clause target must be an lvalue or a call to __CPROVER_POINTER_OBJECT or to a function returning __CPROVER_assignable_t$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_side_effects_2/test.desc b/regression/contracts/assigns_enforce_side_effects_2/test.desc index 8cab6884f92..368481cb54d 100644 --- a/regression/contracts/assigns_enforce_side_effects_2/test.desc +++ b/regression/contracts/assigns_enforce_side_effects_2/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$ +^.*error: assigns clause target must be an lvalue or a call to __CPROVER_POINTER_OBJECT or to a function returning __CPROVER_assignable_t$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_side_effects_3/test.desc b/regression/contracts/assigns_enforce_side_effects_3/test.desc index 8cab6884f92..368481cb54d 100644 --- a/regression/contracts/assigns_enforce_side_effects_3/test.desc +++ b/regression/contracts/assigns_enforce_side_effects_3/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$ +^.*error: assigns clause target must be an lvalue or a call to __CPROVER_POINTER_OBJECT or to a function returning __CPROVER_assignable_t$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_type_checking_invalid_case_01/test.desc b/regression/contracts/assigns_type_checking_invalid_case_01/test.desc index 51c84807dcb..232c8b3f575 100644 --- a/regression/contracts/assigns_type_checking_invalid_case_01/test.desc +++ b/regression/contracts/assigns_type_checking_invalid_case_01/test.desc @@ -4,6 +4,6 @@ main.c ^EXIT=(1|64)$ ^SIGNAL=0$ ^CONVERSION ERROR$ -^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$ +^.*error: assigns clause target must be an lvalue or a call to __CPROVER_POINTER_OBJECT or to a function returning __CPROVER_assignable_t$ -- Checks whether type checking rejects literal constants in assigns clause. diff --git a/regression/contracts/cprover-assignable-fail/main.c b/regression/contracts/cprover-assignable-fail/main.c new file mode 100644 index 00000000000..9db72b0af93 --- /dev/null +++ b/regression/contracts/cprover-assignable-fail/main.c @@ -0,0 +1,29 @@ +#include + +__CPROVER_assignable_t my_write_set(char *arr, size_t size) +{ + __CPROVER_assert( + !arr || __CPROVER_rw_ok(arr, size), "target null or writable"); + + if(arr && size > 0) + { + __CPROVER_whole_object(arr); + __CPROVER_object_upto(arr, size); + __CPROVER_object_from(arr); + __CPROVER_typed_target(arr[0]); + } +} + +void main() +{ + size_t size; + char *arr; + int do_init; + if(do_init) + { + int nondet; + arr = nondet ? malloc(size) : NULL; + } + // pointer can be invalid expecting failed checks + my_write_set(arr, size); +} diff --git a/regression/contracts/cprover-assignable-fail/test.desc b/regression/contracts/cprover-assignable-fail/test.desc new file mode 100644 index 00000000000..0550c09fb40 --- /dev/null +++ b/regression/contracts/cprover-assignable-fail/test.desc @@ -0,0 +1,20 @@ +CORE +main.c + +CALL __CPROVER_whole_object +CALL __CPROVER_object_upto +CALL __CPROVER_object_from +CALL __CPROVER_assignable +^\[my_write_set.assertion.\d+\] .* target null or writable: FAILURE$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +CALL __CPROVER_typed_target +-- +This test checks that: +- built-in __CPROVER_assignable_t functions are supported; +- GOTO conversion preserves calls to __CPROVER_whole_object, + __CPROVER_object_upto, __CPROVER_object_from; +- GOTO conversion translates __CPROVER_typed_target to __CPROVER_assignable; +- user-defined checks embedded in `my_write_set` persist after conversion. diff --git a/regression/contracts/cprover-assignable-pass/main.c b/regression/contracts/cprover-assignable-pass/main.c new file mode 100644 index 00000000000..bbeb08acc03 --- /dev/null +++ b/regression/contracts/cprover-assignable-pass/main.c @@ -0,0 +1,25 @@ +#include + +__CPROVER_assignable_t my_write_set(char *arr, size_t size) +{ + __CPROVER_assert( + !arr || __CPROVER_rw_ok(arr, size), "target null or writable"); + + if(arr && size > 0) + { + __CPROVER_whole_object(arr); + __CPROVER_object_upto(arr, size); + __CPROVER_object_from(arr); + __CPROVER_typed_target(arr[0]); + } +} + +void main() +{ + int nondet; + size_t size; + char *arr; + arr = nondet ? malloc(size) : NULL; + // pointer is not invalid + my_write_set(arr, size); +} diff --git a/regression/contracts/cprover-assignable-pass/test.desc b/regression/contracts/cprover-assignable-pass/test.desc new file mode 100644 index 00000000000..ee96e43352f --- /dev/null +++ b/regression/contracts/cprover-assignable-pass/test.desc @@ -0,0 +1,20 @@ +CORE +main.c + +CALL __CPROVER_whole_object +CALL __CPROVER_object_upto +CALL __CPROVER_object_from +CALL __CPROVER_assignable +^\[my_write_set.assertion.\d+\] .* target null or writable: SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +CALL __CPROVER_typed_target +-- +This test checks that: +- built-in __CPROVER_assignable_t functions are supported; +- GOTO conversion preserves calls to __CPROVER_whole_object, + __CPROVER_object_upto, __CPROVER_object_from; +- GOTO conversion translates __CPROVER_typed_target to __CPROVER_assignable; +- user-defined checks embedded in `my_write_set` persist after conversion. diff --git a/regression/contracts/frees-clause-and-predicates-fail/main.c b/regression/contracts/frees-clause-and-predicates-fail/main.c new file mode 100644 index 00000000000..7285a551e6d --- /dev/null +++ b/regression/contracts/frees-clause-and-predicates-fail/main.c @@ -0,0 +1,46 @@ +#include + +// A function defining a conditionally freeable target +__CPROVER_freeable_t +foo_frees(char *arr, const size_t size, const size_t new_size) +{ + __CPROVER_freeable(arr); +} + +char *foo(char *arr, const size_t size, const size_t new_size) + // clang-format off + // error is_freed cannot be used in preconditions +__CPROVER_requires(!__CPROVER_is_freed(arr)) +__CPROVER_requires(__CPROVER_is_freeable(arr)) +__CPROVER_assigns(__CPROVER_whole_object(arr)) +__CPROVER_frees(foo_frees(arr, size, new_size)) +__CPROVER_ensures( + (arr && new_size > size) ==> + __CPROVER_is_fresh(__CPROVER_return_value, new_size)) +__CPROVER_ensures( + (arr && new_size > size) ==> + __CPROVER_is_freed(__CPROVER_old(arr))) +__CPROVER_ensures( + !(arr && new_size > size) ==> + __CPROVER_return_value == __CPROVER_old(arr)) +// clang-format on +{ + if(arr && new_size > size) + { + free(arr); + return malloc(new_size); + } + else + { + return arr; + } +} + +int main() +{ + size_t size; + size_t new_size; + char *arr = malloc(size); + arr = foo(arr, size, new_size); + return 0; +} diff --git a/regression/contracts/frees-clause-and-predicates-fail/test.desc b/regression/contracts/frees-clause-and-predicates-fail/test.desc new file mode 100644 index 00000000000..7c01104d8f6 --- /dev/null +++ b/regression/contracts/frees-clause-and-predicates-fail/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--enforce-contract foo +^main.c.* error: __CPROVER_is_freed is not allowed in preconditions.$ +^CONVERSION ERROR$ +^EXIT=(1|64)$ +^SIGNAL=0$ +-- +-- +This test checks that the front end rejects __CPROVER_is_freed in preconditions. diff --git a/regression/contracts/frees-clause-and-predicates-fail2/main.c b/regression/contracts/frees-clause-and-predicates-fail2/main.c new file mode 100644 index 00000000000..bf23353d665 --- /dev/null +++ b/regression/contracts/frees-clause-and-predicates-fail2/main.c @@ -0,0 +1,43 @@ +#include + +// A function defining a conditionally freeable target +void foo_frees(char *arr, const size_t size, const size_t new_size) +{ + __CPROVER_freeable(arr); +} + +char *foo(char *arr, const size_t size, const size_t new_size) + // clang-format off +__CPROVER_requires(__CPROVER_is_freeable(arr)) +__CPROVER_assigns(__CPROVER_whole_object(arr)) +__CPROVER_frees(foo_frees(arr, size, new_size)) +__CPROVER_ensures( + (arr && new_size > size) ==> + __CPROVER_is_fresh(__CPROVER_return_value, new_size)) +__CPROVER_ensures( + (arr && new_size > size) ==> + __CPROVER_is_freed(__CPROVER_old(arr))) +__CPROVER_ensures( + !(arr && new_size > size) ==> + __CPROVER_return_value == __CPROVER_old(arr)) +// clang-format on +{ + if(arr && new_size > size) + { + free(arr); + return malloc(new_size); + } + else + { + return arr; + } +} + +int main() +{ + size_t size; + size_t new_size; + char *arr = malloc(size); + arr = foo(arr, size, new_size); + return 0; +} diff --git a/regression/contracts/frees-clause-and-predicates-fail2/test.desc b/regression/contracts/frees-clause-and-predicates-fail2/test.desc new file mode 100644 index 00000000000..57230e0a51c --- /dev/null +++ b/regression/contracts/frees-clause-and-predicates-fail2/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--enforce-contract foo +^main.c.* error: expecting __CPROVER_freeable_t return type for function foo_frees called in frees clause$ +^CONVERSION ERROR$ +^EXIT=(1|64)$ +^SIGNAL=0$ +-- +-- +This test checks that the front-end rejects non-__CPROVER_freeable_t-typed +function calls in frees clauses. diff --git a/regression/contracts/frees-clause-and-predicates/main.c b/regression/contracts/frees-clause-and-predicates/main.c new file mode 100644 index 00000000000..74da4a8d4a7 --- /dev/null +++ b/regression/contracts/frees-clause-and-predicates/main.c @@ -0,0 +1,76 @@ +#include +#include + +// A function defining an assignable target +__CPROVER_assignable_t foo_assigns(char *arr, const size_t size) +{ + __CPROVER_object_upto(arr, size); +} + +// A function defining an freeable target +__CPROVER_freeable_t foo_frees(char *arr, const size_t size) +{ + __CPROVER_freeable(arr); +} + +bool is_freeable(void *ptr) +{ + bool is_dynamic_object = (ptr == 0) | __CPROVER_DYNAMIC_OBJECT(ptr); + bool has_offset_zero = (ptr == 0) | (__CPROVER_POINTER_OFFSET(ptr) == 0); + return is_dynamic_object & has_offset_zero; +} + +char *foo(char *ptr, const size_t size, const size_t new_size) + // clang-format off +__CPROVER_requires(__CPROVER_is_freeable(ptr)) +__CPROVER_assigns(foo_assigns(ptr, size)) +__CPROVER_frees(foo_frees(ptr, size)) +__CPROVER_ensures( + (ptr && new_size > size) ==> + __CPROVER_is_fresh(__CPROVER_return_value, new_size)) +__CPROVER_ensures( + (ptr && new_size > size) ==> + __CPROVER_is_freed(ptr)) +__CPROVER_ensures( + !(ptr && new_size > size) ==> + __CPROVER_return_value == __CPROVER_old(ptr)) +// clang-format on +{ + // The harness allows to add a nondet offset to the pointer passed to foo. + // Proving this assertion shows that the __CPROVER_is_freeable(ptr) assumption + // is in effect as expected for the verification + __CPROVER_assert(is_freeable(ptr), "ptr is freeable"); + + if(ptr && new_size > size) + { + free(ptr); + ptr = malloc(new_size); + + // write at some nondet i (should be always allowed since ptr is fresh) + size_t i; + if(i < new_size) + ptr[i] = 0; + + return ptr; + } + else + { + // write at some nondet i + size_t i; + if(i < size) + ptr[i] = 0; + + return ptr; + } +} + +int main() +{ + size_t size; + size_t new_size; + __CPROVER_assume(size < __CPROVER_max_malloc_size); + __CPROVER_assume(new_size < __CPROVER_max_malloc_size); + char *arr = malloc(size); + arr = foo(arr, size, new_size); + return 0; +} diff --git a/regression/contracts/frees-clause-and-predicates/test.desc b/regression/contracts/frees-clause-and-predicates/test.desc new file mode 100644 index 00000000000..13027907495 --- /dev/null +++ b/regression/contracts/frees-clause-and-predicates/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +-dfcc main --enforce-contract foo +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This test checks that using the -dffdfcc flag we can check contracts that use: +- __CPROVER_freeable_t function calls as frees clause targets +- the __CPROVER_freeable built-in +- the __CPROVER_is_freeable built-in predicate +- the __CPROVER_is_freed built-in predicate diff --git a/regression/contracts/frees-clause-for-loop-fail/main.c b/regression/contracts/frees-clause-for-loop-fail/main.c new file mode 100644 index 00000000000..715b93998dc --- /dev/null +++ b/regression/contracts/frees-clause-for-loop-fail/main.c @@ -0,0 +1,19 @@ +#include +int main() +{ + size_t size = 10; + char *arr = malloc(size); + + for(size_t i = 0; i <= size; i++) + // clang-format off + __CPROVER_assigns(i, arr[2], __CPROVER_POINTER_OBJECT(arr)) + __CPROVER_frees(arr[2]) + // clang-format on2 + { + if(i == 2) + arr[i] = 0; + if(i == size) + free(arr); + } + return 0; +} diff --git a/regression/contracts/frees-clause-for-loop-fail/test.desc b/regression/contracts/frees-clause-for-loop-fail/test.desc new file mode 100644 index 00000000000..84b08d72c84 --- /dev/null +++ b/regression/contracts/frees-clause-for-loop-fail/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--apply-loop-contracts +^main.c.*: error: frees clause target must be a pointer-typed expression or a call to a function returning __CPROVER_freeable_t$ +^CONVERSION ERROR$ +^EXIT=(1|64)$ +^SIGNAL=0$ +-- +-- +This test is expected trigger a typchecking error on a frees clause target. diff --git a/regression/contracts/frees-clause-for-loop-pass/main.c b/regression/contracts/frees-clause-for-loop-pass/main.c new file mode 100644 index 00000000000..5bd912d69e9 --- /dev/null +++ b/regression/contracts/frees-clause-for-loop-pass/main.c @@ -0,0 +1,19 @@ +#include +int main() +{ + size_t size = 10; + char *arr = malloc(size); + + for(size_t i = 0; i <= size; i++) + // clang-format off + __CPROVER_assigns(i, arr[2], __CPROVER_POINTER_OBJECT(arr)) + __CPROVER_frees(arr) + // clang-format on2 + { + if(i == 2) + arr[i] = 0; + if(i == size) + free(arr); + } + return 0; +} diff --git a/regression/contracts/frees-clause-for-loop-pass/test.desc b/regression/contracts/frees-clause-for-loop-pass/test.desc new file mode 100644 index 00000000000..85d74473748 --- /dev/null +++ b/regression/contracts/frees-clause-for-loop-pass/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--apply-loop-contracts +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This test checks that frees clauses are parsed and typechecked for for loops. diff --git a/regression/contracts/frees-clause-function-fail/main.c b/regression/contracts/frees-clause-function-fail/main.c new file mode 100644 index 00000000000..f25c8e0be67 --- /dev/null +++ b/regression/contracts/frees-clause-function-fail/main.c @@ -0,0 +1,19 @@ +#include + +int foo(char *arr, int size) + // clang-format off +__CPROVER_frees(size) +// clang-format on +{ + // the body does not actually free the array + // since we are only testing parsing and typechecking + return 0; +} + +int main() +{ + size_t size; + char *arr = malloc(size); + foo(arr, size); + return 0; +} diff --git a/regression/contracts/frees-clause-function-fail/test.desc b/regression/contracts/frees-clause-function-fail/test.desc new file mode 100644 index 00000000000..8c217f0a311 --- /dev/null +++ b/regression/contracts/frees-clause-function-fail/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--enforce-contract foo +^main.c.* error: frees clause target must be a pointer-typed expression or a call to a function returning __CPROVER_freeable_t$ +^CONVERSION ERROR$ +^EXIT=(1|64)$ +^SIGNAL=0$ +-- +-- +This test is expected trigger a typchecking error on a frees clause target. diff --git a/regression/contracts/frees-clause-function-pass/main.c b/regression/contracts/frees-clause-function-pass/main.c new file mode 100644 index 00000000000..99c5ee2b0e0 --- /dev/null +++ b/regression/contracts/frees-clause-function-pass/main.c @@ -0,0 +1,20 @@ +#include + +int foo(char *arr1, char *arr2, size_t size) + // clang-format off +__CPROVER_frees(size > 0 && arr1: arr1; arr2) +// clang-format on +{ + // the body does not actually free the function + // since we are only testing parsing and typechecking + return 0; +} + +int main() +{ + size_t size; + char *arr1 = malloc(size); + char *arr2 = malloc(size); + foo(arr1, arr2, size); + return 0; +} diff --git a/regression/contracts/frees-clause-function-pass/test.desc b/regression/contracts/frees-clause-function-pass/test.desc new file mode 100644 index 00000000000..88f63207658 --- /dev/null +++ b/regression/contracts/frees-clause-function-pass/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--enforce-contract foo +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that frees clauses are parsed and typechecked. diff --git a/regression/contracts/frees-clause-while-loop-fail/main.c b/regression/contracts/frees-clause-while-loop-fail/main.c new file mode 100644 index 00000000000..e49afea1bb3 --- /dev/null +++ b/regression/contracts/frees-clause-while-loop-fail/main.c @@ -0,0 +1,20 @@ +#include +int main() +{ + size_t size = 10; + char *arr = malloc(size); + size_t i = 0; + while(i <= size) + // clang-format off + __CPROVER_assigns(i, arr[2], __CPROVER_POINTER_OBJECT(arr)) + __CPROVER_frees(arr[2]) + // clang-format on2 + { + if(i == 2) + arr[i] = 0; + if(i == size) + free(arr); + i++; + } + return 0; +} diff --git a/regression/contracts/frees-clause-while-loop-fail/test.desc b/regression/contracts/frees-clause-while-loop-fail/test.desc new file mode 100644 index 00000000000..e2d39e5a965 --- /dev/null +++ b/regression/contracts/frees-clause-while-loop-fail/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--apply-loop-contracts +^main.c.* error: frees clause target must be a pointer-typed expression or a call to a function returning __CPROVER_freeable_t$ +^CONVERSION ERROR$ +^EXIT=(1|64)$ +^SIGNAL=0$ +-- +-- +This test is expected trigger a typchecking error on a frees clause target. diff --git a/regression/contracts/frees-clause-while-loop-pass/main.c b/regression/contracts/frees-clause-while-loop-pass/main.c new file mode 100644 index 00000000000..d8a1edbfae9 --- /dev/null +++ b/regression/contracts/frees-clause-while-loop-pass/main.c @@ -0,0 +1,20 @@ +#include +int main() +{ + size_t size = 10; + char *arr = malloc(size); + size_t i = 0; + while(i <= size) + // clang-format off + __CPROVER_assigns(i, arr[2], __CPROVER_POINTER_OBJECT(arr)) + __CPROVER_frees(arr) + // clang-format on2 + { + if(i == 2) + arr[i] = 0; + if(i == size) + free(arr); + i++; + } + return 0; +} diff --git a/regression/contracts/frees-clause-while-loop-pass/test.desc b/regression/contracts/frees-clause-while-loop-pass/test.desc new file mode 100644 index 00000000000..44420a4a998 --- /dev/null +++ b/regression/contracts/frees-clause-while-loop-pass/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--apply-loop-contracts +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This test checks that frees clauses are parsed and typechecked for while loops. diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index cb5beb98a2c..270daf1da2a 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -273,6 +273,14 @@ void ansi_c_convert_typet::read_rec(const typet &type) for(const exprt &target : to_unary_expr(as_expr).op().operands()) assigns.push_back(target); } + else if(type.id() == ID_C_spec_frees) + { + const exprt &as_expr = + static_cast(static_cast(type)); + + for(const exprt &target : to_unary_expr(as_expr).op().operands()) + frees.push_back(target); + } else if(type.id() == ID_C_spec_ensures) { const exprt &as_expr = @@ -341,6 +349,9 @@ void ansi_c_convert_typet::write(typet &type) if(!assigns.empty()) to_code_with_contract_type(type).assigns() = std::move(assigns); + if(!frees.empty()) + to_code_with_contract_type(type).frees() = std::move(frees); + if(!ensures.empty()) to_code_with_contract_type(type).ensures() = std::move(ensures); diff --git a/src/ansi-c/ansi_c_convert_type.h b/src/ansi-c/ansi_c_convert_type.h index 83f65ffe3ff..1eabc279006 100644 --- a/src/ansi-c/ansi_c_convert_type.h +++ b/src/ansi-c/ansi_c_convert_type.h @@ -47,7 +47,7 @@ class ansi_c_convert_typet:public messaget bool constructor, destructor; // contracts - exprt::operandst assigns, ensures, requires, ensures_contract, + exprt::operandst assigns, frees, ensures, requires, ensures_contract, requires_contract; // storage spec diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 6ea08fb5b44..fabb546b528 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -216,6 +216,29 @@ void ansi_c_internal_additions(std::string &code) // This function needs to be declared, or otherwise can't be called // by the entry-point construction. "void " INITIALIZE_FUNCTION "(void);\n" + "\n" + // frame specifications for contracts + // Type that describes assignable memory locations + "typedef void " CPROVER_PREFIX "assignable_t;\n" + // Declares a range of bytes as assignable (internal representation) + CPROVER_PREFIX "assignable_t " CPROVER_PREFIX "assignable(void *ptr, " + CPROVER_PREFIX "size_t size," + CPROVER_PREFIX "bool is_ptr_to_ptr);\n" + // Declares a range of bytes as assignable + CPROVER_PREFIX "assignable_t " CPROVER_PREFIX "object_upto(void *ptr, " + CPROVER_PREFIX "size_t size);\n" + // Declares bytes from ptr to the end of the object as assignable + CPROVER_PREFIX "assignable_t " CPROVER_PREFIX "object_from(void *ptr);\n" + // Declares the whole object pointer to by ptr + CPROVER_PREFIX "assignable_t " CPROVER_PREFIX "whole_object(void *ptr);\n" + // Type that describes sets of freeable pointers + "typedef void " CPROVER_PREFIX "freeable_t;\n" + // Declares a pointer as freeable + CPROVER_PREFIX "freeable_t " CPROVER_PREFIX "freeable(void *ptr);\n" + // True iff ptr satisfies the preconditions of the free stdlib function + CPROVER_PREFIX "bool " CPROVER_PREFIX "is_freeable(void *ptr);\n" + // True iff ptr was freed during function execution or loop execution + CPROVER_PREFIX "bool " CPROVER_PREFIX "is_freed(void *ptr);\n" "\n"; // clang-format on diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index a10ae5847e2..ef07dde57f8 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -777,6 +777,42 @@ void c_typecheck_baset::typecheck_declaration( CPROVER_PREFIX "loop_entry is not allowed in preconditions."); }; + auto check_return_value = [&](const exprt &expr) { + const irep_idt id = CPROVER_PREFIX "return_value"; + + auto pred = [&](const exprt &expr) { + if(!can_cast_expr(expr)) + return false; + + return to_symbol_expr(expr).get_identifier() == id; + }; + + if(!has_subexpr(expr, pred)) + return; + + error().source_location = expr.source_location(); + error() << id2string(id) + " is not allowed in preconditions." << eom; + throw 0; + }; + + auto check_is_freed = [&](const exprt &expr) { + const irep_idt id = CPROVER_PREFIX "is_freed"; + + auto pred = [&](const exprt &expr) { + if(!can_cast_expr(expr)) + return false; + + return to_symbol_expr(expr).get_identifier() == id; + }; + + if(!has_subexpr(expr, pred)) + return; + + error().source_location = expr.source_location(); + error() << id2string(id) + " is not allowed in preconditions." << eom; + throw 0; + }; + // check the contract, if any symbolt &new_symbol = symbol_table.get_writeable_ref(identifier); if( @@ -833,6 +869,8 @@ void c_typecheck_baset::typecheck_declaration( typecheck_expr(requires); implicit_typecast_bool(requires); check_history_expr(requires); + check_return_value(requires); + check_is_freed(requires); lambda_exprt lambda{temporary_parameter_symbols, requires}; lambda.add_source_location() = requires.source_location(); requires.swap(lambda); @@ -846,6 +884,14 @@ void c_typecheck_baset::typecheck_declaration( assigns.swap(lambda); } + typecheck_spec_frees(code_type.frees()); + for(auto &frees : code_type.frees()) + { + lambda_exprt lambda{temporary_parameter_symbols, frees}; + lambda.add_source_location() = frees.source_location(); + frees.swap(lambda); + } + for(auto &expr : code_type.ensures_contract()) { typecheck_spec_function_pointer_obeys_contract(expr); @@ -898,6 +944,7 @@ void c_typecheck_baset::typecheck_declaration( // Remove the contract from the original symbol as we have created a // dedicated contract symbol. new_symbol.type.remove(ID_C_spec_assigns); + new_symbol.type.remove(ID_C_spec_frees); new_symbol.type.remove(ID_C_spec_ensures); new_symbol.type.remove(ID_C_spec_ensures_contract); new_symbol.type.remove(ID_C_spec_requires); diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index 10dbb1f8196..f9080af5eb8 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -148,10 +148,17 @@ class c_typecheck_baset: // contracts virtual void typecheck_spec_function_pointer_obeys_contract(exprt &expr); virtual void typecheck_spec_assigns(exprt::operandst &targets); - virtual void typecheck_spec_assigns_condition(exprt &condition); + virtual void typecheck_spec_frees(exprt::operandst &targets); + virtual void typecheck_conditional_targets( + exprt::operandst &targets, + const std::function typecheck_target, + const std::string &clause_type); + virtual void typecheck_spec_condition(exprt &condition); virtual void typecheck_spec_assigns_target(exprt &target); + virtual void typecheck_spec_frees_target(exprt &target); virtual void typecheck_spec_loop_invariant(codet &code); virtual void typecheck_spec_decreases(codet &code); + virtual void throw_on_side_effects(const exprt &expr); bool break_is_allowed; bool continue_is_allowed; diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index a27585d8022..613cc308602 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -505,6 +505,12 @@ void c_typecheck_baset::typecheck_for(codet &code) typecheck_spec_assigns( static_cast(code.add(ID_C_spec_assigns)).op().operands()); } + + if(code.find(ID_C_spec_frees).is_not_nil()) + { + typecheck_spec_frees( + static_cast(code.add(ID_C_spec_frees)).op().operands()); + } } void c_typecheck_baset::typecheck_label(code_labelt &code) @@ -805,6 +811,12 @@ void c_typecheck_baset::typecheck_while(code_whilet &code) typecheck_spec_assigns( static_cast(code.add(ID_C_spec_assigns)).op().operands()); } + + if(code.find(ID_C_spec_frees).is_not_nil()) + { + typecheck_spec_frees( + static_cast(code.add(ID_C_spec_frees)).op().operands()); + } } void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code) @@ -845,9 +857,15 @@ void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code) typecheck_spec_assigns( static_cast(code.add(ID_C_spec_assigns)).op().operands()); } + + if(code.find(ID_C_spec_frees).is_not_nil()) + { + typecheck_spec_frees( + static_cast(code.add(ID_C_spec_frees)).op().operands()); + } } -void c_typecheck_baset::typecheck_spec_assigns_condition(exprt &condition) +void c_typecheck_baset::typecheck_spec_condition(exprt &condition) { // compute type typecheck_expr(condition); @@ -903,13 +921,36 @@ void c_typecheck_baset::typecheck_spec_assigns_condition(exprt &condition) throw 0; } +void c_typecheck_baset::throw_on_side_effects(const exprt &expr) +{ + if(has_subexpr(expr, ID_side_effect)) + { + error().source_location = expr.source_location(); + error() << "side-effects not allowed in assigns clause targets" + << messaget::eom; + throw 0; + } + if(has_subexpr(expr, ID_if)) + { + error().source_location = expr.source_location(); + error() << "ternary expressions not allowed in assigns " + "clause targets" + << messaget::eom; + throw 0; + } +} + void c_typecheck_baset::typecheck_spec_assigns_target(exprt &target) { // compute type typecheck_expr(target); // fatal errors - if(target.type().id() == ID_empty) + bool is_empty_type = target.type().id() == ID_empty; + bool is_assignable_typedef = + target.type().get(ID_C_typedef) == CPROVER_PREFIX "assignable_t"; + // only allow void type if it is the typedef CPROVER_PREFIX "assignable_t" + if(target.type().id() == ID_empty && !is_assignable_typedef) { error().source_location = target.source_location(); error() << "void-typed expressions not allowed as assigns clause targets" @@ -917,25 +958,6 @@ void c_typecheck_baset::typecheck_spec_assigns_target(exprt &target) throw 0; } - // throws exception if expr contains side effect or ternary expr - auto throw_on_side_effects = [&](const exprt &expr) { - if(has_subexpr(expr, ID_side_effect)) - { - error().source_location = expr.source_location(); - error() << "side-effects not allowed in assigns clause targets" - << messaget::eom; - throw 0; - } - if(has_subexpr(expr, ID_if)) - { - error().source_location = expr.source_location(); - error() << "ternary expressions not allowed in assigns " - "clause targets" - << messaget::eom; - throw 0; - } - }; - if(target.get_bool(ID_C_lvalue)) { throw_on_side_effects(target); @@ -950,36 +972,84 @@ void c_typecheck_baset::typecheck_spec_assigns_target(exprt &target) if(can_cast_expr(funcall.function())) { const auto &ident = to_symbol_expr(funcall.function()).get_identifier(); - if( - ident == CPROVER_PREFIX "object_from" || ident == CPROVER_PREFIX - "object_slice") - { - for(const auto &argument : funcall.arguments()) - throw_on_side_effects(argument); - } - else + if(!(is_empty_type && is_assignable_typedef)) { error().source_location = target.source_location(); - error() << "function calls in assigns clause targets must be " - "to " CPROVER_PREFIX "object_from, " CPROVER_PREFIX - "object_slice" + error() << "expecting " CPROVER_PREFIX + "assignable_t return type for function " + + id2string(ident) + " called in assigns clause" << eom; throw 0; } + for(const auto &argument : funcall.arguments()) + throw_on_side_effects(argument); } else { error().source_location = target.source_location(); - error() << "function pointer calls not allowed in assigns targets" << eom; + error() << "function pointer calls not allowed in assigns clauses" << eom; throw 0; } } else { error().source_location = target.source_location(); - error() << "assigns clause target must be an lvalue or a " CPROVER_PREFIX - "POINTER_OBJECT, " CPROVER_PREFIX "object_from, " CPROVER_PREFIX - "object_slice expression" + error() + << "assigns clause target must be an lvalue or a call to " CPROVER_PREFIX + "POINTER_OBJECT or to a function returning " CPROVER_PREFIX + "assignable_t" + << eom; + throw 0; + } +} + +void c_typecheck_baset::typecheck_spec_frees_target(exprt &target) +{ + // compute type + typecheck_expr(target); + const auto &type = target.type(); + + if(can_cast_type(type)) + { + // an expression with pointer-type without side effects + throw_on_side_effects(target); + } + else if(can_cast_expr(target)) + { + // A call to a freeable_t function symbol without other side effects + const auto &funcall = to_side_effect_expr_function_call(target); + + if(!can_cast_expr(funcall.function())) + { + error().source_location = target.source_location(); + error() << "function pointer calls not allowed in frees clauses" << eom; + throw 0; + } + + bool has_freeable_type = + (type.id() == ID_empty) && + (type.get(ID_C_typedef) == CPROVER_PREFIX "freeable_t"); + if(!has_freeable_type) + { + error().source_location = target.source_location(); + error() << "expecting " CPROVER_PREFIX + "freeable_t return type for function " + + id2string( + to_symbol_expr(funcall.function()).get_identifier()) + + " called in frees clause" + << eom; + throw 0; + } + + for(const auto &argument : funcall.arguments()) + throw_on_side_effects(argument); + } + else + { + // anything else is rejected + error().source_location = target.source_location(); + error() << "frees clause target must be a pointer-typed expression or a " + "call to a function returning " CPROVER_PREFIX "freeable_t" << eom; throw 0; } @@ -1067,7 +1137,10 @@ void c_typecheck_baset::typecheck_spec_function_pointer_obeys_contract( } } -void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets) +void c_typecheck_baset::typecheck_conditional_targets( + exprt::operandst &targets, + const std::function typecheck_target, + const std::string &clause_type) { exprt::operandst tmp; bool must_throw = false; @@ -1078,8 +1151,8 @@ void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets) { must_throw = true; error().source_location = target.source_location(); - error() << "expected ID_conditional_target_group expression in assigns " - "clause, found " + error() << "expected ID_conditional_target_group expression in " + + clause_type + "clause, found " << id2string(target.id()) << eom; } @@ -1088,7 +1161,7 @@ void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets) // typecheck condition auto &condition = conditional_target_group.condition(); - typecheck_spec_assigns_condition(condition); + typecheck_spec_condition(condition); if(condition.is_true()) { @@ -1096,7 +1169,7 @@ void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets) // simplify expr and expose the bare expressions for(auto &actual_target : conditional_target_group.targets()) { - typecheck_spec_assigns_target(actual_target); + typecheck_target(actual_target); tmp.push_back(actual_target); } } @@ -1105,7 +1178,7 @@ void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets) // if the condition is not trivially true, typecheck in place for(auto &actual_target : conditional_target_group.targets()) { - typecheck_spec_assigns_target(actual_target); + typecheck_target(actual_target); } tmp.push_back(std::move(target)); } @@ -1123,6 +1196,22 @@ void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets) std::swap(targets, tmp); } +void c_typecheck_baset::typecheck_spec_frees(exprt::operandst &targets) +{ + const std::function typecheck_target = [&](exprt &target) { + typecheck_spec_frees_target(target); + }; + typecheck_conditional_targets(targets, typecheck_target, "frees"); +} + +void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets) +{ + const std::function typecheck_target = [&](exprt &target) { + typecheck_spec_assigns_target(target); + }; + typecheck_conditional_targets(targets, typecheck_target, "assigns"); +} + void c_typecheck_baset::typecheck_spec_loop_invariant(codet &code) { if(code.find(ID_C_spec_loop_invariant).is_not_nil()) diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 7e560ec7c47..f4876f53d81 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -492,7 +492,9 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr) { // already type checked } - else if(expr.id() == ID_C_spec_assigns || expr.id() == ID_target_list) + else if( + expr.id() == ID_C_spec_assigns || expr.id() == ID_C_spec_frees || + expr.id() == ID_target_list) { // already type checked } @@ -1949,8 +1951,54 @@ void c_typecheck_baset::typecheck_side_effect_function_call( if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end()) { // This is an undeclared function. + + // Is it the polymorphic typed_target function ? + if(identifier == CPROVER_PREFIX "typed_target") + { + if(expr.arguments().size() != 1) + { + error().source_location = f_op.source_location(); + error() << "expected 1 argument for " << CPROVER_PREFIX "typed_target" + << " found " << expr.arguments().size() << eom; + throw 0; + } + + auto arg0 = expr.arguments().at(0); + typecheck_expr(arg0); + if(!is_assignable(arg0) || !arg0.get_bool(ID_C_lvalue)) + { + error().source_location = arg0.source_location(); + error() << "argument of " << CPROVER_PREFIX "typed_target" + << "must be assignable" << eom; + throw 0; + } + const auto &size = size_of_expr(arg0.type(), *this); + if(!size.has_value()) + { + error().source_location = arg0.source_location(); + error() << "sizeof not defined for argument of " + << CPROVER_PREFIX "typed_target" + << " of type " << to_string(arg0.type()) << eom; + throw 0; + } + // rewrite call to "assignable" + to_symbol_expr(f_op).set_identifier(CPROVER_PREFIX "assignable"); + exprt::operandst arguments; + // pointer + arguments.push_back(address_of_exprt(arg0)); + // size + arguments.push_back(size.value()); + // is_pointer + if(arg0.type().id() == ID_pointer) + arguments.push_back(true_exprt()); + else + arguments.push_back(false_exprt()); + + expr.arguments().swap(arguments); + typecheck_side_effect_function_call(expr); + } // Is this a builtin? - if(!builtin_factory(identifier, symbol_table, get_message_handler())) + else if(!builtin_factory(identifier, symbol_table, get_message_handler())) { // yes, it's a builtin } @@ -2207,6 +2255,42 @@ exprt c_typecheck_baset::do_special_functions( typecheck_function_call_arguments(expr); return nil_exprt(); } + if(identifier == CPROVER_PREFIX "is_freshr") + { + if(expr.arguments().size() != 2) + { + error().source_location = f_op.source_location(); + error() << CPROVER_PREFIX "is_freshr expects two operands; " + << expr.arguments().size() << "provided." << eom; + throw 0; + } + typecheck_function_call_arguments(expr); + return nil_exprt(); + } + else if(identifier == CPROVER_PREFIX "is_freeable") + { + if(expr.arguments().size() != 1) + { + error().source_location = f_op.source_location(); + error() << CPROVER_PREFIX "is_freeable expects one operand; " + << expr.arguments().size() << "provided." << eom; + throw 0; + } + typecheck_function_call_arguments(expr); + return nil_exprt(); + } + else if(identifier == CPROVER_PREFIX "is_freed") + { + if(expr.arguments().size() != 1) + { + error().source_location = f_op.source_location(); + error() << CPROVER_PREFIX "is_freed expects one operand; " + << expr.arguments().size() << "provided." << eom; + throw 0; + } + typecheck_function_call_arguments(expr); + return nil_exprt(); + } else if(identifier == CPROVER_PREFIX "same_object") { if(expr.arguments().size()!=2) diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h index 17876ea8981..e00f0d3c0e3 100644 --- a/src/ansi-c/cprover_builtin_headers.h +++ b/src/ansi-c/cprover_builtin_headers.h @@ -45,7 +45,11 @@ void __CPROVER_atomic_end(); void __CPROVER_fence(const char *kind, ...); // contract-related functions +__CPROVER_bool __CPROVER_is_freeable(const void *mem); +__CPROVER_bool __CPROVER_is_freed(const void *mem); __CPROVER_bool __CPROVER_is_fresh(const void *mem, __CPROVER_size_t size); +// Is fresh, reference version (pronounced "fresher") +__CPROVER_bool __CPROVER_is_freshr(const void **mem, __CPROVER_size_t size); void __CPROVER_old(const void *); void __CPROVER_loop_entry(const void *); @@ -134,6 +138,10 @@ __CPROVER_bool __CPROVER_overflow_unary_minus(); __CPROVER_bool __CPROVER_enum_is_in_range(); // contracts -__CPROVER_size_t __CPROVER_object_from(void *); -__CPROVER_size_t __CPROVER_object_slice(void *, __CPROVER_size_t); +__CPROVER_assignable_t __CPROVER_assignable(void *ptr, __CPROVER_size_t size, + __CPROVER_bool is_ptr_to_ptr); +__CPROVER_assignable_t __CPROVER_whole_object(void *ptr); +__CPROVER_assignable_t __CPROVER_object_from(void *ptr); +__CPROVER_assignable_t __CPROVER_object_upto(void *ptr, __CPROVER_size_t size); +__CPROVER_assignable_t __CPROVER_freeable(void *ptr); // clang-format on diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h index 16b17990ea8..e62818879f8 100644 --- a/src/ansi-c/library/cprover.h +++ b/src/ansi-c/library/cprover.h @@ -17,6 +17,10 @@ Author: Daniel Kroening, kroening@kroening.com typedef __typeof__(sizeof(int)) __CPROVER_size_t; // NOLINTNEXTLINE(readability/identifiers) typedef signed long long __CPROVER_ssize_t; +// NOLINTNEXTLINE(readability/identifiers) +typedef void __CPROVER_assignable_t; +// NOLINTNEXTLINE(readability/identifiers) +typedef void __CPROVER_freeable_t; void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero); void __CPROVER_deallocate(void *); diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c new file mode 100644 index 00000000000..714c6287476 --- /dev/null +++ b/src/ansi-c/library/cprover_contracts.c @@ -0,0 +1,3518 @@ +/// \file cprover_contracts.c +/// This file defines types functions supporting dynamic frames in contracts. + +/* FUNCTION: __CPROVER_contracts_car_create */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +/// \brief A conditionally writable range of bytes. +typedef struct __CPROVER_contracts_car_t +{ + /// \brief True iff __CPROVER_w_ok(lb, size) holds at creation + __CPROVER_bool is_writable; + /// \brief Size of the range in bytes + __CPROVER_size_t size; + /// \brief Lower bound address of the range + void *lb; + /// \brief Upper bound address of the range + void *ub; +} __CPROVER_contracts_car_t; + +/// \brief A set of \ref __CPROVER_contracts_car_t. +typedef struct __CPROVER_contracts_car_set_t +{ + /// \brief Maximum number of elements that can be stored in the set + __CPROVER_size_t max_elems; + /// \brief An array of car_t of size max_elems + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +/// \brief Type of pointers to \ref __CPROVER_contracts_car_set_t. +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +/// \brief A set of pointers. +typedef struct __CPROVER_contracts_obj_set_t +{ + /// \brief Maximum number of elements that can be stored in the set + __CPROVER_size_t max_elems; + /// \brief next usable index in elems if less than max_elems + /// (1 + greatest used index in elems) + __CPROVER_size_t watermark; + /// \brief Number of elements currently in the elems array + __CPROVER_size_t nof_elems; + /// \brief True iff nof_elems is 0 + __CPROVER_bool is_empty; + /// \brief True iff elems is indexed by the object id of the pointers + __CPROVER_bool indexed_by_object_id; + /// \brief Array of void *pointers, indexed by their object ID + /// or some other order + void **elems; +} __CPROVER_contracts_obj_set_t; + +/// \brief Type of pointers to \ref __CPROVER_contracts_car_set_t. +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +/// \brief Runtime representation of a write set. +typedef struct __CPROVER_contracts_write_set_t +{ + /// \brief Set of car derived from the contract + __CPROVER_contracts_car_set_t contract_assigns; + /// \brief Set of freeable pointers derived from the contract (indexed mode) + __CPROVER_contracts_obj_set_t contract_frees; + /// \brief Set of freeable pointers derived from the contract (append mode) + __CPROVER_contracts_obj_set_t contract_frees_replacement; + /// \brief Set of objects allocated by the function under analysis + /// (indexed mode) + __CPROVER_contracts_obj_set_t allocated; + /// \brief Set of objects deallocated by the function under analysis + /// (indexed mode) + __CPROVER_contracts_obj_set_t deallocated; + /// \brief Object set supporting the is_freshr predicate checks + /// (indexed mode) + __CPROVER_contracts_obj_set_t is_freshr_seen; + /// \brief Object set recording the is_freshr allocations in post conditions + /// (replacement mode only) + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + /// \brief Object set recording the deallocations (used by predicate is_freed) + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + /// \brief True iff this write set is used for contract replacement + __CPROVER_bool replacement; + /// \brief True iff the write set checks requires clauses in an assumption ctx + __CPROVER_bool assume_requires_ctx; + /// \brief True iff the write set checks requires clauses in an assertion ctx + __CPROVER_bool assert_requires_ctx; + /// \brief True iff the write set checks ensures clauses in an assumption ctx + __CPROVER_bool assume_ensures_ctx; + /// \brief True iff this write set checks ensures clauses in an assertion ctx + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; +/// \brief Type of pointers to \ref __CPROVER_contracts_write_set_t. +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +/// \brief Creates a __CPROVER_car_t struct from \p ptr and \p size +/// \param[in] ptr Start address of the range +/// \param[in] size Size in bytes +/// \return A \ref __CPROVER_contracts_car_t value +inline __CPROVER_contracts_car_t +__CPROVER_contracts_car_create(void *ptr, __CPROVER_size_t size) +{ +__CPROVER_HIDE:; +#pragma CPROVER check push +#pragma CPROVER check disable "pointer" +#pragma CPROVER check disable "pointer-primitive" +#pragma CPROVER check disable "unsigned-overflow" +#pragma CPROVER check disable "signed-overflow" +#pragma CPROVER check disable "undefined-shift" +#pragma CPROVER check disable "conversion" + __CPROVER_assert( + ((ptr == 0) | __CPROVER_rw_ok(ptr, size)), + "ptr NULL or writable up to size"); + __CPROVER_contracts_car_t car = {0}; + car.is_writable = ptr != 0; + car.size = size; + car.lb = ptr; + __CPROVER_assert( + size < __CPROVER_max_malloc_size, + "CAR size is less than __CPROVER_max_malloc_size"); + __CPROVER_ssize_t offset = __CPROVER_POINTER_OFFSET(ptr); + __CPROVER_assert( + !(offset > 0) | + ((__CPROVER_size_t)offset + size < __CPROVER_max_malloc_size), + "no offset bits overflow on CAR upper bound computation"); + car.ub = (void *)((char *)ptr + size); +#pragma CPROVER check pop + return car; +} + +/* FUNCTION: __CPROVER_contracts_car_set_create */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +/// \brief Initialises a __CPROVER_contracts_car_set_ptr_t object +/// \param[inout] set Pointer to the object to initialise +/// \param[in] max_elems Max number of elements to store in the set +inline void __CPROVER_contracts_car_set_create( + __CPROVER_contracts_car_set_ptr_t set, + // maximum number of elements that can be stored in the set + __CPROVER_size_t max_elems) +{ +__CPROVER_HIDE:; +#ifdef DFCC_SELF_CHECK + __CPROVER_assert( + __CPROVER_rw_ok(set, sizeof(__CPROVER_contracts_car_set_t)), + "set writable"); +#endif + set->max_elems = max_elems; + set->elems = + __CPROVER_allocate(max_elems * sizeof(__CPROVER_contracts_car_t), 1); +} + +/* FUNCTION: __CPROVER_contracts_car_set_insert */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +extern __CPROVER_size_t __CPROVER_max_malloc_size; + +/// \brief Inserts a \ref __CPROVER_contracts_car_t snapshotted from \p ptr +/// and \p size into \p set at index \p idx. +/// \param[inout] set Set to insert into +/// \param[in] idx Insertion index +/// \param[in] ptr Pointer to the range of bytes +/// \param[in] size Size of the range in number of bytes +inline void __CPROVER_contracts_car_set_insert( + __CPROVER_contracts_car_set_ptr_t set, + __CPROVER_size_t idx, + void *ptr, + __CPROVER_size_t size) +{ +__CPROVER_HIDE:; +#pragma CPROVER check push +#pragma CPROVER check disable "pointer" +#pragma CPROVER check disable "pointer-overflow" +#pragma CPROVER check disable "pointer-primitive" +#pragma CPROVER check disable "unsigned-overflow" +#pragma CPROVER check disable "signed-overflow" +#pragma CPROVER check disable "undefined-shift" +#pragma CPROVER check disable "conversion" +#ifdef DFCC_SELF_CHECK + __CPROVER_assert((set != 0) & (idx < set->max_elems), "no OOB access"); +#endif + __CPROVER_assert( + ((ptr == 0) | __CPROVER_rw_ok(ptr, size)), + "ptr NULL or writable up to size"); + __CPROVER_contracts_car_t *elem = set->elems + idx; + elem->is_writable = ptr != 0; + elem->size = size; + elem->lb = ptr; + __CPROVER_assert( + size < __CPROVER_max_malloc_size, + "CAR size is less than __CPROVER_max_malloc_size"); + __CPROVER_ssize_t offset = __CPROVER_POINTER_OFFSET(ptr); + __CPROVER_assert( + !(offset > 0) | + ((__CPROVER_size_t)offset + size < __CPROVER_max_malloc_size), + "no offset bits overflow on CAR upper bound computation"); + elem->ub = (void *)((char *)ptr + size); +#pragma CPROVER check pop +} + +/* FUNCTION: __CPROVER_contracts_car_set_remove */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +/// \brief Invalidates all cars in the \p set that point into the same object +/// as the given \p ptr. +/// \param[inout] set Set to update +/// \param[in] ptr Pointer to the object to invalidate +void __CPROVER_contracts_car_set_remove( + __CPROVER_contracts_car_set_ptr_t set, + void *ptr) +{ +__CPROVER_HIDE:; + __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr); + __CPROVER_size_t idx = set->max_elems; + __CPROVER_contracts_car_t *elem = set->elems; +CAR_SET_REMOVE_LOOP: + while(idx != 0) + { + if(object_id == __CPROVER_POINTER_OBJECT(elem->lb)) + elem->is_writable = 0; + ++elem; + --idx; + } +} + +/* FUNCTION: __CPROVER_contracts_car_set_contains */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +/// \brief Checks if \p candidate is included in one of \p set 's elements. +/// \param[in] set Set to check inclusion in +/// \param[in] candidate A candidate \ref __CPROVER_contracts_car_t +/// \return True iff an element of \p set contains \p candidate +inline __CPROVER_bool __CPROVER_contracts_car_set_contains( + __CPROVER_contracts_car_set_ptr_t set, + __CPROVER_contracts_car_t candidate) +{ +__CPROVER_HIDE:; + __CPROVER_bool incl = 0; + __CPROVER_size_t idx = set->max_elems; + __CPROVER_contracts_car_t *elem = set->elems; +CAR_SET_CONTAINS_LOOP: + while(idx != 0) + { + incl |= candidate.is_writable & elem->is_writable & + __CPROVER_same_object(elem->lb, candidate.lb) & + (__CPROVER_POINTER_OFFSET(elem->lb) <= + __CPROVER_POINTER_OFFSET(candidate.lb)) & + (__CPROVER_POINTER_OFFSET(candidate.ub) <= + __CPROVER_POINTER_OFFSET(elem->ub)); + ++elem; + --idx; + } + + return incl; +} + +/* FUNCTION: __CPROVER_contracts_obj_set_create_indexed_by_object_id */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +extern __CPROVER_size_t __CPROVER_max_malloc_size; + +/// \brief Count the number of leading zeroes in an unsigned long long +int __builtin_clzll(unsigned long long); + +/// \brief Initialises a \ref __CPROVER_contracts_obj_set_t object to use it +/// in "indexed by object id" mode. +/// +/// The elements array is allocated to `2^OBJECT_BITS`, where object bits is +/// calculated as the number of leading zeroes in the `__CPROVER_max_alloc_size` +/// constant. +/// +/// \param[inout] set Pointer to the object to initialise +inline void __CPROVER_contracts_obj_set_create_indexed_by_object_id( + __CPROVER_contracts_obj_set_ptr_t set) +{ +__CPROVER_HIDE:; +#ifdef DFCC_SELF_CHECK + __CPROVER_assert( + __CPROVER_rw_ok(set, sizeof(__CPROVER_contracts_obj_set_t)), + "set writable"); +#endif + // compute the maximum number of objects that can exist in the + // symex state from the number of object_bits/offset_bits + // the number of object bits is determined by counting the number of leading + // zeroes of the built-in constant __CPROVER_max_malloc_size; + __CPROVER_size_t object_bits = __builtin_clzll(__CPROVER_max_malloc_size); + __CPROVER_size_t nof_objects = 1UL << object_bits; + set->max_elems = nof_objects; + set->watermark = 0; + set->nof_elems = 0; + set->is_empty = 1; + set->indexed_by_object_id = 1; + set->elems = __CPROVER_allocate(nof_objects * sizeof(*(set->elems)), 1); +} + +/* FUNCTION: __CPROVER_contracts_obj_set_create_append */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +/// \brief Initialises a \ref __CPROVER_contracts_obj_set_t object to use it +/// in "append" mode for at most \p max_elems elements. +/// +/// \param[inout] set Pointer to the object to initialise +/// \param[inout] max_elems Maximum number of objects in the set. +inline void __CPROVER_contracts_obj_set_create_append( + __CPROVER_contracts_obj_set_ptr_t set, + __CPROVER_size_t max_elems) +{ +__CPROVER_HIDE:; +#ifdef DFCC_SELF_CHECK + __CPROVER_assert( + __CPROVER_rw_ok(set, sizeof(__CPROVER_contracts_obj_set_t)), + "set writable"); +#endif + set->max_elems = max_elems; + set->watermark = 0; + set->nof_elems = 0; + set->is_empty = 1; + set->indexed_by_object_id = 0; + set->elems = __CPROVER_allocate(set->max_elems * sizeof(*(set->elems)), 1); +} + +/* FUNCTION: __CPROVER_contracts_obj_set_add */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +/// \brief Adds the \p ptr to \p set. +/// \pre \p set->indexed_by_object_id must be true. +/// \param[inout] set Set to add the pointer to +/// \param[in] ptr The pointer to add +inline void __CPROVER_contracts_obj_set_add( + __CPROVER_contracts_obj_set_ptr_t set, + void *ptr) +{ +__CPROVER_HIDE:; +#ifdef DFCC_SELF_CHECK + __CPROVER_assert(set->indexed_by_object_id, "indexed by object id"); + __CPROVER_assert( + __CPROVER_POINTER_OBJECT(ptr) < set->max_elems, "no OOB access"); +#endif + __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr); + set->nof_elems = + (set->elems[object_id] != 0) ? set->nof_elems : set->nof_elems + 1; + set->elems[object_id] = ptr; + set->is_empty = 0; +} + +/* FUNCTION: __CPROVER_contracts_obj_set_append */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +/// \brief Appends \p ptr to \p set. +/// \pre \p set->indexed_by_object_id must be false. +/// \param[inout] set The set to append to +/// \param[in] ptr The pointer to append +inline void __CPROVER_contracts_obj_set_append( + __CPROVER_contracts_obj_set_ptr_t set, + void *ptr) +{ +__CPROVER_HIDE:; +#ifdef DFCC_SELF_CHECK + __CPROVER_assert(!(set->indexed_by_object_id), "not indexed by object id"); + __CPROVER_assert(set->watermark < set->max_elems, "no OOB access"); +#endif + set->nof_elems = set->watermark; + set->elems[set->watermark] = ptr; + set->watermark += 1; + set->is_empty = 0; +} + +/* FUNCTION: __CPROVER_contracts_obj_set_remove */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +/// \brief Removes \p ptr form \p set if \p ptr exists in \p set, +/// no-op otherwise. +/// \param[inout] set Set to update +/// \param[in] ptr Pointer to remove +inline void __CPROVER_contracts_obj_set_remove( + __CPROVER_contracts_obj_set_ptr_t set, + void *ptr) +{ +__CPROVER_HIDE:; +#ifdef DFCC_SELF_CHECK + __CPROVER_assert(set->indexed_by_object_id, "indexed by object id"); + __CPROVER_assert( + __CPROVER_POINTER_OBJECT(ptr) < set->max_elems, "no OOB access"); +#endif + __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr); + set->nof_elems = set->elems[object_id] ? set->nof_elems - 1 : set->nof_elems; + set->is_empty = set->nof_elems == 0; + set->elems[object_id] = 0; +} + +/* FUNCTION: __CPROVER_contracts_obj_set_contains */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +/// \brief Checks if a pointer with the same object id as \p ptr is contained in +/// \p set. +/// \param[inout] set The set to check membership in +/// \param ptr The pointer to check +/// \return True iff a pointer with the same object id exists in \p set +inline __CPROVER_bool __CPROVER_contracts_obj_set_contains( + __CPROVER_contracts_obj_set_ptr_t set, + void *ptr) +{ +__CPROVER_HIDE:; +#ifdef DFCC_SELF_CHECK + __CPROVER_assert(set->indexed_by_object_id, "indexed by object id"); + __CPROVER_assert( + __CPROVER_POINTER_OBJECT(ptr) < set->max_elems, "no OOB access"); +#endif + return set->elems[__CPROVER_POINTER_OBJECT(ptr)] != 0; +} + +/* FUNCTION: __CPROVER_contracts_obj_set_contains_exact */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +/// \brief Checks if \p ptr is contained in \p set. +/// \param[inout] set The set to check membership in +/// \param ptr The pointer to check +/// \return True iff \p ptr exists in \p set +inline __CPROVER_bool __CPROVER_contracts_obj_set_contains_exact( + __CPROVER_contracts_obj_set_ptr_t set, + void *ptr) +{ +__CPROVER_HIDE:; +#ifdef DFCC_SELF_CHECK + __CPROVER_assert(set->indexed_by_object_id, "indexed by object id"); + __CPROVER_assert( + __CPROVER_POINTER_OBJECT(ptr) < set->max_elems, "no OOB access"); +#endif + return set->elems[__CPROVER_POINTER_OBJECT(ptr)] == ptr; +} + +/* FUNCTION: __CPROVER_contracts_write_set_create */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +inline void __CPROVER_contracts_car_set_create( + __CPROVER_contracts_car_set_ptr_t, + __CPROVER_size_t); + +inline void __CPROVER_contracts_obj_set_create_indexed_by_object_id( + __CPROVER_contracts_obj_set_ptr_t); + +inline void __CPROVER_contracts_obj_set_create_append( + __CPROVER_contracts_obj_set_ptr_t, + __CPROVER_size_t); + +/// \brief Initialises a \ref __CPROVER_contracts_write_set_t object. +/// \param[inout] set Pointer to the object to initialise +/// \param[in] contract_assigns_size Max size of the assigns clause +/// \param[in] contract_frees_size Max size of the frees clause +/// \param[in] replacement True iff this write set is used to replace a contract +/// \param[in] assume_requires_ctx True iff this write set is used to check side +/// effects in a requires clause in contract checking mode +/// \param[in] assert_requires_ctx True iff this write set is used to check side +/// effects in a requires clause in contract replacement mode +/// \param[in] assume_ensures_ctx True iff this write set is used to check for +/// side effects in an ensures clause in contract replacement mode +/// \param[in] assert_ensures_ctx True iff this write set is used to check for +/// side effects in an ensures clause in contract checking mode +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 replacement, + __CPROVER_bool assume_requires_ctx, + __CPROVER_bool assert_requires_ctx, + __CPROVER_bool assume_ensures_ctx, + __CPROVER_bool assert_ensures_ctx) +{ +__CPROVER_HIDE:; +#ifdef DFCC_SELF_CHECK + __CPROVER_assert( + __CPROVER_w_ok(set, sizeof(__CPROVER_contracts_write_set_t)), + "set writable"); +#endif + __CPROVER_contracts_car_set_create( + &(set->contract_assigns), contract_assigns_size); + __CPROVER_contracts_obj_set_create_indexed_by_object_id( + &(set->contract_frees)); + set->replacement = replacement; + if(replacement) + { + __CPROVER_contracts_obj_set_create_append( + &(set->contract_frees_replacement), contract_frees_size); + } + else + { + set->contract_frees_replacement.elems = 0; + } + __CPROVER_contracts_obj_set_create_indexed_by_object_id(&(set->allocated)); + __CPROVER_contracts_obj_set_create_indexed_by_object_id(&(set->deallocated)); + __CPROVER_contracts_obj_set_create_indexed_by_object_id( + &(set->is_freshr_seen)); + set->linked_allocated = 0; + set->assume_requires_ctx = assume_requires_ctx; + set->assert_requires_ctx = assert_requires_ctx; + set->assume_ensures_ctx = assume_ensures_ctx; + set->assert_ensures_ctx = assert_ensures_ctx; +} + +/* FUNCTION: __CPROVER_contracts_write_set_release */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +/// @brief Releases resources used by \p set. +void __CPROVER_contracts_write_set_release( + __CPROVER_contracts_write_set_ptr_t set) +{ +__CPROVER_HIDE:; +#ifdef DFCC_SELF_CHECK + __CPROVER_assert( + __CPROVER_rw_ok(set, sizeof(__CPROVER_contracts_write_set_t)), + "set readable"); + __CPROVER_assert( + __CPROVER_rw_ok(&(set->contract_assigns.elems), 0), + "contract_assigns writable"); + __CPROVER_assert( + __CPROVER_rw_ok(&(set->contract_frees.elems), 0), + "contract_frees writable"); + __CPROVER_assert( + (set->replacement == 0) || + __CPROVER_rw_ok(&(set->contract_frees_replacement.elems), 0), + "contract_frees_replacement writable"); + __CPROVER_assert( + __CPROVER_rw_ok(&(set->allocated.elems), 0), "allocated writable"); + __CPROVER_assert( + __CPROVER_rw_ok(&(set->deallocated.elems), 0), "deallocated writable"); + __CPROVER_assert( + __CPROVER_rw_ok(&(set->deallocated.elems), 0), "is_freshr_seen writable"); +#endif + __CPROVER_deallocate(set->contract_assigns.elems); + __CPROVER_deallocate(set->contract_frees.elems); + if(set->replacement != 0) + { + __CPROVER_deallocate(set->contract_frees_replacement.elems); + } + __CPROVER_deallocate(set->allocated.elems); + __CPROVER_deallocate(set->deallocated.elems); + __CPROVER_deallocate(set->is_freshr_seen.elems); + // do not free set->deallocated_linked->elems + // since it is owned by another write_set instance +} + +/* FUNCTION: __CPROVER_contracts_write_set_insert_assignable */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +inline void __CPROVER_contracts_car_set_insert( + __CPROVER_contracts_car_set_ptr_t set, + __CPROVER_size_t idx, + void *ptr, + __CPROVER_size_t size); + +/// \brief Inserts a snapshot of the range starting at \p ptr of size \p size +/// at index \p idx in \p set->contract_assigns. +/// \param[inout] set The set to update +/// \param[in] idx Insertion index +/// \param[in] ptr Start of the range of bytes +/// \param[in] size Size of the range in bytes +void __CPROVER_contracts_write_set_insert_assignable( + __CPROVER_contracts_write_set_ptr_t set, + __CPROVER_size_t idx, + void *ptr, + __CPROVER_size_t size) +{ +__CPROVER_HIDE:; + __CPROVER_contracts_car_set_insert(&(set->contract_assigns), idx, ptr, size); +} + +/* FUNCTION: __CPROVER_contracts_write_set_insert_whole_object */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +inline void __CPROVER_contracts_car_set_insert( + __CPROVER_contracts_car_set_ptr_t set, + __CPROVER_size_t idx, + void *ptr, + __CPROVER_size_t size); + +/// \brief Inserts a snapshot of the range of bytes covering the whole object +/// pointed to by \p ptr in \p set->contact_assigns at index \p idx. +/// +/// - The start address is `ptr - __CPROVER_POINTER_OFFSET(ptr)` +/// - The size in bytes is `__CPROVER_OBJECT_SIZE(ptr)` +/// +/// at index \p idx in \p set. +/// \param[inout] set The set to update +/// \param[in] idx Insertion index +/// \param[in] ptr Pointer to the object +void __CPROVER_contracts_write_set_insert_whole_object( + __CPROVER_contracts_write_set_ptr_t set, + __CPROVER_size_t idx, + void *ptr) +{ +__CPROVER_HIDE:; + __CPROVER_contracts_car_set_insert( + &(set->contract_assigns), + idx, + ((char *)ptr) - __CPROVER_POINTER_OFFSET(ptr), + __CPROVER_OBJECT_SIZE(ptr)); +} + +/* FUNCTION: __CPROVER_contracts_write_set_insert_object_from */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +inline void __CPROVER_contracts_car_set_insert( + __CPROVER_contracts_car_set_ptr_t set, + __CPROVER_size_t idx, + void *ptr, + __CPROVER_size_t size); + +/// \brief Inserts a snapshot of the range of bytes starting at \p ptr and +/// extending to the end of the object in \p set->contact_assigns at index +/// \p idx. +/// +/// - The start address is `ptr` +/// - The size in bytes is +/// `__CPROVER_OBJECT_SIZE(ptr) - __CPROVER_POINTER_OFFSET(ptr)` +/// +/// \param[inout] set The set to update +/// \param[in] idx Insertion index +/// \param[in] ptr Pointer to the start of the range +void __CPROVER_contracts_write_set_insert_object_from( + __CPROVER_contracts_write_set_ptr_t set, + __CPROVER_size_t idx, + void *ptr) +{ + __CPROVER_contracts_car_set_insert( + &(set->contract_assigns), + idx, + ptr, + __CPROVER_OBJECT_SIZE(ptr) - __CPROVER_POINTER_OFFSET(ptr)); +} + +/* FUNCTION: __CPROVER_contracts_write_set_insert_object_upto */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +inline void __CPROVER_contracts_car_set_insert( + __CPROVER_contracts_car_set_ptr_t set, + __CPROVER_size_t idx, + void *ptr, + __CPROVER_size_t size); + +/// \brief Inserts a snapshot of the range of bytes starting at \p ptr of +/// \p size bytes in \p set->contact_assigns at index \p idx. +/// +/// - The start address is `ptr` +/// - The size in bytes is `size` +/// +/// \param[inout] set The set to update +/// \param[in] idx Insertion index +/// \param[in] ptr Pointer to the start of the range +/// \param[in] size Size of the range in bytes +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) +{ +__CPROVER_HIDE:; + __CPROVER_contracts_car_set_insert(&(set->contract_assigns), idx, ptr, size); +} + +/* FUNCTION: __CPROVER_contracts_write_set_add_freeable */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +void __CPROVER_contracts_obj_set_add( + __CPROVER_contracts_obj_set_ptr_t set, + void *ptr); + +void __CPROVER_contracts_obj_set_append( + __CPROVER_contracts_obj_set_ptr_t set, + void *ptr); + +/// \brief Adds the freeable pointer \p ptr to \p set->contract_frees. +/// \param[inout] set The set to update +/// \param[in] ptr The pointer to add +void __CPROVER_contracts_write_set_add_freeable( + __CPROVER_contracts_write_set_ptr_t set, + void *ptr) +{ +__CPROVER_HIDE:; + // we don't check yet that the pointer satisfies + // the __CPROVER_contracts_is_freeable as precondition. + // preconditions will be checked if there is an actual attempt + // to free the pointer. + + // store pointer + __CPROVER_contracts_obj_set_add(&(set->contract_frees), ptr); + + // append pointer if available + if(set->replacement) + __CPROVER_contracts_obj_set_append(&(set->contract_frees_replacement), ptr); +} + +/* FUNCTION: __CPROVER_contracts_write_set_add_allocated */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +void __CPROVER_contracts_obj_set_add(__CPROVER_contracts_obj_set_ptr_t, void *); + +/// \brief Adds the pointer \p ptr to \p set->allocated. +/// \param[inout] set The set to update +/// \param[in] ptr Pointer to an object declared using a `DECL x` or +/// `x = __CPROVER_allocate(...)` GOTO instruction. +void __CPROVER_contracts_write_set_add_allocated( + __CPROVER_contracts_write_set_ptr_t set, + void *ptr) +{ +__CPROVER_HIDE:; + __CPROVER_contracts_obj_set_add(&(set->allocated), ptr); +} + +/* FUNCTION: __CPROVER_contracts_write_set_record_dead */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +void __CPROVER_contracts_obj_set_remove( + __CPROVER_contracts_obj_set_ptr_t, + void *); + +/// \brief Records that an object is dead by removing the pointer \p ptr from +/// \p set->allocated. +/// +/// \pre \p ptr is the start address `&x` of an object declared as 'DEAD x'. +/// +/// \param[inout] set The set to update +/// \param[in] ptr Pointer to the dead object +void __CPROVER_contracts_write_set_record_dead( + __CPROVER_contracts_write_set_ptr_t set, + void *ptr) +{ +__CPROVER_HIDE:; + __CPROVER_contracts_obj_set_remove(&(set->allocated), ptr); +} + +/* FUNCTION: __CPROVER_contracts_write_set_record_deallocated */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +/// \brief Records that an object is deallocated by adding the pointer \p ptr to +/// \p set->deallocated. +/// +/// \pre \p ptr was deallocated with a call to `__CPROVER_deallocate(ptr)`. +/// +/// \param[inout] set The set to update +/// \param[in] ptr Pointer to the deallocated object +void __CPROVER_contracts_write_set_record_deallocated( + __CPROVER_contracts_write_set_ptr_t set, + void *ptr) +{ +__CPROVER_HIDE:; +#ifdef DFCC_SELF_CHECK + __CPROVER_assert(set->replacement == 0, "!replacement"); +#endif + // we need to record the deallocation to evaluate post conditions + __CPROVER_contracts_obj_set_add(&(set->deallocated), ptr); +} + +/* FUNCTION: __CPROVER_contracts_write_set_check_allocated_deallocated_is_empty */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +/// \brief Returns true iff \p set->deallocated is empty. +/// +/// \param[in] set The set to be checked for emptiness +/// \returns True iff \p set->deallocated is empty +inline __CPROVER_bool +__CPROVER_contracts_write_set_check_allocated_deallocated_is_empty( + __CPROVER_contracts_write_set_ptr_t set) +{ +__CPROVER_HIDE:; + return set->allocated.is_empty & set->deallocated.is_empty; +} + +/* FUNCTION: __CPROVER_contracts_write_set_check_assignment */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +inline __CPROVER_contracts_car_t +__CPROVER_contracts_car_create(void *, __CPROVER_size_t); + +inline __CPROVER_bool __CPROVER_contracts_car_set_contains( + __CPROVER_contracts_car_set_ptr_t, + __CPROVER_contracts_car_t); + +#if 0 +/// \brief Checks if an assignment to the range of bytes starting at \p ptr of +/// size \p size is allowed by \p set. +/// +/// \param[in] set Write set to check the assignment against +/// \param[in] ptr Start address of the assigned range +/// \param[in] size Size of the assigned range in bytes +/// \return True iff the range of bytes starting at \p ptr of size \p size is +/// contained \p set->allocated or in \p set->contract_assigns. +inline __CPROVER_bool __CPROVER_contracts_write_set_check_assignment( + __CPROVER_contracts_write_set_ptr_t set, + void *ptr, + __CPROVER_size_t size) +{ +__CPROVER_HIDE:; +# ifdef DFCC_SELF_CHECK + __CPROVER_assert(set->replacement == 0, "!replacement"); +# endif + __CPROVER_assert( + ((ptr == 0) | __CPROVER_rw_ok(ptr, size)), + "ptr NULL or writable up to size"); + + __CPROVER_assert( + (ptr == 0) | (__CPROVER_POINTER_OBJECT(ptr) < set->allocated.max_elems), + "no OOB access"); + + __CPROVER_contracts_car_t car = __CPROVER_contracts_car_create(ptr, size); + if(!car.is_writable) + return 0; + + if(set->allocated.elems[__CPROVER_POINTER_OBJECT(ptr)] != 0) + return 1; + + return __CPROVER_contracts_car_set_contains(&(set->contract_assigns), car); +} +#else + +/// \brief Checks if an assignment to the range of bytes starting at \p ptr and +/// of \p size bytes is allowed according to \p set. +/// +/// \param[in] set Write set to check the assignment against +/// \param[in] ptr Start address of the assigned range +/// \param[in] size Size of the assigned range in bytes +/// \return True iff the range of bytes starting at \p ptr of \p size bytes is +/// contained in \p set->allocated or \p set->contract_assigns. +inline __CPROVER_bool __CPROVER_contracts_write_set_check_assignment( + __CPROVER_contracts_write_set_ptr_t set, + void *ptr, + __CPROVER_size_t size) +{ +__CPROVER_HIDE:; +# ifdef DFCC_SELF_CHECK + __CPROVER_assert(set->replacement == 0, "!replacement"); +# endif + +# pragma CPROVER check push +# pragma CPROVER check disable "pointer" +# pragma CPROVER check disable "pointer-primitive" +# pragma CPROVER check disable "unsigned-overflow" +# pragma CPROVER check disable "signed-overflow" +# pragma CPROVER check disable "undefined-shift" +# pragma CPROVER check disable "conversion" + + __CPROVER_assert( + (ptr == 0) | (__CPROVER_POINTER_OBJECT(ptr) < set->allocated.max_elems), + "no OOB access"); + + __CPROVER_assert( + ((ptr == 0) | __CPROVER_rw_ok(ptr, size)), + "ptr NULL or writable up to size"); + + // the range is not writable + if(ptr == 0) + return 0; + + // is ptr pointing to a locally allocated object ? + if(set->allocated.elems[__CPROVER_POINTER_OBJECT(ptr)] != 0) + return 1; + + // don't even drive symex into the rest of the function if the set is emtpy + if(set->contract_assigns.max_elems == 0) + return 0; + + // Compute the upper bound, perform inclusion check against contract-assigns + __CPROVER_assert( + size < __CPROVER_max_malloc_size, + "CAR size is less than __CPROVER_max_malloc_size"); + __CPROVER_ssize_t offset = __CPROVER_POINTER_OFFSET(ptr); + __CPROVER_assert( + !(offset > 0) | + ((__CPROVER_size_t)offset + size < __CPROVER_max_malloc_size), + "no offset bits overflow on CAR upper bound computation"); + void *ub = (void *)((char *)ptr + size); + __CPROVER_contracts_car_t *elem = set->contract_assigns.elems; + __CPROVER_size_t idx = set->contract_assigns.max_elems; + __CPROVER_bool incl = 0; + +SET_CHECK_ASSIGNMENT_LOOP: + while(idx != 0) + { + incl |= + elem->is_writable & __CPROVER_same_object(elem->lb, ptr) & + (__CPROVER_POINTER_OFFSET(elem->lb) <= __CPROVER_POINTER_OFFSET(ptr)) & + (__CPROVER_POINTER_OFFSET(ub) <= __CPROVER_POINTER_OFFSET(elem->ub)); + ++elem; + --idx; + } + return incl; +# pragma CPROVER check pop +} +#endif + +/* FUNCTION: __CPROVER_contracts_write_set_check_array_set */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +inline __CPROVER_bool __CPROVER_contracts_write_set_check_assignment( + __CPROVER_contracts_write_set_ptr_t, + void *, + __CPROVER_size_t); + +/// \brief Checks if the operation `array_set(dest, ...)` is allowed according +/// to \p set. +/// +/// \remark The `array_set` operation updates all bytes of the object starting +/// from \p dest. +/// +/// \param[in] set Write set to check the array_set operation against +/// \param[in] dest The destination pointer +/// \return True iff the range of bytes starting at \p dest and of +/// `__CPROVER_OBJECT_SIZE(dest) - __CPROVER_POINTER_OFFSET(dest)` bytes is +/// contained in \p set->allocated or \p set->contract_assigns. +__CPROVER_bool __CPROVER_contracts_write_set_check_array_set( + __CPROVER_contracts_write_set_ptr_t set, + void *dest) +{ +__CPROVER_HIDE:; + return __CPROVER_contracts_write_set_check_assignment( + set, dest, __CPROVER_OBJECT_SIZE(dest) - __CPROVER_POINTER_OFFSET(dest)); +} + +/* FUNCTION: __CPROVER_contracts_write_set_check_array_copy */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +inline __CPROVER_bool __CPROVER_contracts_write_set_check_assignment( + __CPROVER_contracts_write_set_ptr_t, + void *, + __CPROVER_size_t); + +/// \brief Checks if the operation `array_copy(dest, ...)` is allowed according +/// to \p set. +/// +/// \remark The `array_copy` operation updates all of `*dest` (possibly using +/// nondet values), even when `*src` is smaller. +/// +/// \param[in] set Write set to check the `array_copy` operation against +/// \param[in] dest The destination pointer +/// \return True iff the range of bytes starting at \p dest and of +/// `__CPROVER_OBJECT_SIZE(dest) - __CPROVER_POINTER_OFFSET(dest)` bytes is +/// contained in \p set->allocated or \p set->contract_assigns. +__CPROVER_bool __CPROVER_contracts_write_set_check_array_copy( + __CPROVER_contracts_write_set_ptr_t set, + void *dest) +{ +__CPROVER_HIDE:; + return __CPROVER_contracts_write_set_check_assignment( + set, dest, __CPROVER_OBJECT_SIZE(dest) - __CPROVER_POINTER_OFFSET(dest)); +} + +/* FUNCTION: __CPROVER_contracts_write_set_check_array_replace */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +inline __CPROVER_bool __CPROVER_contracts_write_set_check_assignment( + __CPROVER_contracts_write_set_ptr_t, + void *, + __CPROVER_size_t); + +/// \brief Checks if the operation `array_replace(dest, src)` is allowed +/// according to \p set. +/// +/// \remark The `array_replace` operation updates at most `size-of-*src` bytes +/// in \p *dest, i.e. it replaces `MIN(size-of-*dest, size-of-*src)` bytes in +/// \p *dest. +/// +/// \param[in] set Write set to check the `array_replace` operation against +/// \param[in] dest The destination pointer +/// \param[in] src The source pointer +/// \return True iff the range of bytes starting at \p dest and extending for +/// `MIN(__CPROVER_OBJECT_SIZE(dest) - __CPROVER_POINTER_OFFSET(dest), +/// __CPROVER_OBJECT_SIZE(src) - __CPROVER_POINTER_OFFSET(src))` bytes is +/// contained in \p set->allocated or \p set->contract_assigns. +__CPROVER_bool __CPROVER_contracts_write_set_check_array_replace( + __CPROVER_contracts_write_set_ptr_t set, + void *dest, + void *src) +{ +__CPROVER_HIDE:; + __CPROVER_size_t src_size = + __CPROVER_OBJECT_SIZE(src) - __CPROVER_POINTER_OFFSET(src); + __CPROVER_size_t dest_size = + __CPROVER_OBJECT_SIZE(dest) - __CPROVER_POINTER_OFFSET(dest); + __CPROVER_size_t size = dest_size < src_size ? dest_size : src_size; + return __CPROVER_contracts_write_set_check_assignment(set, dest, size); +} + +/* FUNCTION: __CPROVER_contracts_write_set_check_havoc_object */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +inline __CPROVER_bool __CPROVER_contracts_write_set_check_assignment( + __CPROVER_contracts_write_set_ptr_t, + void *, + __CPROVER_size_t); + +/// \brief Checks if a `havoc_object(ptr)` is allowed according to \p set. +/// +/// \param[in] set The write set to check the operation against +/// \param[in] ptr Pointer to the havoced object +/// \return True iff the range of bytes starting at +/// `(char *)ptr - __CPROVER_POINTER_OFFSET(ptr)` and of size +/// `__CPROVER_OBJECT_SIZE(ptr)` is contained in `set->contract_assigns` or +/// `set->allocated`. +__CPROVER_bool __CPROVER_contracts_write_set_check_havoc_object( + __CPROVER_contracts_write_set_ptr_t set, + void *ptr) +{ +__CPROVER_HIDE:; + return __CPROVER_contracts_write_set_check_assignment( + set, + (char *)ptr - __CPROVER_POINTER_OFFSET(ptr), + __CPROVER_OBJECT_SIZE(ptr)); +} + +/* FUNCTION: __CPROVER_contracts_write_set_check_deallocate */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +__CPROVER_bool +__CPROVER_contracts_obj_set_contains(__CPROVER_contracts_obj_set_ptr_t, void *); + +/// \brief Checks if the deallocation of \p ptr is allowed according to \p set. +/// +/// \pre The pointer \p ptr is involved in the GOTO instruction +/// `CALL __CPROVER_deallocate(ptr);` +/// +/// \param[in] set Write set to check the deallocation against +/// \param[in] ptr Deallocated pointer to check set to check the deallocation +/// against +/// \return True iff \p ptr is contained in \p set->contract_frees or +/// \p set->allocated. +__CPROVER_bool __CPROVER_contracts_write_set_check_deallocate( + __CPROVER_contracts_write_set_ptr_t set, + void *ptr) +{ +__CPROVER_HIDE:; +#ifdef DFCC_SELF_CHECK + __CPROVER_assert(set->replacement == 0, "!replacement"); +#endif + // NULL pointers can always be passed to free + if(!ptr) + return 1; + + // is this one of the recorded pointers ? + return __CPROVER_contracts_obj_set_contains_exact( + &(set->contract_frees), ptr) || + __CPROVER_contracts_obj_set_contains_exact(&(set->allocated), ptr); +} + +/* FUNCTION: __CPROVER_contracts_write_set_check_assigns_clause_inclusion */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +/// \brief Checks the inclusion of the \p candidate->contract_assigns elements +/// in \p reference->contract_assigns or \p reference->allocated. +/// +/// \pre \p reference must not be in replacement mode. +/// \pre \p candidate must be in replacement mode and \p candidate->allocated +/// must be empty. +/// +/// \param[in] reference Reference write set from a caller +/// \param[in] candidate Candidate write set from a contract being replaced +/// \return True iff all elements of \p candidate->contract_assigns are included +/// in some element of \p reference->contract_assigns or \p reference->allocated +inline __CPROVER_bool +__CPROVER_contracts_write_set_check_assigns_clause_inclusion( + __CPROVER_contracts_write_set_ptr_t reference, + __CPROVER_contracts_write_set_ptr_t candidate) +{ +__CPROVER_HIDE:; +#ifdef DFCC_SELF_CHECK + __CPROVER_assert( + reference->replacement == 0, "reference set in !replacement"); + __CPROVER_assert(candidate->replacement != 0, "candidate set in replacement"); +#endif + __CPROVER_bool incl = 1; + __CPROVER_contracts_car_t *current = candidate->contract_assigns.elems; + __CPROVER_size_t idx = candidate->contract_assigns.max_elems; +SET_CHECK_ASSIGNS_CLAUSE_INCLUSION_LOOP: + while(idx != 0) + { + if(current->is_writable) + { + incl &= __CPROVER_contracts_write_set_check_assignment( + reference, current->lb, current->size); + } + --idx; + ++current; + } + return incl; +} + +/* FUNCTION: __CPROVER_contracts_write_set_check_frees_clause_inclusion */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +/// \brief Checks the inclusion of the \p candidate->contract_frees elements +/// in \p reference->contract_frees or \p reference->allocated. +/// +/// \pre \p reference must not be in replacement mode. +/// \pre \p candidate must be in replacement mode and \p candidate->allocated +/// must be empty. +/// +/// \param[in] reference Reference write set from a caller +/// \param[in] candidate Candidate write set from a contract being replaced +/// \return True iff all elements of \p candidate->contract_frees are included +/// in some element of \p reference->contract_frees or \p reference->allocated +inline __CPROVER_bool +__CPROVER_contracts_write_set_check_frees_clause_inclusion( + __CPROVER_contracts_write_set_ptr_t reference, + __CPROVER_contracts_write_set_ptr_t candidate) +{ +__CPROVER_HIDE:; +#ifdef DFCC_SELF_CHECK + __CPROVER_assert( + reference->replacement == 0, "reference set in !replacement"); + __CPROVER_assert(candidate->replacement != 0, "candidate set in replacement"); +#endif + __CPROVER_bool all_incl = 1; + void **current = candidate->contract_frees_replacement.elems; + __CPROVER_size_t idx = candidate->contract_frees_replacement.max_elems; +SET_CHECK_FREES_CLAUSE_INCLUSION_LOOP: + while(idx != 0) + { + void *ptr = *current; + all_incl &= + __CPROVER_contracts_obj_set_contains(&(reference->contract_frees), ptr) || + __CPROVER_contracts_obj_set_contains(&(reference->allocated), ptr); + --idx; + ++current; + } + + return all_incl; +} + +/* FUNCTION: __CPROVER_contracts_write_set_deallocate_freeable */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +__CPROVER_bool nondet_CPROVER_bool(); + +/// \brief Models the instrumented version of the free function. +/// +/// \remark Uses of this function will be remapped to the instrumented version +/// of the `free` found in the goto model. +__CPROVER_bool +__CPROVER_contracts_free(void *, __CPROVER_contracts_write_set_ptr_t); + +void __CPROVER_contracts_write_set_record_deallocated( + __CPROVER_contracts_write_set_ptr_t, + void *); + +/// \brief Non-deterministically call \ref __CPROVER_contracts_free on all +/// elements of \p set->contract_frees, and records the freed pointers in +/// \p target->deallocated. +/// +/// \param[in] set Write set to free +/// \param[out] target Write set to record deallocations in +void __CPROVER_contracts_write_set_deallocate_freeable( + __CPROVER_contracts_write_set_ptr_t set, + __CPROVER_contracts_write_set_ptr_t target) +{ +__CPROVER_HIDE:; +#ifdef DFCC_SELF_CHECK + __CPROVER_assert(set->replacement == 1, "set is in replacement"); + __CPROVER_assert( + (target == 0) | (target->replacement == 0), "target is in !replacement"); +#endif + void **current = set->contract_frees_replacement.elems; + __CPROVER_size_t idx = set->contract_frees_replacement.max_elems; +SET_DEALLOCATE_FREEABLE_LOOP: + while(idx != 0) + { + void *ptr = *current; + + // call free only iff the pointer is valid preconditions are met +#pragma CPROVER check push +#pragma CPROVER check disable "pointer" +#pragma CPROVER check disable "pointer-primitive" +#pragma CPROVER check disable "unsigned-overflow" +#pragma CPROVER check disable "signed-overflow" +#pragma CPROVER check disable "undefined-shift" +#pragma CPROVER check disable "conversion" + // avoid pointer-primitive checks on r_ok, dynobject and offset + __CPROVER_bool preconditions = + (ptr == 0) | (__CPROVER_r_ok(ptr, 0) & __CPROVER_DYNAMIC_OBJECT(ptr) & + (__CPROVER_POINTER_OFFSET(ptr) == 0)); +#pragma CPROVER check pop + // TODO make sure not to deallocate the same pointer twice + if((ptr != 0) & preconditions & nondet_CPROVER_bool()) + { + __CPROVER_contracts_free(ptr, 0); + __CPROVER_contracts_write_set_record_deallocated(set, ptr); + // also record effects in the caller write set + if(target != 0) + __CPROVER_contracts_write_set_record_deallocated(target, ptr); + } + --idx; + ++current; + } +} + +/* FUNCTION: __CPROVER_contracts_link_is_freshr_allocated */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +/// \brief Links \p write_set_to_link->allocated to +/// \p write_set_postconditions->linked_allocated so that allocations performed +/// by \ref __CPROVER_contracts_is_freshr when evaluating ensures clauses are +/// recorded in \p write_set_to_link. +void __CPROVER_contracts_link_is_freshr_allocated( + __CPROVER_contracts_write_set_ptr_t write_set_postconditions, + __CPROVER_contracts_write_set_ptr_t write_set_to_link) +{ +__CPROVER_HIDE:; +#ifdef DFCC_SELF_CHECK + __CPROVER_assert( + write_set_postconditions != 0, "write_set_postconditions not NULL"); +#endif + if((write_set_to_link != 0)) + { + write_set_postconditions->linked_allocated = + &(write_set_to_link->allocated); + } + else + { + write_set_postconditions->linked_allocated = 0; + } +} + +/* FUNCTION: __CPROVER_contracts_link_deallocated */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +/// \brief Links \p write_set_to_link->deallocated to +/// \p write_set_postconditions->linked_deallocated so that deallocations +/// performed by the function get recorded in \p write_set_to_link->deallocated +/// and are later available to \ref __CPROVER_contracts_is_freed predicate +/// when evaluating ensures clauses. +void __CPROVER_contracts_link_deallocated( + __CPROVER_contracts_write_set_ptr_t write_set_postconditions, + __CPROVER_contracts_write_set_ptr_t write_set_to_link) +{ +__CPROVER_HIDE:; +#ifdef DFCC_SELF_CHECK + __CPROVER_assert( + write_set_postconditions != 0, "write_set_postconditions not NULL"); +#endif + if((write_set_to_link != 0)) + { + write_set_postconditions->linked_deallocated = + &(write_set_to_link->deallocated); + } + else + { + write_set_postconditions->linked_deallocated = 0; + } +} + +/* FUNCTION: __CPROVER_contracts_is_freshr */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +/// \brief Models the instrumented interface of the `malloc` function +/// \remark Calls to this function will be remapped to the actual instrumented +/// version of malloc found in the goto model. +void *__CPROVER_contracts_malloc( + __CPROVER_size_t, + __CPROVER_contracts_write_set_ptr_t); + +void __CPROVER_contracts_obj_set_add(__CPROVER_contracts_obj_set_ptr_t, void *); + +__CPROVER_bool +__CPROVER_contracts_obj_set_contains(__CPROVER_contracts_obj_set_ptr_t, void *); + +/// \brief Implementation of the `is_fresh`/`is_freshr` front-end predicates. +/// +/// The behaviour depends on the boolean flags carried by \p set +/// which reflect the invocation context: checking vs. replacing a contract, +/// in a requires or an ensures clause context. +/// \param elem First argument of the `is_freshr`/`is_fresh` predicate +/// \param size Second argument of the `is_freshr`/`is_fresh` predicate +/// \param set Write set to record seen and allocated objects in; +/// +/// \details The behaviour is as follows: +/// - When \p set->assume_requires_ctx is `true`, the predicate allocates a new +/// object, records the object in \p set->is_freshr_seen, updates \p *elem to +/// point to the fresh object and returns `true`; +/// - When \p set->assume_ensures_ctx is `true`, the predicate allocates a new +/// object, records the object in \p set->linked_allocated, updates \p *elem +/// to point to the fresh object and returns `true`; +/// - When \p set->assert_requires_ctx or \p set->assert_ensures_ctx is `true`, +/// the predicate computes if \p *elem is readable to the desired \p size and is +/// is not found in \p set->is_freshr_seen, records the object in +/// \p set->is_freshr_seen and returns the computed condition. +__CPROVER_bool __CPROVER_contracts_is_freshr( + void **elem, + __CPROVER_size_t size, + __CPROVER_contracts_write_set_ptr_t set) +{ +__CPROVER_HIDE:; +#ifdef DFCC_SELF_CHECK + __CPROVER_assert( + __CPROVER_rw_ok(set, sizeof(__CPROVER_contracts_write_set_t)), + "set readable"); +#endif +#pragma CPROVER check push +#pragma CPROVER check disable "pointer" +#pragma CPROVER check disable "pointer-primitive" +#pragma CPROVER check disable "pointer-overflow" +#pragma CPROVER check disable "signed-overflow" +#pragma CPROVER check disable "unsigned-overflow" +#pragma CPROVER check disable "conversion" + if(set->assume_requires_ctx) + { + __CPROVER_assert( + (set->assert_requires_ctx == 0) & (set->assume_ensures_ctx == 0) & + (set->assert_ensures_ctx == 0), + "only one context flag at a time"); + // pass a null pointer to malloc si that the object does not get tracked + // as assignable in the requires clause scope + void *ptr = __CPROVER_contracts_malloc(size, 0); + *elem = ptr; + if(!ptr) + return 0; + // record fresh object in the map + __CPROVER_contracts_obj_set_add(&(set->is_freshr_seen), ptr); + return 1; + } + else if(set->assume_ensures_ctx) + { + __CPROVER_assert( + (set->assume_requires_ctx == 0) & (set->assert_requires_ctx == 0) & + (set->assert_ensures_ctx == 0), + "only one context flag at a time"); + void *ptr = __CPROVER_contracts_malloc(size, 0); + // record new object in linked allocated set + __CPROVER_contracts_obj_set_add(set->linked_allocated, ptr); + *elem = ptr; + return (ptr != 0); + } + else if(set->assert_requires_ctx | set->assert_ensures_ctx) + { + __CPROVER_assert( + (set->assume_requires_ctx == 0) & (set->assume_ensures_ctx == 0), + "only one context flag at a time"); + // check separation + __CPROVER_contracts_obj_set_ptr_t seen = &(set->is_freshr_seen); + __CPROVER_bool not_contains = + !__CPROVER_contracts_obj_set_contains(seen, *elem); + __CPROVER_bool r_ok = __CPROVER_r_ok(*elem, size); + __CPROVER_bool ok = not_contains & r_ok; + // record object + __CPROVER_contracts_obj_set_add(seen, *elem); + return ok; + } + else + { + __CPROVER_assert( + 0, "__CPROVER_is_freshr is only called in requires or ensures clauses"); + __CPROVER_assume(0); + return 0; // just to silence libcheck + } +#pragma CPROVER check pop +} + +/* FUNCTION: __CPROVER_contracts_write_set_havoc_get_assignable_target */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +/// \brief Returns the start address of the conditional address range found at +/// index \p idx in \p set->contract_assigns. +void *__CPROVER_contracts_write_set_havoc_get_assignable_target( + __CPROVER_contracts_write_set_ptr_t set, + __CPROVER_size_t idx) +{ +__CPROVER_HIDE:; +#ifdef DFCC_SELF_CHECK + __CPROVER_assert(idx < set->contract_assigns.max_elems, "no OOB access"); +#endif + __CPROVER_contracts_car_t car = set->contract_assigns.elems[idx]; + if(car.is_writable) + return car.lb; + else + return (void *)0; +} + +/* FUNCTION: __CPROVER_contracts_write_set_havoc_whole_object */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +/// \brief Havocs the whole object pointed to by the lower bound pointer of the +/// element stored at index \p idx in \p set->contract_assigns, if it is +/// writable. +void __CPROVER_contracts_write_set_havoc_whole_object( + __CPROVER_contracts_write_set_ptr_t set, + __CPROVER_size_t idx) +{ +__CPROVER_HIDE:; +#ifdef DFCC_SELF_CHECK + __CPROVER_assert(idx < set->contract_assigns.max_elems, "no OOB access"); +#endif + __CPROVER_contracts_car_t car = set->contract_assigns.elems[idx]; + if(car.is_writable) + __CPROVER_havoc_object(car.lb); +} + +/* FUNCTION: __CPROVER_contracts_write_set_havoc_slice */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +char __VERIFIER_nondet_char(); + +/// \brief Havocs the range of bytes represented byt the element stored at index +/// \p idx in \p set->contract_assigns, if it is writable. +void __CPROVER_contracts_write_set_havoc_slice( + __CPROVER_contracts_write_set_ptr_t set, + __CPROVER_size_t idx) +{ +__CPROVER_HIDE:; +#ifdef DFCC_SELF_CHECK + __CPROVER_assert(idx < set->contract_assigns.max_elems, "no OOB access"); +#endif + __CPROVER_contracts_car_t car = set->contract_assigns.elems[idx]; + if(car.is_writable) + { + // TODO use __CPROVER_havoc_slice(car.lb, car.size); + // when array_replace gets fixed + char *target = car.lb; + __CPROVER_size_t i = car.size; + while(i != 0) + { + *(target) = __VERIFIER_nondet_char(); + target++; + i--; + } + } +} + +/* FUNCTION: __CPROVER_contracts_is_freeable */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +extern void *__CPROVER_alloca_object; +extern const void *__CPROVER_deallocated; +extern const void *__CPROVER_new_object; +extern __CPROVER_bool __CPROVER_malloc_is_new_array; + +/// \brief Implementation of the `is_freeable` front-end predicate. +/// \return True iff a pointer satisfies the preconditions for the `free` +/// function and can hence be safely deallocated using `free`. +/// +/// \details If called in an assumption context, +/// only basic conditions are checked: the pointer has offset 0 and points to a +/// dynamic object. If called in an assertion context, extra conditions +/// depending on nondeterministic CPROVER instrumentation variables are checked, +/// yielding the full set of conditions checked by the CPROVER library +/// implementation of free. +__CPROVER_bool __CPROVER_contracts_is_freeable( + void *ptr, + __CPROVER_contracts_write_set_ptr_t set) +{ +__CPROVER_HIDE:; + __CPROVER_assert( + (set != 0) & + ((set->assume_requires_ctx == 1) | (set->assert_requires_ctx == 1) | + (set->assume_ensures_ctx == 1) | (set->assert_ensures_ctx == 1)), + "__CPROVER_is_freeable is used only in requires or ensures clauses"); + + // These are all the preconditions checked by `free` of the CPROVER library + __CPROVER_bool is_dynamic_object = (ptr == 0) | __CPROVER_DYNAMIC_OBJECT(ptr); + __CPROVER_bool has_offset_zero = + (ptr == 0) | (__CPROVER_POINTER_OFFSET(ptr) == 0); + + if((set->assume_requires_ctx == 1) || (set->assume_ensures_ctx == 1)) + return is_dynamic_object & has_offset_zero; + + // these conditions cannot be used in assumptions since they involve + // demonic non-determinism + __CPROVER_bool is_null_or_valid_pointer = (ptr == 0) | __CPROVER_r_ok(ptr, 0); + __CPROVER_bool is_not_deallocated = + (ptr == 0) | (__CPROVER_deallocated != ptr); + __CPROVER_bool is_not_alloca = (ptr == 0) | (__CPROVER_alloca_object != ptr); + __CPROVER_bool is_not_array = (ptr == 0) | (__CPROVER_new_object != ptr) | + (!__CPROVER_malloc_is_new_array); + return is_null_or_valid_pointer & is_dynamic_object & has_offset_zero & + is_not_deallocated & is_not_alloca & is_not_array; +} + +/* FUNCTION: __CPROVER_contracts_is_freed */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +__CPROVER_bool +__CPROVER_contracts_obj_set_contains(__CPROVER_contracts_obj_set_ptr_t, void *); + +/// \brief Returns true iff the pointer \p ptr is found in \p set->deallocated. +__CPROVER_bool +__CPROVER_contracts_is_freed(void *ptr, __CPROVER_contracts_write_set_ptr_t set) +{ +__CPROVER_HIDE:; + __CPROVER_assert( + (set != 0) & + ((set->assume_ensures_ctx == 1) | (set->assert_ensures_ctx == 1)), + "__CPROVER_is_freed is used only in ensures clauses"); + __CPROVER_assert( + (set->linked_deallocated != 0), "linked_deallocated is not null"); + return __CPROVER_contracts_obj_set_contains(set->linked_deallocated, ptr); +} + +/* FUNCTION: __CPROVER_contracts_check_replace_ensures_is_freed_preconditions */ + +#ifndef __CPROVER_contracts_write_set_t_defined +# define __CPROVER_contracts_write_set_t_defined + +typedef struct __CPROVER_contracts_car_t +{ + __CPROVER_bool is_writable; + __CPROVER_size_t size; + void *lb; + void *ub; +} __CPROVER_contracts_car_t; + +typedef struct __CPROVER_contracts_car_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_contracts_car_t *elems; +} __CPROVER_contracts_car_set_t; + +typedef __CPROVER_contracts_car_set_t *__CPROVER_contracts_car_set_ptr_t; + +typedef struct __CPROVER_contracts_obj_set_t +{ + __CPROVER_size_t max_elems; + __CPROVER_size_t watermark; + __CPROVER_size_t nof_elems; + __CPROVER_bool is_empty; + __CPROVER_bool indexed_by_object_id; + void **elems; +} __CPROVER_contracts_obj_set_t; + +typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; + +typedef struct __CPROVER_contracts_write_set_t +{ + __CPROVER_contracts_car_set_t contract_assigns; + __CPROVER_contracts_obj_set_t contract_frees; + __CPROVER_contracts_obj_set_t contract_frees_replacement; + __CPROVER_contracts_obj_set_t allocated; + __CPROVER_contracts_obj_set_t deallocated; + __CPROVER_contracts_obj_set_t is_freshr_seen; + __CPROVER_contracts_obj_set_ptr_t linked_allocated; + __CPROVER_contracts_obj_set_ptr_t linked_deallocated; + __CPROVER_bool replacement; + __CPROVER_bool assume_requires_ctx; + __CPROVER_bool assert_requires_ctx; + __CPROVER_bool assume_ensures_ctx; + __CPROVER_bool assert_ensures_ctx; +} __CPROVER_contracts_write_set_t; + +typedef __CPROVER_contracts_write_set_t *__CPROVER_contracts_write_set_ptr_t; +#endif + +__CPROVER_bool +__CPROVER_contracts_obj_set_contains(__CPROVER_contracts_obj_set_ptr_t, void *); + +/// \brief Asserts that \p ptr is found in \p set->contract_frees. +/// +/// \details If proved, the assertion demonstrates that it is possible to assume +/// that `is_freed(ptr)` holds as a post condition without causing a +/// contradiction when assuming that the ensures clause of a contract holds. +void __CPROVER_contracts_check_replace_ensures_is_freed_preconditions( + void *ptr, + __CPROVER_contracts_write_set_ptr_t set) +{ +__CPROVER_HIDE:; + __CPROVER_assert( + set && ((set->assume_ensures_ctx == 1) | (set->assert_ensures_ctx == 1)), + "__CPROVER_is_freed is used only in ensures clauses"); + + if(set->assume_ensures_ctx) + { + __CPROVER_assert( + __CPROVER_contracts_obj_set_contains(&(set->contract_frees), ptr), + "assuming __CPROVER_is_freed(ptr) requires ptr to always exist in the " + "contract's frees clause"); + } +} diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index b8f187e3050..63090755cbc 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -209,6 +209,7 @@ extern char *yyansi_ctext; %token TOK_CPROVER_ENSURES_CONTRACT "__CPROVER_ensures_contract" %token TOK_CPROVER_ENSURES "__CPROVER_ensures" %token TOK_CPROVER_ASSIGNS "__CPROVER_assigns" +%token TOK_CPROVER_FREES "__CPROVER_frees" %token TOK_IMPLIES "==>" %token TOK_EQUIVALENT "<==>" %token TOK_XORXOR "^^" @@ -2449,26 +2450,31 @@ declaration_or_expression_statement: iteration_statement: TOK_WHILE '(' comma_expression_opt ')' cprover_contract_assigns_opt - cprover_contract_loop_invariant_list_opt + cprover_contract_frees_opt + cprover_contract_loop_invariant_list_opt cprover_contract_decreases_opt statement { $$=$1; statement($$, ID_while); - parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($8))); + parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($9))); if(!parser_stack($5).operands().empty()) static_cast(parser_stack($$).add(ID_C_spec_assigns)).operands().swap(parser_stack($5).operands()); if(!parser_stack($6).operands().empty()) - static_cast(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($6).operands()); + static_cast(parser_stack($$).add(ID_C_spec_frees)).operands().swap(parser_stack($6).operands()); if(!parser_stack($7).operands().empty()) - static_cast(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($7).operands()); + static_cast(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($7).operands()); + + if(!parser_stack($8).operands().empty()) + static_cast(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($8).operands()); } | TOK_DO statement TOK_WHILE '(' comma_expression ')' cprover_contract_assigns_opt - cprover_contract_loop_invariant_list_opt + cprover_contract_frees_opt + cprover_contract_loop_invariant_list_opt cprover_contract_decreases_opt ';' { $$=$1; @@ -2479,10 +2485,13 @@ iteration_statement: static_cast(parser_stack($$).add(ID_C_spec_assigns)).operands().swap(parser_stack($7).operands()); if(!parser_stack($8).operands().empty()) - static_cast(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($8).operands()); + static_cast(parser_stack($$).add(ID_C_spec_frees)).operands().swap(parser_stack($8).operands()); if(!parser_stack($9).operands().empty()) - static_cast(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($9).operands()); + static_cast(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($9).operands()); + + if(!parser_stack($10).operands().empty()) + static_cast(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($10).operands()); } | TOK_FOR { @@ -2497,7 +2506,8 @@ iteration_statement: comma_expression_opt ';' comma_expression_opt ')' cprover_contract_assigns_opt - cprover_contract_loop_invariant_list_opt + cprover_contract_frees_opt + cprover_contract_loop_invariant_list_opt cprover_contract_decreases_opt statement { @@ -2507,16 +2517,19 @@ iteration_statement: mto($$, $4); mto($$, $5); mto($$, $7); - mto($$, $12); + mto($$, $13); if(!parser_stack($9).operands().empty()) static_cast(parser_stack($$).add(ID_C_spec_assigns)).operands().swap(parser_stack($9).operands()); if(!parser_stack($10).operands().empty()) - static_cast(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($10).operands()); + static_cast(parser_stack($$).add(ID_C_spec_frees)).operands().swap(parser_stack($10).operands()); if(!parser_stack($11).operands().empty()) - static_cast(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($11).operands()); + static_cast(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($11).operands()); + + if(!parser_stack($12).operands().empty()) + static_cast(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($12).operands()); if(PARSER.for_has_scope) PARSER.pop_scope(); // remove the C99 for-scope @@ -3319,6 +3332,7 @@ cprover_function_contract: parser_stack($$).add_to_operands(std::move(tmp)); } | cprover_contract_assigns + | cprover_contract_frees ; unary_expression_list: @@ -3372,7 +3386,7 @@ conditional_target_list_opt_semicol: } | conditional_target_list { - $$ = $1; + $$ = $1; } cprover_contract_assigns: @@ -3396,6 +3410,27 @@ cprover_contract_assigns_opt: | cprover_contract_assigns ; +cprover_contract_frees: + TOK_CPROVER_FREES '(' conditional_target_list_opt_semicol ')' + { + $$=$1; + set($$, ID_C_spec_frees); + mto($$, $3); + } + | TOK_CPROVER_FREES '(' ')' + { + $$=$1; + set($$, ID_C_spec_frees); + parser_stack($$).add_to_operands(exprt(ID_target_list)); + } + ; + +cprover_contract_frees_opt: + /* nothing */ + { init($$); parser_stack($$).make_nil(); } + | cprover_contract_frees + ; + cprover_function_contract_sequence: cprover_function_contract | cprover_function_contract_sequence cprover_function_contract diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index 210e6866dac..05faae82d62 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -1292,6 +1292,7 @@ __decltype { if(PARSER.cpp98 && {CPROVER_PREFIX}"requires" { loc(); return TOK_CPROVER_REQUIRES; } {CPROVER_PREFIX}"ensures" { loc(); return TOK_CPROVER_ENSURES; } {CPROVER_PREFIX}"assigns" { loc(); return TOK_CPROVER_ASSIGNS; } +{CPROVER_PREFIX}"frees" { loc(); return TOK_CPROVER_FREES; } {CPROVER_PREFIX}"requires_contract" { loc(); return TOK_CPROVER_REQUIRES_CONTRACT; } {CPROVER_PREFIX}"ensures_contract" { loc(); return TOK_CPROVER_ENSURES_CONTRACT; } diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 1e73214a8b2..c56191418ad 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -17,6 +17,17 @@ SRC = accelerate/accelerate.cpp \ branch.cpp \ call_sequences.cpp \ contracts/contracts.cpp \ + contracts/dynamic-frames/dfcc_utils.cpp \ + contracts/dynamic-frames/dfcc_library.cpp \ + contracts/dynamic-frames/dfcc_is_fresh.cpp \ + contracts/dynamic-frames/dfcc_is_freeable.cpp \ + contracts/dynamic-frames/dfcc_instrument.cpp \ + contracts/dynamic-frames/dfcc_spec_functions.cpp \ + contracts/dynamic-frames/dfcc_dsl_contract_functions.cpp \ + contracts/dynamic-frames/dfcc_dsl_wrapper_program.cpp \ + contracts/dynamic-frames/dfcc_dsl_contract_handler.cpp \ + contracts/dynamic-frames/dfcc_swap_and_wrap.cpp \ + contracts/dynamic-frames/dfcc.cpp \ contracts/havoc_assigns_clause_targets.cpp \ contracts/instrument_spec_assigns.cpp \ contracts/memory_predicates.cpp \ diff --git a/src/goto-instrument/contracts/cfg_info.h b/src/goto-instrument/contracts/cfg_info.h index 1ed166c3f4a..a3cc8b44dbd 100644 --- a/src/goto-instrument/contracts/cfg_info.h +++ b/src/goto-instrument/contracts/cfg_info.h @@ -188,4 +188,49 @@ class loop_cfg_infot : public cfg_infot const dirtyt is_dirty; std::unordered_set locals; }; + +/// For a goto program. locals and dirty locals are inferred directly from +/// the instruction sequence. +class goto_program_cfg_infot : public cfg_infot +{ +public: + explicit goto_program_cfg_infot(const goto_programt &goto_program) + { + // collect symbols declared in the insruction sequence as locals + for(const auto &instruction : goto_program.instructions) + { + if(instruction.is_decl()) + locals.insert(instruction.decl_symbol().get_identifier()); + } + + // collect dirty locals + goto_functiont goto_function; + goto_function.body.copy_from(goto_program); + + dirtyt is_dirty(goto_function); + auto dirty_ids = is_dirty.get_dirty_ids(); + dirty.insert(dirty_ids.begin(), dirty_ids.end()); + } + + /// Returns true iff `ident` is a loop local. + bool is_local(const irep_idt &ident) const override + { + return locals.find(ident) != locals.end(); + } + + /// Returns true iff the given `ident` is either not a loop local + /// or is a loop local that is dirty. + bool is_not_local_or_dirty_local(const irep_idt &ident) const override + { + if(is_local(ident)) + return dirty.find(ident) != dirty.end(); + else + return true; + } + +protected: + std::unordered_set locals; + std::unordered_set dirty; +}; + #endif diff --git a/src/goto-instrument/contracts/doc/Doxyfile b/src/goto-instrument/contracts/doc/Doxyfile new file mode 100644 index 00000000000..02b78eadb6a --- /dev/null +++ b/src/goto-instrument/contracts/doc/Doxyfile @@ -0,0 +1,2683 @@ +# Doxyfile 1.9.5 + +# This file describes the settings to be used by the documentation system +# doxygen (www.doxygen.org) for a project. +# +# All text after a double hash (##) is considered a comment and is placed in +# front of the TAG it is preceding. +# +# All text after a single hash (#) is considered a comment and will be ignored. +# The format is: +# TAG = value [value, ...] +# For lists, items can also be appended using: +# TAG += value [value, ...] +# Values that contain spaces should be placed between quotes (\" \"). +# +# Note: +# +# Use doxygen to compare the used configuration file with the template +# configuration file: +# doxygen -x [configFile] +# Use doxygen to compare the used configuration file with the template +# configuration file without replacing the environment variables or CMake type +# replacement variables: +# doxygen -x_noenv [configFile] + +#--------------------------------------------------------------------------- +# Project related configuration options +#--------------------------------------------------------------------------- + +# This tag specifies the encoding used for all characters in the configuration +# file that follow. The default is UTF-8 which is also the encoding used for all +# text before the first occurrence of this tag. Doxygen uses libiconv (or the +# iconv built into libc) for the transcoding. See +# https://www.gnu.org/software/libiconv/ for the list of possible encodings. +# The default value is: UTF-8. + +DOXYFILE_ENCODING = UTF-8 + +# The PROJECT_NAME tag is a single word (or a sequence of words surrounded by +# double-quotes, unless you are using Doxywizard) that should identify the +# project for which the documentation is generated. This name is used in the +# title of most generated pages and in a few other places. +# The default value is: My Project. + +PROJECT_NAME = "contracts" + +# The PROJECT_NUMBER tag can be used to enter a project or revision number. This +# could be handy for archiving the generated documentation or if some version +# control system is used. + +PROJECT_NUMBER = + +# Using the PROJECT_BRIEF tag one can provide an optional one line description +# for a project that appears at the top of each page and should give viewer a +# quick idea about the purpose of the project. Keep the description short. + +PROJECT_BRIEF = + +# With the PROJECT_LOGO tag one can specify a logo or an icon that is included +# in the documentation. The maximum height of the logo should not exceed 55 +# pixels and the maximum width should not exceed 200 pixels. Doxygen will copy +# the logo to the output directory. + +PROJECT_LOGO = + +# The OUTPUT_DIRECTORY tag is used to specify the (relative or absolute) path +# into which the generated documentation will be written. If a relative path is +# entered, it will be relative to the location where doxygen was started. If +# left blank the current directory will be used. + +OUTPUT_DIRECTORY = . + +# If the CREATE_SUBDIRS tag is set to YES then doxygen will create up to 4096 +# sub-directories (in 2 levels) under the output directory of each output format +# and will distribute the generated files over these directories. Enabling this +# option can be useful when feeding doxygen a huge amount of source files, where +# putting all generated files in the same directory would otherwise causes +# performance problems for the file system. Adapt CREATE_SUBDIRS_LEVEL to +# control the number of sub-directories. +# The default value is: NO. + +CREATE_SUBDIRS = NO + +# Controls the number of sub-directories that will be created when +# CREATE_SUBDIRS tag is set to YES. Level 0 represents 16 directories, and every +# level increment doubles the number of directories, resulting in 4096 +# directories at level 8 which is the default and also the maximum value. The +# sub-directories are organized in 2 levels, the first level always has a fixed +# numer of 16 directories. +# Minimum value: 0, maximum value: 8, default value: 8. +# This tag requires that the tag CREATE_SUBDIRS is set to YES. + +CREATE_SUBDIRS_LEVEL = 8 + +# If the ALLOW_UNICODE_NAMES tag is set to YES, doxygen will allow non-ASCII +# characters to appear in the names of generated files. If set to NO, non-ASCII +# characters will be escaped, for example _xE3_x81_x84 will be used for Unicode +# U+3044. +# The default value is: NO. + +ALLOW_UNICODE_NAMES = NO + +# The OUTPUT_LANGUAGE tag is used to specify the language in which all +# documentation generated by doxygen is written. Doxygen will use this +# information to generate all constant output in the proper language. +# Possible values are: Afrikaans, Arabic, Armenian, Brazilian, Bulgarian, +# Catalan, Chinese, Chinese-Traditional, Croatian, Czech, Danish, Dutch, English +# (United States), Esperanto, Farsi (Persian), Finnish, French, German, Greek, +# Hindi, Hungarian, Indonesian, Italian, Japanese, Japanese-en (Japanese with +# English messages), Korean, Korean-en (Korean with English messages), Latvian, +# Lithuanian, Macedonian, Norwegian, Persian (Farsi), Polish, Portuguese, +# Romanian, Russian, Serbian, Serbian-Cyrillic, Slovak, Slovene, Spanish, +# Swedish, Turkish, Ukrainian and Vietnamese. +# The default value is: English. + +OUTPUT_LANGUAGE = English + +# If the BRIEF_MEMBER_DESC tag is set to YES, doxygen will include brief member +# descriptions after the members that are listed in the file and class +# documentation (similar to Javadoc). Set to NO to disable this. +# The default value is: YES. + +BRIEF_MEMBER_DESC = YES + +# If the REPEAT_BRIEF tag is set to YES, doxygen will prepend the brief +# description of a member or function before the detailed description +# +# Note: If both HIDE_UNDOC_MEMBERS and BRIEF_MEMBER_DESC are set to NO, the +# brief descriptions will be completely suppressed. +# The default value is: YES. + +REPEAT_BRIEF = YES + +# This tag implements a quasi-intelligent brief description abbreviator that is +# used to form the text in various listings. Each string in this list, if found +# as the leading text of the brief description, will be stripped from the text +# and the result, after processing the whole list, is used as the annotated +# text. Otherwise, the brief description is used as-is. If left blank, the +# following values are used ($name is automatically replaced with the name of +# the entity):The $name class, The $name widget, The $name file, is, provides, +# specifies, contains, represents, a, an and the. + +ABBREVIATE_BRIEF = "The $name class" \ + "The $name widget" \ + "The $name file" \ + is \ + provides \ + specifies \ + contains \ + represents \ + a \ + an \ + the + +# If the ALWAYS_DETAILED_SEC and REPEAT_BRIEF tags are both set to YES then +# doxygen will generate a detailed section even if there is only a brief +# description. +# The default value is: NO. + +ALWAYS_DETAILED_SEC = NO + +# If the INLINE_INHERITED_MEMB tag is set to YES, doxygen will show all +# inherited members of a class in the documentation of that class as if those +# members were ordinary class members. Constructors, destructors and assignment +# operators of the base classes will not be shown. +# The default value is: NO. + +INLINE_INHERITED_MEMB = NO + +# If the FULL_PATH_NAMES tag is set to YES, doxygen will prepend the full path +# before files name in the file list and in the header files. If set to NO the +# shortest path that makes the file name unique will be used +# The default value is: YES. + +FULL_PATH_NAMES = YES + +# The STRIP_FROM_PATH tag can be used to strip a user-defined part of the path. +# Stripping is only done if one of the specified strings matches the left-hand +# part of the path. The tag can be used to show relative paths in the file list. +# If left blank the directory from which doxygen is run is used as the path to +# strip. +# +# Note that you can specify absolute paths here, but also relative paths, which +# will be relative from the directory where doxygen is started. +# This tag requires that the tag FULL_PATH_NAMES is set to YES. + +STRIP_FROM_PATH = + +# The STRIP_FROM_INC_PATH tag can be used to strip a user-defined part of the +# path mentioned in the documentation of a class, which tells the reader which +# header file to include in order to use a class. If left blank only the name of +# the header file containing the class definition is used. Otherwise one should +# specify the list of include paths that are normally passed to the compiler +# using the -I flag. + +STRIP_FROM_INC_PATH = + +# If the SHORT_NAMES tag is set to YES, doxygen will generate much shorter (but +# less readable) file names. This can be useful is your file systems doesn't +# support long names like on DOS, Mac, or CD-ROM. +# The default value is: NO. + +SHORT_NAMES = NO + +# If the JAVADOC_AUTOBRIEF tag is set to YES then doxygen will interpret the +# first line (until the first dot) of a Javadoc-style comment as the brief +# description. If set to NO, the Javadoc-style will behave just like regular Qt- +# style comments (thus requiring an explicit @brief command for a brief +# description.) +# The default value is: NO. + +JAVADOC_AUTOBRIEF = NO + +# If the JAVADOC_BANNER tag is set to YES then doxygen will interpret a line +# such as +# /*************** +# as being the beginning of a Javadoc-style comment "banner". If set to NO, the +# Javadoc-style will behave just like regular comments and it will not be +# interpreted by doxygen. +# The default value is: NO. + +JAVADOC_BANNER = NO + +# If the QT_AUTOBRIEF tag is set to YES then doxygen will interpret the first +# line (until the first dot) of a Qt-style comment as the brief description. If +# set to NO, the Qt-style will behave just like regular Qt-style comments (thus +# requiring an explicit \brief command for a brief description.) +# The default value is: NO. + +QT_AUTOBRIEF = NO + +# The MULTILINE_CPP_IS_BRIEF tag can be set to YES to make doxygen treat a +# multi-line C++ special comment block (i.e. a block of //! or /// comments) as +# a brief description. This used to be the default behavior. The new default is +# to treat a multi-line C++ comment block as a detailed description. Set this +# tag to YES if you prefer the old behavior instead. +# +# Note that setting this tag to YES also means that rational rose comments are +# not recognized any more. +# The default value is: NO. + +MULTILINE_CPP_IS_BRIEF = NO + +# By default Python docstrings are displayed as preformatted text and doxygen's +# special commands cannot be used. By setting PYTHON_DOCSTRING to NO the +# doxygen's special commands can be used and the contents of the docstring +# documentation blocks is shown as doxygen documentation. +# The default value is: YES. + +PYTHON_DOCSTRING = YES + +# If the INHERIT_DOCS tag is set to YES then an undocumented member inherits the +# documentation from any documented member that it re-implements. +# The default value is: YES. + +INHERIT_DOCS = YES + +# If the SEPARATE_MEMBER_PAGES tag is set to YES then doxygen will produce a new +# page for each member. If set to NO, the documentation of a member will be part +# of the file/class/namespace that contains it. +# The default value is: NO. + +SEPARATE_MEMBER_PAGES = NO + +# The TAB_SIZE tag can be used to set the number of spaces in a tab. Doxygen +# uses this value to replace tabs by spaces in code fragments. +# Minimum value: 1, maximum value: 16, default value: 4. + +TAB_SIZE = 4 + +# This tag can be used to specify a number of aliases that act as commands in +# the documentation. An alias has the form: +# name=value +# For example adding +# "sideeffect=@par Side Effects:^^" +# will allow you to put the command \sideeffect (or @sideeffect) in the +# documentation, which will result in a user-defined paragraph with heading +# "Side Effects:". Note that you cannot put \n's in the value part of an alias +# to insert newlines (in the resulting output). You can put ^^ in the value part +# of an alias to insert a newline as if a physical newline was in the original +# file. When you need a literal { or } or , in the value part of an alias you +# have to escape them by means of a backslash (\), this can lead to conflicts +# with the commands \{ and \} for these it is advised to use the version @{ and +# @} or use a double escape (\\{ and \\}) + +ALIASES = + +# Set the OPTIMIZE_OUTPUT_FOR_C tag to YES if your project consists of C sources +# only. Doxygen will then generate output that is more tailored for C. For +# instance, some of the names that are used will be different. The list of all +# members will be omitted, etc. +# The default value is: NO. + +OPTIMIZE_OUTPUT_FOR_C = NO + +# Set the OPTIMIZE_OUTPUT_JAVA tag to YES if your project consists of Java or +# Python sources only. Doxygen will then generate output that is more tailored +# for that language. For instance, namespaces will be presented as packages, +# qualified scopes will look different, etc. +# The default value is: NO. + +OPTIMIZE_OUTPUT_JAVA = NO + +# Set the OPTIMIZE_FOR_FORTRAN tag to YES if your project consists of Fortran +# sources. Doxygen will then generate output that is tailored for Fortran. +# The default value is: NO. + +OPTIMIZE_FOR_FORTRAN = NO + +# Set the OPTIMIZE_OUTPUT_VHDL tag to YES if your project consists of VHDL +# sources. Doxygen will then generate output that is tailored for VHDL. +# The default value is: NO. + +OPTIMIZE_OUTPUT_VHDL = NO + +# Set the OPTIMIZE_OUTPUT_SLICE tag to YES if your project consists of Slice +# sources only. Doxygen will then generate output that is more tailored for that +# language. For instance, namespaces will be presented as modules, types will be +# separated into more groups, etc. +# The default value is: NO. + +OPTIMIZE_OUTPUT_SLICE = NO + +# Doxygen selects the parser to use depending on the extension of the files it +# parses. With this tag you can assign which parser to use for a given +# extension. Doxygen has a built-in mapping, but you can override or extend it +# using this tag. The format is ext=language, where ext is a file extension, and +# language is one of the parsers supported by doxygen: IDL, Java, JavaScript, +# Csharp (C#), C, C++, Lex, D, PHP, md (Markdown), Objective-C, Python, Slice, +# VHDL, Fortran (fixed format Fortran: FortranFixed, free formatted Fortran: +# FortranFree, unknown formatted Fortran: Fortran. In the later case the parser +# tries to guess whether the code is fixed or free formatted code, this is the +# default for Fortran type files). For instance to make doxygen treat .inc files +# as Fortran files (default is PHP), and .f files as C (default is Fortran), +# use: inc=Fortran f=C. +# +# Note: For files without extension you can use no_extension as a placeholder. +# +# Note that for custom extensions you also need to set FILE_PATTERNS otherwise +# the files are not read by doxygen. When specifying no_extension you should add +# * to the FILE_PATTERNS. +# +# Note see also the list of default file extension mappings. + +EXTENSION_MAPPING = + +# If the MARKDOWN_SUPPORT tag is enabled then doxygen pre-processes all comments +# according to the Markdown format, which allows for more readable +# documentation. See https://daringfireball.net/projects/markdown/ for details. +# The output of markdown processing is further processed by doxygen, so you can +# mix doxygen, HTML, and XML commands with Markdown formatting. Disable only in +# case of backward compatibilities issues. +# The default value is: YES. + +MARKDOWN_SUPPORT = YES + +# When the TOC_INCLUDE_HEADINGS tag is set to a non-zero value, all headings up +# to that level are automatically included in the table of contents, even if +# they do not have an id attribute. +# Note: This feature currently applies only to Markdown headings. +# Minimum value: 0, maximum value: 99, default value: 5. +# This tag requires that the tag MARKDOWN_SUPPORT is set to YES. + +TOC_INCLUDE_HEADINGS = 5 + +# When enabled doxygen tries to link words that correspond to documented +# classes, or namespaces to their corresponding documentation. Such a link can +# be prevented in individual cases by putting a % sign in front of the word or +# globally by setting AUTOLINK_SUPPORT to NO. +# The default value is: YES. + +AUTOLINK_SUPPORT = YES + +# If you use STL classes (i.e. std::string, std::vector, etc.) but do not want +# to include (a tag file for) the STL sources as input, then you should set this +# tag to YES in order to let doxygen match functions declarations and +# definitions whose arguments contain STL classes (e.g. func(std::string); +# versus func(std::string) {}). This also make the inheritance and collaboration +# diagrams that involve STL classes more complete and accurate. +# The default value is: NO. + +BUILTIN_STL_SUPPORT = NO + +# If you use Microsoft's C++/CLI language, you should set this option to YES to +# enable parsing support. +# The default value is: NO. + +CPP_CLI_SUPPORT = NO + +# Set the SIP_SUPPORT tag to YES if your project consists of sip (see: +# https://www.riverbankcomputing.com/software/sip/intro) sources only. Doxygen +# will parse them like normal C++ but will assume all classes use public instead +# of private inheritance when no explicit protection keyword is present. +# The default value is: NO. + +SIP_SUPPORT = NO + +# For Microsoft's IDL there are propget and propput attributes to indicate +# getter and setter methods for a property. Setting this option to YES will make +# doxygen to replace the get and set methods by a property in the documentation. +# This will only work if the methods are indeed getting or setting a simple +# type. If this is not the case, or you want to show the methods anyway, you +# should set this option to NO. +# The default value is: YES. + +IDL_PROPERTY_SUPPORT = YES + +# If member grouping is used in the documentation and the DISTRIBUTE_GROUP_DOC +# tag is set to YES then doxygen will reuse the documentation of the first +# member in the group (if any) for the other members of the group. By default +# all members of a group must be documented explicitly. +# The default value is: NO. + +DISTRIBUTE_GROUP_DOC = NO + +# If one adds a struct or class to a group and this option is enabled, then also +# any nested class or struct is added to the same group. By default this option +# is disabled and one has to add nested compounds explicitly via \ingroup. +# The default value is: NO. + +GROUP_NESTED_COMPOUNDS = NO + +# Set the SUBGROUPING tag to YES to allow class member groups of the same type +# (for instance a group of public functions) to be put as a subgroup of that +# type (e.g. under the Public Functions section). Set it to NO to prevent +# subgrouping. Alternatively, this can be done per class using the +# \nosubgrouping command. +# The default value is: YES. + +SUBGROUPING = YES + +# When the INLINE_GROUPED_CLASSES tag is set to YES, classes, structs and unions +# are shown inside the group in which they are included (e.g. using \ingroup) +# instead of on a separate page (for HTML and Man pages) or section (for LaTeX +# and RTF). +# +# Note that this feature does not work in combination with +# SEPARATE_MEMBER_PAGES. +# The default value is: NO. + +INLINE_GROUPED_CLASSES = NO + +# When the INLINE_SIMPLE_STRUCTS tag is set to YES, structs, classes, and unions +# with only public data fields or simple typedef fields will be shown inline in +# the documentation of the scope in which they are defined (i.e. file, +# namespace, or group documentation), provided this scope is documented. If set +# to NO, structs, classes, and unions are shown on a separate page (for HTML and +# Man pages) or section (for LaTeX and RTF). +# The default value is: NO. + +INLINE_SIMPLE_STRUCTS = NO + +# When TYPEDEF_HIDES_STRUCT tag is enabled, a typedef of a struct, union, or +# enum is documented as struct, union, or enum with the name of the typedef. So +# typedef struct TypeS {} TypeT, will appear in the documentation as a struct +# with name TypeT. When disabled the typedef will appear as a member of a file, +# namespace, or class. And the struct will be named TypeS. This can typically be +# useful for C code in case the coding convention dictates that all compound +# types are typedef'ed and only the typedef is referenced, never the tag name. +# The default value is: NO. + +TYPEDEF_HIDES_STRUCT = NO + +# The size of the symbol lookup cache can be set using LOOKUP_CACHE_SIZE. This +# cache is used to resolve symbols given their name and scope. Since this can be +# an expensive process and often the same symbol appears multiple times in the +# code, doxygen keeps a cache of pre-resolved symbols. If the cache is too small +# doxygen will become slower. If the cache is too large, memory is wasted. The +# cache size is given by this formula: 2^(16+LOOKUP_CACHE_SIZE). The valid range +# is 0..9, the default is 0, corresponding to a cache size of 2^16=65536 +# symbols. At the end of a run doxygen will report the cache usage and suggest +# the optimal cache size from a speed point of view. +# Minimum value: 0, maximum value: 9, default value: 0. + +LOOKUP_CACHE_SIZE = 0 + +# The NUM_PROC_THREADS specifies the number of threads doxygen is allowed to use +# during processing. When set to 0 doxygen will based this on the number of +# cores available in the system. You can set it explicitly to a value larger +# than 0 to get more control over the balance between CPU load and processing +# speed. At this moment only the input processing can be done using multiple +# threads. Since this is still an experimental feature the default is set to 1, +# which effectively disables parallel processing. Please report any issues you +# encounter. Generating dot graphs in parallel is controlled by the +# DOT_NUM_THREADS setting. +# Minimum value: 0, maximum value: 32, default value: 1. + +NUM_PROC_THREADS = 1 + +#--------------------------------------------------------------------------- +# Build related configuration options +#--------------------------------------------------------------------------- + +# If the EXTRACT_ALL tag is set to YES, doxygen will assume all entities in +# documentation are documented, even if no documentation was available. Private +# class members and static file members will be hidden unless the +# EXTRACT_PRIVATE respectively EXTRACT_STATIC tags are set to YES. +# Note: This will also disable the warnings about undocumented members that are +# normally produced when WARNINGS is set to YES. +# The default value is: NO. + +EXTRACT_ALL = YES + +# If the EXTRACT_PRIVATE tag is set to YES, all private members of a class will +# be included in the documentation. +# The default value is: NO. + +EXTRACT_PRIVATE = YES + +# If the EXTRACT_PRIV_VIRTUAL tag is set to YES, documented private virtual +# methods of a class will be included in the documentation. +# The default value is: NO. + +EXTRACT_PRIV_VIRTUAL = NO + +# If the EXTRACT_PACKAGE tag is set to YES, all members with package or internal +# scope will be included in the documentation. +# The default value is: NO. + +EXTRACT_PACKAGE = NO + +# If the EXTRACT_STATIC tag is set to YES, all static members of a file will be +# included in the documentation. +# The default value is: NO. + +EXTRACT_STATIC = YES + +# If the EXTRACT_LOCAL_CLASSES tag is set to YES, classes (and structs) defined +# locally in source files will be included in the documentation. If set to NO, +# only classes defined in header files are included. Does not have any effect +# for Java sources. +# The default value is: YES. + +EXTRACT_LOCAL_CLASSES = YES + +# This flag is only useful for Objective-C code. If set to YES, local methods, +# which are defined in the implementation section but not in the interface are +# included in the documentation. If set to NO, only methods in the interface are +# included. +# The default value is: NO. + +EXTRACT_LOCAL_METHODS = NO + +# If this flag is set to YES, the members of anonymous namespaces will be +# extracted and appear in the documentation as a namespace called +# 'anonymous_namespace{file}', where file will be replaced with the base name of +# the file that contains the anonymous namespace. By default anonymous namespace +# are hidden. +# The default value is: NO. + +EXTRACT_ANON_NSPACES = NO + +# If this flag is set to YES, the name of an unnamed parameter in a declaration +# will be determined by the corresponding definition. By default unnamed +# parameters remain unnamed in the output. +# The default value is: YES. + +RESOLVE_UNNAMED_PARAMS = YES + +# If the HIDE_UNDOC_MEMBERS tag is set to YES, doxygen will hide all +# undocumented members inside documented classes or files. If set to NO these +# members will be included in the various overviews, but no documentation +# section is generated. This option has no effect if EXTRACT_ALL is enabled. +# The default value is: NO. + +HIDE_UNDOC_MEMBERS = NO + +# If the HIDE_UNDOC_CLASSES tag is set to YES, doxygen will hide all +# undocumented classes that are normally visible in the class hierarchy. If set +# to NO, these classes will be included in the various overviews. This option +# has no effect if EXTRACT_ALL is enabled. +# The default value is: NO. + +HIDE_UNDOC_CLASSES = NO + +# If the HIDE_FRIEND_COMPOUNDS tag is set to YES, doxygen will hide all friend +# declarations. If set to NO, these declarations will be included in the +# documentation. +# The default value is: NO. + +HIDE_FRIEND_COMPOUNDS = NO + +# If the HIDE_IN_BODY_DOCS tag is set to YES, doxygen will hide any +# documentation blocks found inside the body of a function. If set to NO, these +# blocks will be appended to the function's detailed documentation block. +# The default value is: NO. + +HIDE_IN_BODY_DOCS = NO + +# The INTERNAL_DOCS tag determines if documentation that is typed after a +# \internal command is included. If the tag is set to NO then the documentation +# will be excluded. Set it to YES to include the internal documentation. +# The default value is: NO. + +INTERNAL_DOCS = NO + +# With the correct setting of option CASE_SENSE_NAMES doxygen will better be +# able to match the capabilities of the underlying filesystem. In case the +# filesystem is case sensitive (i.e. it supports files in the same directory +# whose names only differ in casing), the option must be set to YES to properly +# deal with such files in case they appear in the input. For filesystems that +# are not case sensitive the option should be set to NO to properly deal with +# output files written for symbols that only differ in casing, such as for two +# classes, one named CLASS and the other named Class, and to also support +# references to files without having to specify the exact matching casing. On +# Windows (including Cygwin) and MacOS, users should typically set this option +# to NO, whereas on Linux or other Unix flavors it should typically be set to +# YES. +# Possible values are: SYSTEM, NO and YES. +# The default value is: SYSTEM. + +CASE_SENSE_NAMES = SYSTEM + +# If the HIDE_SCOPE_NAMES tag is set to NO then doxygen will show members with +# their full class and namespace scopes in the documentation. If set to YES, the +# scope will be hidden. +# The default value is: NO. + +HIDE_SCOPE_NAMES = NO + +# If the HIDE_COMPOUND_REFERENCE tag is set to NO (default) then doxygen will +# append additional text to a page's title, such as Class Reference. If set to +# YES the compound reference will be hidden. +# The default value is: NO. + +HIDE_COMPOUND_REFERENCE= NO + +# If the SHOW_HEADERFILE tag is set to YES then the documentation for a class +# will show which file needs to be included to use the class. +# The default value is: YES. + +SHOW_HEADERFILE = YES + +# If the SHOW_INCLUDE_FILES tag is set to YES then doxygen will put a list of +# the files that are included by a file in the documentation of that file. +# The default value is: YES. + +SHOW_INCLUDE_FILES = YES + +# If the SHOW_GROUPED_MEMB_INC tag is set to YES then Doxygen will add for each +# grouped member an include statement to the documentation, telling the reader +# which file to include in order to use the member. +# The default value is: NO. + +SHOW_GROUPED_MEMB_INC = NO + +# If the FORCE_LOCAL_INCLUDES tag is set to YES then doxygen will list include +# files with double quotes in the documentation rather than with sharp brackets. +# The default value is: NO. + +FORCE_LOCAL_INCLUDES = NO + +# If the INLINE_INFO tag is set to YES then a tag [inline] is inserted in the +# documentation for inline members. +# The default value is: YES. + +INLINE_INFO = YES + +# If the SORT_MEMBER_DOCS tag is set to YES then doxygen will sort the +# (detailed) documentation of file and class members alphabetically by member +# name. If set to NO, the members will appear in declaration order. +# The default value is: YES. + +SORT_MEMBER_DOCS = YES + +# If the SORT_BRIEF_DOCS tag is set to YES then doxygen will sort the brief +# descriptions of file, namespace and class members alphabetically by member +# name. If set to NO, the members will appear in declaration order. Note that +# this will also influence the order of the classes in the class list. +# The default value is: NO. + +SORT_BRIEF_DOCS = NO + +# If the SORT_MEMBERS_CTORS_1ST tag is set to YES then doxygen will sort the +# (brief and detailed) documentation of class members so that constructors and +# destructors are listed first. If set to NO the constructors will appear in the +# respective orders defined by SORT_BRIEF_DOCS and SORT_MEMBER_DOCS. +# Note: If SORT_BRIEF_DOCS is set to NO this option is ignored for sorting brief +# member documentation. +# Note: If SORT_MEMBER_DOCS is set to NO this option is ignored for sorting +# detailed member documentation. +# The default value is: NO. + +SORT_MEMBERS_CTORS_1ST = NO + +# If the SORT_GROUP_NAMES tag is set to YES then doxygen will sort the hierarchy +# of group names into alphabetical order. If set to NO the group names will +# appear in their defined order. +# The default value is: NO. + +SORT_GROUP_NAMES = NO + +# If the SORT_BY_SCOPE_NAME tag is set to YES, the class list will be sorted by +# fully-qualified names, including namespaces. If set to NO, the class list will +# be sorted only by class name, not including the namespace part. +# Note: This option is not very useful if HIDE_SCOPE_NAMES is set to YES. +# Note: This option applies only to the class list, not to the alphabetical +# list. +# The default value is: NO. + +SORT_BY_SCOPE_NAME = NO + +# If the STRICT_PROTO_MATCHING option is enabled and doxygen fails to do proper +# type resolution of all parameters of a function it will reject a match between +# the prototype and the implementation of a member function even if there is +# only one candidate or it is obvious which candidate to choose by doing a +# simple string match. By disabling STRICT_PROTO_MATCHING doxygen will still +# accept a match between prototype and implementation in such cases. +# The default value is: NO. + +STRICT_PROTO_MATCHING = NO + +# The GENERATE_TODOLIST tag can be used to enable (YES) or disable (NO) the todo +# list. This list is created by putting \todo commands in the documentation. +# The default value is: YES. + +GENERATE_TODOLIST = YES + +# The GENERATE_TESTLIST tag can be used to enable (YES) or disable (NO) the test +# list. This list is created by putting \test commands in the documentation. +# The default value is: YES. + +GENERATE_TESTLIST = YES + +# The GENERATE_BUGLIST tag can be used to enable (YES) or disable (NO) the bug +# list. This list is created by putting \bug commands in the documentation. +# The default value is: YES. + +GENERATE_BUGLIST = YES + +# The GENERATE_DEPRECATEDLIST tag can be used to enable (YES) or disable (NO) +# the deprecated list. This list is created by putting \deprecated commands in +# the documentation. +# The default value is: YES. + +GENERATE_DEPRECATEDLIST= YES + +# The ENABLED_SECTIONS tag can be used to enable conditional documentation +# sections, marked by \if ... \endif and \cond +# ... \endcond blocks. + +ENABLED_SECTIONS = + +# The MAX_INITIALIZER_LINES tag determines the maximum number of lines that the +# initial value of a variable or macro / define can have for it to appear in the +# documentation. If the initializer consists of more lines than specified here +# it will be hidden. Use a value of 0 to hide initializers completely. The +# appearance of the value of individual variables and macros / defines can be +# controlled using \showinitializer or \hideinitializer command in the +# documentation regardless of this setting. +# Minimum value: 0, maximum value: 10000, default value: 30. + +MAX_INITIALIZER_LINES = 30 + +# Set the SHOW_USED_FILES tag to NO to disable the list of files generated at +# the bottom of the documentation of classes and structs. If set to YES, the +# list will mention the files that were used to generate the documentation. +# The default value is: YES. + +SHOW_USED_FILES = YES + +# Set the SHOW_FILES tag to NO to disable the generation of the Files page. This +# will remove the Files entry from the Quick Index and from the Folder Tree View +# (if specified). +# The default value is: YES. + +SHOW_FILES = YES + +# Set the SHOW_NAMESPACES tag to NO to disable the generation of the Namespaces +# page. This will remove the Namespaces entry from the Quick Index and from the +# Folder Tree View (if specified). +# The default value is: YES. + +SHOW_NAMESPACES = YES + +# The FILE_VERSION_FILTER tag can be used to specify a program or script that +# doxygen should invoke to get the current version for each file (typically from +# the version control system). Doxygen will invoke the program by executing (via +# popen()) the command command input-file, where command is the value of the +# FILE_VERSION_FILTER tag, and input-file is the name of an input file provided +# by doxygen. Whatever the program writes to standard output is used as the file +# version. For an example see the documentation. + +FILE_VERSION_FILTER = + +# The LAYOUT_FILE tag can be used to specify a layout file which will be parsed +# by doxygen. The layout file controls the global structure of the generated +# output files in an output format independent way. To create the layout file +# that represents doxygen's defaults, run doxygen with the -l option. You can +# optionally specify a file name after the option, if omitted DoxygenLayout.xml +# will be used as the name of the layout file. See also section "Changing the +# layout of pages" for information. +# +# Note that if you run doxygen from a directory containing a file called +# DoxygenLayout.xml, doxygen will parse it automatically even if the LAYOUT_FILE +# tag is left empty. + +LAYOUT_FILE = + +# The CITE_BIB_FILES tag can be used to specify one or more bib files containing +# the reference definitions. This must be a list of .bib files. The .bib +# extension is automatically appended if omitted. This requires the bibtex tool +# to be installed. See also https://en.wikipedia.org/wiki/BibTeX for more info. +# For LaTeX the style of the bibliography can be controlled using +# LATEX_BIB_STYLE. To use this feature you need bibtex and perl available in the +# search path. See also \cite for info how to create references. + +CITE_BIB_FILES = + +#--------------------------------------------------------------------------- +# Configuration options related to warning and progress messages +#--------------------------------------------------------------------------- + +# The QUIET tag can be used to turn on/off the messages that are generated to +# standard output by doxygen. If QUIET is set to YES this implies that the +# messages are off. +# The default value is: NO. + +QUIET = YES + +# The WARNINGS tag can be used to turn on/off the warning messages that are +# generated to standard error (stderr) by doxygen. If WARNINGS is set to YES +# this implies that the warnings are on. +# +# Tip: Turn warnings on while writing the documentation. +# The default value is: YES. + +WARNINGS = YES + +# If the WARN_IF_UNDOCUMENTED tag is set to YES then doxygen will generate +# warnings for undocumented members. If EXTRACT_ALL is set to YES then this flag +# will automatically be disabled. +# The default value is: YES. + +WARN_IF_UNDOCUMENTED = YES + +# If the WARN_IF_DOC_ERROR tag is set to YES, doxygen will generate warnings for +# potential errors in the documentation, such as documenting some parameters in +# a documented function twice, or documenting parameters that don't exist or +# using markup commands wrongly. +# The default value is: YES. + +WARN_IF_DOC_ERROR = YES + +# If WARN_IF_INCOMPLETE_DOC is set to YES, doxygen will warn about incomplete +# function parameter documentation. If set to NO, doxygen will accept that some +# parameters have no documentation without warning. +# The default value is: YES. + +WARN_IF_INCOMPLETE_DOC = YES + +# This WARN_NO_PARAMDOC option can be enabled to get warnings for functions that +# are documented, but have no documentation for their parameters or return +# value. If set to NO, doxygen will only warn about wrong parameter +# documentation, but not about the absence of documentation. If EXTRACT_ALL is +# set to YES then this flag will automatically be disabled. See also +# WARN_IF_INCOMPLETE_DOC +# The default value is: NO. + +WARN_NO_PARAMDOC = NO + +# If the WARN_AS_ERROR tag is set to YES then doxygen will immediately stop when +# a warning is encountered. If the WARN_AS_ERROR tag is set to FAIL_ON_WARNINGS +# then doxygen will continue running as if WARN_AS_ERROR tag is set to NO, but +# at the end of the doxygen process doxygen will return with a non-zero status. +# Possible values are: NO, YES and FAIL_ON_WARNINGS. +# The default value is: NO. + +WARN_AS_ERROR = NO + +# The WARN_FORMAT tag determines the format of the warning messages that doxygen +# can produce. The string should contain the $file, $line, and $text tags, which +# will be replaced by the file and line number from which the warning originated +# and the warning text. Optionally the format may contain $version, which will +# be replaced by the version of the file (if it could be obtained via +# FILE_VERSION_FILTER) +# See also: WARN_LINE_FORMAT +# The default value is: $file:$line: $text. + +WARN_FORMAT = "$file:$line: $text" + +# In the $text part of the WARN_FORMAT command it is possible that a reference +# to a more specific place is given. To make it easier to jump to this place +# (outside of doxygen) the user can define a custom "cut" / "paste" string. +# Example: +# WARN_LINE_FORMAT = "'vi $file +$line'" +# See also: WARN_FORMAT +# The default value is: at line $line of file $file. + +WARN_LINE_FORMAT = "at line $line of file $file" + +# The WARN_LOGFILE tag can be used to specify a file to which warning and error +# messages should be written. If left blank the output is written to standard +# error (stderr). In case the file specified cannot be opened for writing the +# warning and error messages are written to standard error. When as file - is +# specified the warning and error messages are written to standard output +# (stdout). + +WARN_LOGFILE = + +#--------------------------------------------------------------------------- +# Configuration options related to the input files +#--------------------------------------------------------------------------- + +# The INPUT tag is used to specify the files and/or directories that contain +# documented source files. You may enter file names like myfile.cpp or +# directories like /usr/src/myproject. Separate the files or directories with +# spaces. See also FILE_PATTERNS and EXTENSION_MAPPING +# Note: If this tag is empty the current directory is searched. + +INPUT = ../ ../../../ansi-c/library/cprover_contracts.c + +# This tag can be used to specify the character encoding of the source files +# that doxygen parses. Internally doxygen uses the UTF-8 encoding. Doxygen uses +# libiconv (or the iconv built into libc) for the transcoding. See the libiconv +# documentation (see: +# https://www.gnu.org/software/libiconv/) for the list of possible encodings. +# See also: INPUT_FILE_ENCODING +# The default value is: UTF-8. + +INPUT_ENCODING = UTF-8 + +# This tag can be used to specify the character encoding of the source files +# that doxygen parses The INPUT_FILE_ENCODING tag can be used to specify +# character encoding on a per file pattern basis. Doxygen will compare the file +# name with each pattern and apply the encoding instead of the default +# INPUT_ENCODING) if there is a match. The character encodings are a list of the +# form: pattern=encoding (like *.php=ISO-8859-1). See cfg_input_encoding +# "INPUT_ENCODING" for further information on supported encodings. + +INPUT_FILE_ENCODING = + +# If the value of the INPUT tag contains directories, you can use the +# FILE_PATTERNS tag to specify one or more wildcard patterns (like *.cpp and +# *.h) to filter out the source-files in the directories. +# +# Note that for custom extensions or not directly supported extensions you also +# need to set EXTENSION_MAPPING for the extension otherwise the files are not +# read by doxygen. +# +# Note the list of default checked file patterns might differ from the list of +# default file extension mappings. +# +# If left blank the following patterns are tested:*.c, *.cc, *.cxx, *.cpp, +# *.c++, *.java, *.ii, *.ixx, *.ipp, *.i++, *.inl, *.idl, *.ddl, *.odl, *.h, +# *.hh, *.hxx, *.hpp, *.h++, *.l, *.cs, *.d, *.php, *.php4, *.php5, *.phtml, +# *.inc, *.m, *.markdown, *.md, *.mm, *.dox (to be provided as doxygen C +# comment), *.py, *.pyw, *.f90, *.f95, *.f03, *.f08, *.f18, *.f, *.for, *.vhd, +# *.vhdl, *.ucf, *.qsf and *.ice. + +FILE_PATTERNS = *.cpp \ + *.h \ + *.md + +# The RECURSIVE tag can be used to specify whether or not subdirectories should +# be searched for input files as well. +# The default value is: NO. + +RECURSIVE = YES + +# The EXCLUDE tag can be used to specify files and/or directories that should be +# excluded from the INPUT source files. This way you can easily exclude a +# subdirectory from a directory tree whose root is specified with the INPUT tag. +# +# Note that relative paths are relative to the directory from which doxygen is +# run. + +EXCLUDE = + +# The EXCLUDE_SYMLINKS tag can be used to select whether or not files or +# directories that are symbolic links (a Unix file system feature) are excluded +# from the input. +# The default value is: NO. + +EXCLUDE_SYMLINKS = NO + +# If the value of the INPUT tag contains directories, you can use the +# EXCLUDE_PATTERNS tag to specify one or more wildcard patterns to exclude +# certain files from those directories. +# +# Note that the wildcards are matched against the file with absolute path, so to +# exclude all test directories for example use the pattern */test/* + +EXCLUDE_PATTERNS = */.svn/* \ + */.git/* + +# The EXCLUDE_SYMBOLS tag can be used to specify one or more symbol names +# (namespaces, classes, functions, etc.) that should be excluded from the +# output. The symbol name can be a fully qualified name, a word, or if the +# wildcard * is used, a substring. Examples: ANamespace, AClass, +# ANamespace::AClass, ANamespace::*Test +# +# Note that the wildcards are matched against the file with absolute path, so to +# exclude all test directories use the pattern */test/* + +EXCLUDE_SYMBOLS = + +# The EXAMPLE_PATH tag can be used to specify one or more files or directories +# that contain example code fragments that are included (see the \include +# command). + +EXAMPLE_PATH = doc/assets + +# If the value of the EXAMPLE_PATH tag contains directories, you can use the +# EXAMPLE_PATTERNS tag to specify one or more wildcard pattern (like *.cpp and +# *.h) to filter out the source-files in the directories. If left blank all +# files are included. + +EXAMPLE_PATTERNS = * + +# If the EXAMPLE_RECURSIVE tag is set to YES then subdirectories will be +# searched for input files to be used with the \include or \dontinclude commands +# irrespective of the value of the RECURSIVE tag. +# The default value is: NO. + +EXAMPLE_RECURSIVE = NO + +# The IMAGE_PATH tag can be used to specify one or more files or directories +# that contain images that are to be included in the documentation (see the +# \image command). + +IMAGE_PATH = doc/assets + +# The INPUT_FILTER tag can be used to specify a program that doxygen should +# invoke to filter for each input file. Doxygen will invoke the filter program +# by executing (via popen()) the command: +# +# +# +# where is the value of the INPUT_FILTER tag, and is the +# name of an input file. Doxygen will then use the output that the filter +# program writes to standard output. If FILTER_PATTERNS is specified, this tag +# will be ignored. +# +# Note that the filter must not add or remove lines; it is applied before the +# code is scanned, but not when the output code is generated. If lines are added +# or removed, the anchors will not be placed correctly. +# +# Note that doxygen will use the data processed and written to standard output +# for further processing, therefore nothing else, like debug statements or used +# commands (so in case of a Windows batch file always use @echo OFF), should be +# written to standard output. +# +# Note that for custom extensions or not directly supported extensions you also +# need to set EXTENSION_MAPPING for the extension otherwise the files are not +# properly processed by doxygen. + +INPUT_FILTER = + +# The FILTER_PATTERNS tag can be used to specify filters on a per file pattern +# basis. Doxygen will compare the file name with each pattern and apply the +# filter if there is a match. The filters are a list of the form: pattern=filter +# (like *.cpp=my_cpp_filter). See INPUT_FILTER for further information on how +# filters are used. If the FILTER_PATTERNS tag is empty or if none of the +# patterns match the file name, INPUT_FILTER is applied. +# +# Note that for custom extensions or not directly supported extensions you also +# need to set EXTENSION_MAPPING for the extension otherwise the files are not +# properly processed by doxygen. + +FILTER_PATTERNS = + +# If the FILTER_SOURCE_FILES tag is set to YES, the input filter (if set using +# INPUT_FILTER) will also be used to filter the input files that are used for +# producing the source files to browse (i.e. when SOURCE_BROWSER is set to YES). +# The default value is: NO. + +FILTER_SOURCE_FILES = NO + +# The FILTER_SOURCE_PATTERNS tag can be used to specify source filters per file +# pattern. A pattern will override the setting for FILTER_PATTERN (if any) and +# it is also possible to disable source filtering for a specific pattern using +# *.ext= (so without naming a filter). +# This tag requires that the tag FILTER_SOURCE_FILES is set to YES. + +FILTER_SOURCE_PATTERNS = + +# If the USE_MDFILE_AS_MAINPAGE tag refers to the name of a markdown file that +# is part of the input, its contents will be placed on the main page +# (index.html). This can be useful if you have a project on for instance GitHub +# and want to reuse the introduction page also for the doxygen output. + +USE_MDFILE_AS_MAINPAGE = doc/contracts-mainpage.md + +# The Fortran standard specifies that for fixed formatted Fortran code all +# characters from position 72 are to be considered as comment. A common +# extension is to allow longer lines before the automatic comment starts. The +# setting FORTRAN_COMMENT_AFTER will also make it possible that longer lines can +# be processed before the automatic comment starts. +# Minimum value: 7, maximum value: 10000, default value: 72. + +FORTRAN_COMMENT_AFTER = 72 + +#--------------------------------------------------------------------------- +# Configuration options related to source browsing +#--------------------------------------------------------------------------- + +# If the SOURCE_BROWSER tag is set to YES then a list of source files will be +# generated. Documented entities will be cross-referenced with these sources. +# +# Note: To get rid of all source code in the generated output, make sure that +# also VERBATIM_HEADERS is set to NO. +# The default value is: NO. + +SOURCE_BROWSER = YES + +# Setting the INLINE_SOURCES tag to YES will include the body of functions, +# classes and enums directly into the documentation. +# The default value is: NO. + +INLINE_SOURCES = NO + +# Setting the STRIP_CODE_COMMENTS tag to YES will instruct doxygen to hide any +# special comment blocks from generated source code fragments. Normal C, C++ and +# Fortran comments will always remain visible. +# The default value is: YES. + +STRIP_CODE_COMMENTS = YES + +# If the REFERENCED_BY_RELATION tag is set to YES then for each documented +# entity all documented functions referencing it will be listed. +# The default value is: NO. + +REFERENCED_BY_RELATION = NO + +# If the REFERENCES_RELATION tag is set to YES then for each documented function +# all documented entities called/used by that function will be listed. +# The default value is: NO. + +REFERENCES_RELATION = NO + +# If the REFERENCES_LINK_SOURCE tag is set to YES and SOURCE_BROWSER tag is set +# to YES then the hyperlinks from functions in REFERENCES_RELATION and +# REFERENCED_BY_RELATION lists will link to the source code. Otherwise they will +# link to the documentation. +# The default value is: YES. + +REFERENCES_LINK_SOURCE = YES + +# If SOURCE_TOOLTIPS is enabled (the default) then hovering a hyperlink in the +# source code will show a tooltip with additional information such as prototype, +# brief description and links to the definition and documentation. Since this +# will make the HTML file larger and loading of large files a bit slower, you +# can opt to disable this feature. +# The default value is: YES. +# This tag requires that the tag SOURCE_BROWSER is set to YES. + +SOURCE_TOOLTIPS = YES + +# If the USE_HTAGS tag is set to YES then the references to source code will +# point to the HTML generated by the htags(1) tool instead of doxygen built-in +# source browser. The htags tool is part of GNU's global source tagging system +# (see https://www.gnu.org/software/global/global.html). You will need version +# 4.8.6 or higher. +# +# To use it do the following: +# - Install the latest version of global +# - Enable SOURCE_BROWSER and USE_HTAGS in the configuration file +# - Make sure the INPUT points to the root of the source tree +# - Run doxygen as normal +# +# Doxygen will invoke htags (and that will in turn invoke gtags), so these +# tools must be available from the command line (i.e. in the search path). +# +# The result: instead of the source browser generated by doxygen, the links to +# source code will now point to the output of htags. +# The default value is: NO. +# This tag requires that the tag SOURCE_BROWSER is set to YES. + +USE_HTAGS = NO + +# If the VERBATIM_HEADERS tag is set the YES then doxygen will generate a +# verbatim copy of the header file for each class for which an include is +# specified. Set to NO to disable this. +# See also: Section \class. +# The default value is: YES. + +VERBATIM_HEADERS = YES + +#--------------------------------------------------------------------------- +# Configuration options related to the alphabetical class index +#--------------------------------------------------------------------------- + +# If the ALPHABETICAL_INDEX tag is set to YES, an alphabetical index of all +# compounds will be generated. Enable this if the project contains a lot of +# classes, structs, unions or interfaces. +# The default value is: YES. + +ALPHABETICAL_INDEX = YES + +# In case all classes in a project start with a common prefix, all classes will +# be put under the same header in the alphabetical index. The IGNORE_PREFIX tag +# can be used to specify a prefix (or a list of prefixes) that should be ignored +# while generating the index headers. +# This tag requires that the tag ALPHABETICAL_INDEX is set to YES. + +IGNORE_PREFIX = + +#--------------------------------------------------------------------------- +# Configuration options related to the HTML output +#--------------------------------------------------------------------------- + +# If the GENERATE_HTML tag is set to YES, doxygen will generate HTML output +# The default value is: YES. + +GENERATE_HTML = YES + +# The HTML_OUTPUT tag is used to specify where the HTML docs will be put. If a +# relative path is entered the value of OUTPUT_DIRECTORY will be put in front of +# it. +# The default directory is: html. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_OUTPUT = html + +# The HTML_FILE_EXTENSION tag can be used to specify the file extension for each +# generated HTML page (for example: .htm, .php, .asp). +# The default value is: .html. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_FILE_EXTENSION = .html + +# The HTML_HEADER tag can be used to specify a user-defined HTML header file for +# each generated HTML page. If the tag is left blank doxygen will generate a +# standard header. +# +# To get valid HTML the header file that includes any scripts and style sheets +# that doxygen needs, which is dependent on the configuration options used (e.g. +# the setting GENERATE_TREEVIEW). It is highly recommended to start with a +# default header using +# doxygen -w html new_header.html new_footer.html new_stylesheet.css +# YourConfigFile +# and then modify the file new_header.html. See also section "Doxygen usage" +# for information on how to generate the default header that doxygen normally +# uses. +# Note: The header is subject to change so you typically have to regenerate the +# default header when upgrading to a newer version of doxygen. For a description +# of the possible markers and block names see the documentation. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_HEADER = + +# The HTML_FOOTER tag can be used to specify a user-defined HTML footer for each +# generated HTML page. If the tag is left blank doxygen will generate a standard +# footer. See HTML_HEADER for more information on how to generate a default +# footer and what special commands can be used inside the footer. See also +# section "Doxygen usage" for information on how to generate the default footer +# that doxygen normally uses. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_FOOTER = + +# The HTML_STYLESHEET tag can be used to specify a user-defined cascading style +# sheet that is used by each HTML page. It can be used to fine-tune the look of +# the HTML output. If left blank doxygen will generate a default style sheet. +# See also section "Doxygen usage" for information on how to generate the style +# sheet that doxygen normally uses. +# Note: It is recommended to use HTML_EXTRA_STYLESHEET instead of this tag, as +# it is more robust and this tag (HTML_STYLESHEET) will in the future become +# obsolete. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_STYLESHEET = + +# The HTML_EXTRA_STYLESHEET tag can be used to specify additional user-defined +# cascading style sheets that are included after the standard style sheets +# created by doxygen. Using this option one can overrule certain style aspects. +# This is preferred over using HTML_STYLESHEET since it does not replace the +# standard style sheet and is therefore more robust against future updates. +# Doxygen will copy the style sheet files to the output directory. +# Note: The order of the extra style sheet files is of importance (e.g. the last +# style sheet in the list overrules the setting of the previous ones in the +# list). For an example see the documentation. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_EXTRA_STYLESHEET = + +# The HTML_EXTRA_FILES tag can be used to specify one or more extra images or +# other source files which should be copied to the HTML output directory. Note +# that these files will be copied to the base HTML output directory. Use the +# $relpath^ marker in the HTML_HEADER and/or HTML_FOOTER files to load these +# files. In the HTML_STYLESHEET file, use the file name only. Also note that the +# files will be copied as-is; there are no commands or markers available. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_EXTRA_FILES = + +# The HTML_COLORSTYLE tag can be used to specify if the generated HTML output +# should be rendered with a dark or light theme. Default setting AUTO_LIGHT +# enables light output unless the user preference is dark output. Other options +# are DARK to always use dark mode, LIGHT to always use light mode, AUTO_DARK to +# default to dark mode unless the user prefers light mode, and TOGGLE to let the +# user toggle between dark and light mode via a button. +# Possible values are: LIGHT Always generate light output., DARK Always generate +# dark output., AUTO_LIGHT Automatically set the mode according to the user +# preference, use light mode if no preference is set (the default)., AUTO_DARK +# Automatically set the mode according to the user preference, use dark mode if +# no preference is set. and TOGGLE Allow to user to switch between light and +# dark mode via a button.. +# The default value is: AUTO_LIGHT. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_COLORSTYLE = AUTO_LIGHT + +# The HTML_COLORSTYLE_HUE tag controls the color of the HTML output. Doxygen +# will adjust the colors in the style sheet and background images according to +# this color. Hue is specified as an angle on a color-wheel, see +# https://en.wikipedia.org/wiki/Hue for more information. For instance the value +# 0 represents red, 60 is yellow, 120 is green, 180 is cyan, 240 is blue, 300 +# purple, and 360 is red again. +# Minimum value: 0, maximum value: 359, default value: 220. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_COLORSTYLE_HUE = 220 + +# The HTML_COLORSTYLE_SAT tag controls the purity (or saturation) of the colors +# in the HTML output. For a value of 0 the output will use gray-scales only. A +# value of 255 will produce the most vivid colors. +# Minimum value: 0, maximum value: 255, default value: 100. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_COLORSTYLE_SAT = 100 + +# The HTML_COLORSTYLE_GAMMA tag controls the gamma correction applied to the +# luminance component of the colors in the HTML output. Values below 100 +# gradually make the output lighter, whereas values above 100 make the output +# darker. The value divided by 100 is the actual gamma applied, so 80 represents +# a gamma of 0.8, The value 220 represents a gamma of 2.2, and 100 does not +# change the gamma. +# Minimum value: 40, maximum value: 240, default value: 80. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_COLORSTYLE_GAMMA = 80 + +# If the HTML_TIMESTAMP tag is set to YES then the footer of each generated HTML +# page will contain the date and time when the page was generated. Setting this +# to YES can help to show when doxygen was last run and thus if the +# documentation is up to date. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_TIMESTAMP = NO + +# If the HTML_DYNAMIC_MENUS tag is set to YES then the generated HTML +# documentation will contain a main index with vertical navigation menus that +# are dynamically created via JavaScript. If disabled, the navigation index will +# consists of multiple levels of tabs that are statically embedded in every HTML +# page. Disable this option to support browsers that do not have JavaScript, +# like the Qt help browser. +# The default value is: YES. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_DYNAMIC_MENUS = YES + +# If the HTML_DYNAMIC_SECTIONS tag is set to YES then the generated HTML +# documentation will contain sections that can be hidden and shown after the +# page has loaded. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_DYNAMIC_SECTIONS = YES + +# With HTML_INDEX_NUM_ENTRIES one can control the preferred number of entries +# shown in the various tree structured indices initially; the user can expand +# and collapse entries dynamically later on. Doxygen will expand the tree to +# such a level that at most the specified number of entries are visible (unless +# a fully collapsed tree already exceeds this amount). So setting the number of +# entries 1 will produce a full collapsed tree by default. 0 is a special value +# representing an infinite number of entries and will result in a full expanded +# tree by default. +# Minimum value: 0, maximum value: 9999, default value: 100. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_INDEX_NUM_ENTRIES = 100 + +# If the GENERATE_DOCSET tag is set to YES, additional index files will be +# generated that can be used as input for Apple's Xcode 3 integrated development +# environment (see: +# https://developer.apple.com/xcode/), introduced with OSX 10.5 (Leopard). To +# create a documentation set, doxygen will generate a Makefile in the HTML +# output directory. Running make will produce the docset in that directory and +# running make install will install the docset in +# ~/Library/Developer/Shared/Documentation/DocSets so that Xcode will find it at +# startup. See https://developer.apple.com/library/archive/featuredarticles/Doxy +# genXcode/_index.html for more information. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +GENERATE_DOCSET = NO + +# This tag determines the name of the docset feed. A documentation feed provides +# an umbrella under which multiple documentation sets from a single provider +# (such as a company or product suite) can be grouped. +# The default value is: Doxygen generated docs. +# This tag requires that the tag GENERATE_DOCSET is set to YES. + +DOCSET_FEEDNAME = "Doxygen generated docs" + +# This tag determines the URL of the docset feed. A documentation feed provides +# an umbrella under which multiple documentation sets from a single provider +# (such as a company or product suite) can be grouped. +# This tag requires that the tag GENERATE_DOCSET is set to YES. + +DOCSET_FEEDURL = + +# This tag specifies a string that should uniquely identify the documentation +# set bundle. This should be a reverse domain-name style string, e.g. +# com.mycompany.MyDocSet. Doxygen will append .docset to the name. +# The default value is: org.doxygen.Project. +# This tag requires that the tag GENERATE_DOCSET is set to YES. + +DOCSET_BUNDLE_ID = org.doxygen.Project + +# The DOCSET_PUBLISHER_ID tag specifies a string that should uniquely identify +# the documentation publisher. This should be a reverse domain-name style +# string, e.g. com.mycompany.MyDocSet.documentation. +# The default value is: org.doxygen.Publisher. +# This tag requires that the tag GENERATE_DOCSET is set to YES. + +DOCSET_PUBLISHER_ID = org.doxygen.Publisher + +# The DOCSET_PUBLISHER_NAME tag identifies the documentation publisher. +# The default value is: Publisher. +# This tag requires that the tag GENERATE_DOCSET is set to YES. + +DOCSET_PUBLISHER_NAME = Publisher + +# If the GENERATE_HTMLHELP tag is set to YES then doxygen generates three +# additional HTML index files: index.hhp, index.hhc, and index.hhk. The +# index.hhp is a project file that can be read by Microsoft's HTML Help Workshop +# on Windows. In the beginning of 2021 Microsoft took the original page, with +# a.o. the download links, offline the HTML help workshop was already many years +# in maintenance mode). You can download the HTML help workshop from the web +# archives at Installation executable (see: +# http://web.archive.org/web/20160201063255/http://download.microsoft.com/downlo +# ad/0/A/9/0A939EF6-E31C-430F-A3DF-DFAE7960D564/htmlhelp.exe). +# +# The HTML Help Workshop contains a compiler that can convert all HTML output +# generated by doxygen into a single compiled HTML file (.chm). Compiled HTML +# files are now used as the Windows 98 help format, and will replace the old +# Windows help format (.hlp) on all Windows platforms in the future. Compressed +# HTML files also contain an index, a table of contents, and you can search for +# words in the documentation. The HTML workshop also contains a viewer for +# compressed HTML files. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +GENERATE_HTMLHELP = NO + +# The CHM_FILE tag can be used to specify the file name of the resulting .chm +# file. You can add a path in front of the file if the result should not be +# written to the html output directory. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +CHM_FILE = + +# The HHC_LOCATION tag can be used to specify the location (absolute path +# including file name) of the HTML help compiler (hhc.exe). If non-empty, +# doxygen will try to run the HTML help compiler on the generated index.hhp. +# The file has to be specified with full path. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +HHC_LOCATION = + +# The GENERATE_CHI flag controls if a separate .chi index file is generated +# (YES) or that it should be included in the main .chm file (NO). +# The default value is: NO. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +GENERATE_CHI = NO + +# The CHM_INDEX_ENCODING is used to encode HtmlHelp index (hhk), content (hhc) +# and project file content. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +CHM_INDEX_ENCODING = + +# The BINARY_TOC flag controls whether a binary table of contents is generated +# (YES) or a normal table of contents (NO) in the .chm file. Furthermore it +# enables the Previous and Next buttons. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +BINARY_TOC = NO + +# The TOC_EXPAND flag can be set to YES to add extra items for group members to +# the table of contents of the HTML help documentation and to the tree view. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +TOC_EXPAND = NO + +# If the GENERATE_QHP tag is set to YES and both QHP_NAMESPACE and +# QHP_VIRTUAL_FOLDER are set, an additional index file will be generated that +# can be used as input for Qt's qhelpgenerator to generate a Qt Compressed Help +# (.qch) of the generated HTML documentation. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +GENERATE_QHP = NO + +# If the QHG_LOCATION tag is specified, the QCH_FILE tag can be used to specify +# the file name of the resulting .qch file. The path specified is relative to +# the HTML output folder. +# This tag requires that the tag GENERATE_QHP is set to YES. + +QCH_FILE = + +# The QHP_NAMESPACE tag specifies the namespace to use when generating Qt Help +# Project output. For more information please see Qt Help Project / Namespace +# (see: +# https://doc.qt.io/archives/qt-4.8/qthelpproject.html#namespace). +# The default value is: org.doxygen.Project. +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_NAMESPACE = org.doxygen.Project + +# The QHP_VIRTUAL_FOLDER tag specifies the namespace to use when generating Qt +# Help Project output. For more information please see Qt Help Project / Virtual +# Folders (see: +# https://doc.qt.io/archives/qt-4.8/qthelpproject.html#virtual-folders). +# The default value is: doc. +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_VIRTUAL_FOLDER = doc + +# If the QHP_CUST_FILTER_NAME tag is set, it specifies the name of a custom +# filter to add. For more information please see Qt Help Project / Custom +# Filters (see: +# https://doc.qt.io/archives/qt-4.8/qthelpproject.html#custom-filters). +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_CUST_FILTER_NAME = + +# The QHP_CUST_FILTER_ATTRS tag specifies the list of the attributes of the +# custom filter to add. For more information please see Qt Help Project / Custom +# Filters (see: +# https://doc.qt.io/archives/qt-4.8/qthelpproject.html#custom-filters). +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_CUST_FILTER_ATTRS = + +# The QHP_SECT_FILTER_ATTRS tag specifies the list of the attributes this +# project's filter section matches. Qt Help Project / Filter Attributes (see: +# https://doc.qt.io/archives/qt-4.8/qthelpproject.html#filter-attributes). +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_SECT_FILTER_ATTRS = + +# The QHG_LOCATION tag can be used to specify the location (absolute path +# including file name) of Qt's qhelpgenerator. If non-empty doxygen will try to +# run qhelpgenerator on the generated .qhp file. +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHG_LOCATION = + +# If the GENERATE_ECLIPSEHELP tag is set to YES, additional index files will be +# generated, together with the HTML files, they form an Eclipse help plugin. To +# install this plugin and make it available under the help contents menu in +# Eclipse, the contents of the directory containing the HTML and XML files needs +# to be copied into the plugins directory of eclipse. The name of the directory +# within the plugins directory should be the same as the ECLIPSE_DOC_ID value. +# After copying Eclipse needs to be restarted before the help appears. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +GENERATE_ECLIPSEHELP = NO + +# A unique identifier for the Eclipse help plugin. When installing the plugin +# the directory name containing the HTML and XML files should also have this +# name. Each documentation set should have its own identifier. +# The default value is: org.doxygen.Project. +# This tag requires that the tag GENERATE_ECLIPSEHELP is set to YES. + +ECLIPSE_DOC_ID = org.doxygen.Project + +# If you want full control over the layout of the generated HTML pages it might +# be necessary to disable the index and replace it with your own. The +# DISABLE_INDEX tag can be used to turn on/off the condensed index (tabs) at top +# of each HTML page. A value of NO enables the index and the value YES disables +# it. Since the tabs in the index contain the same information as the navigation +# tree, you can set this option to YES if you also set GENERATE_TREEVIEW to YES. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +DISABLE_INDEX = NO + +# The GENERATE_TREEVIEW tag is used to specify whether a tree-like index +# structure should be generated to display hierarchical information. If the tag +# value is set to YES, a side panel will be generated containing a tree-like +# index structure (just like the one that is generated for HTML Help). For this +# to work a browser that supports JavaScript, DHTML, CSS and frames is required +# (i.e. any modern browser). Windows users are probably better off using the +# HTML help feature. Via custom style sheets (see HTML_EXTRA_STYLESHEET) one can +# further fine tune the look of the index (see "Fine-tuning the output"). As an +# example, the default style sheet generated by doxygen has an example that +# shows how to put an image at the root of the tree instead of the PROJECT_NAME. +# Since the tree basically has the same information as the tab index, you could +# consider setting DISABLE_INDEX to YES when enabling this option. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +GENERATE_TREEVIEW = YES + +# When both GENERATE_TREEVIEW and DISABLE_INDEX are set to YES, then the +# FULL_SIDEBAR option determines if the side bar is limited to only the treeview +# area (value NO) or if it should extend to the full height of the window (value +# YES). Setting this to YES gives a layout similar to +# https://docs.readthedocs.io with more room for contents, but less room for the +# project logo, title, and description. If either GENERATE_TREEVIEW or +# DISABLE_INDEX is set to NO, this option has no effect. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +FULL_SIDEBAR = NO + +# The ENUM_VALUES_PER_LINE tag can be used to set the number of enum values that +# doxygen will group on one line in the generated HTML documentation. +# +# Note that a value of 0 will completely suppress the enum values from appearing +# in the overview section. +# Minimum value: 0, maximum value: 20, default value: 4. +# This tag requires that the tag GENERATE_HTML is set to YES. + +ENUM_VALUES_PER_LINE = 4 + +# If the treeview is enabled (see GENERATE_TREEVIEW) then this tag can be used +# to set the initial width (in pixels) of the frame in which the tree is shown. +# Minimum value: 0, maximum value: 1500, default value: 250. +# This tag requires that the tag GENERATE_HTML is set to YES. + +TREEVIEW_WIDTH = 250 + +# If the EXT_LINKS_IN_WINDOW option is set to YES, doxygen will open links to +# external symbols imported via tag files in a separate window. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +EXT_LINKS_IN_WINDOW = NO + +# If the OBFUSCATE_EMAILS tag is set to YES, doxygen will obfuscate email +# addresses. +# The default value is: YES. +# This tag requires that the tag GENERATE_HTML is set to YES. + +OBFUSCATE_EMAILS = YES + +# If the HTML_FORMULA_FORMAT option is set to svg, doxygen will use the pdf2svg +# tool (see https://github.com/dawbarton/pdf2svg) or inkscape (see +# https://inkscape.org) to generate formulas as SVG images instead of PNGs for +# the HTML output. These images will generally look nicer at scaled resolutions. +# Possible values are: png (the default) and svg (looks nicer but requires the +# pdf2svg or inkscape tool). +# The default value is: png. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_FORMULA_FORMAT = png + +# Use this tag to change the font size of LaTeX formulas included as images in +# the HTML documentation. When you change the font size after a successful +# doxygen run you need to manually remove any form_*.png images from the HTML +# output directory to force them to be regenerated. +# Minimum value: 8, maximum value: 50, default value: 10. +# This tag requires that the tag GENERATE_HTML is set to YES. + +FORMULA_FONTSIZE = 10 + +# The FORMULA_MACROFILE can contain LaTeX \newcommand and \renewcommand commands +# to create new LaTeX commands to be used in formulas as building blocks. See +# the section "Including formulas" for details. + +FORMULA_MACROFILE = + +# Enable the USE_MATHJAX option to render LaTeX formulas using MathJax (see +# https://www.mathjax.org) which uses client side JavaScript for the rendering +# instead of using pre-rendered bitmaps. Use this if you do not have LaTeX +# installed or if you want to formulas look prettier in the HTML output. When +# enabled you may also need to install MathJax separately and configure the path +# to it using the MATHJAX_RELPATH option. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +USE_MATHJAX = YES + +# With MATHJAX_VERSION it is possible to specify the MathJax version to be used. +# Note that the different versions of MathJax have different requirements with +# regards to the different settings, so it is possible that also other MathJax +# settings have to be changed when switching between the different MathJax +# versions. +# Possible values are: MathJax_2 and MathJax_3. +# The default value is: MathJax_2. +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_VERSION = MathJax_2 + +# When MathJax is enabled you can set the default output format to be used for +# the MathJax output. For more details about the output format see MathJax +# version 2 (see: +# http://docs.mathjax.org/en/v2.7-latest/output.html) and MathJax version 3 +# (see: +# http://docs.mathjax.org/en/latest/web/components/output.html). +# Possible values are: HTML-CSS (which is slower, but has the best +# compatibility. This is the name for Mathjax version 2, for MathJax version 3 +# this will be translated into chtml), NativeMML (i.e. MathML. Only supported +# for NathJax 2. For MathJax version 3 chtml will be used instead.), chtml (This +# is the name for Mathjax version 3, for MathJax version 2 this will be +# translated into HTML-CSS) and SVG. +# The default value is: HTML-CSS. +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_FORMAT = HTML-CSS + +# When MathJax is enabled you need to specify the location relative to the HTML +# output directory using the MATHJAX_RELPATH option. The destination directory +# should contain the MathJax.js script. For instance, if the mathjax directory +# is located at the same level as the HTML output directory, then +# MATHJAX_RELPATH should be ../mathjax. The default value points to the MathJax +# Content Delivery Network so you can quickly see the result without installing +# MathJax. However, it is strongly recommended to install a local copy of +# MathJax from https://www.mathjax.org before deployment. The default value is: +# - in case of MathJax version 2: https://cdn.jsdelivr.net/npm/mathjax@2 +# - in case of MathJax version 3: https://cdn.jsdelivr.net/npm/mathjax@3 +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_RELPATH = + +# The MATHJAX_EXTENSIONS tag can be used to specify one or more MathJax +# extension names that should be enabled during MathJax rendering. For example +# for MathJax version 2 (see +# https://docs.mathjax.org/en/v2.7-latest/tex.html#tex-and-latex-extensions): +# MATHJAX_EXTENSIONS = TeX/AMSmath TeX/AMSsymbols +# For example for MathJax version 3 (see +# http://docs.mathjax.org/en/latest/input/tex/extensions/index.html): +# MATHJAX_EXTENSIONS = ams +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_EXTENSIONS = + +# The MATHJAX_CODEFILE tag can be used to specify a file with javascript pieces +# of code that will be used on startup of the MathJax code. See the MathJax site +# (see: +# http://docs.mathjax.org/en/v2.7-latest/output.html) for more details. For an +# example see the documentation. +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_CODEFILE = + +# When the SEARCHENGINE tag is enabled doxygen will generate a search box for +# the HTML output. The underlying search engine uses javascript and DHTML and +# should work on any modern browser. Note that when using HTML help +# (GENERATE_HTMLHELP), Qt help (GENERATE_QHP), or docsets (GENERATE_DOCSET) +# there is already a search function so this one should typically be disabled. +# For large projects the javascript based search engine can be slow, then +# enabling SERVER_BASED_SEARCH may provide a better solution. It is possible to +# search using the keyboard; to jump to the search box use + S +# (what the is depends on the OS and browser, but it is typically +# , /