1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
KNOWNBUG
main.c
--dfcc main --enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract baz
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
// bar
ASSERT \*x > 0
IF !\(\*x == 3\) THEN GOTO \d
tmp_if_expr = \*y == 5 \? true : false;
ASSUME tmp_if_expr
// baz
ASSUME \*z == 7
// foo
ASSUME \*tmp_cc\$\d > 0
ASSERT \*tmp_cc\$\d == 3
--
--
Verification:
This test checks support for an uninitialized pointer that is assigned to by
a function (bar and baz). Both functions bar and baz are being replaced by
their function contracts, while the calling function foo is being checked
(by enforcing it's function contracts).
Known Bug:
Currently, there is a known issue with __CPROVER_w_ok(ptr, 0) such that it
returns true if ptr is uninitialized. This is not the expected behavior,
therefore, the outcome of this test case is currently incorrect.
|
