Skip to content

Commit 3ebfca3

Browse files
committed
local_out_of_scope3 now works
1 parent 3c29377 commit 3ebfca3

File tree

2 files changed

+6
-4
lines changed

2 files changed

+6
-4
lines changed

regression/cprover/safety/local_out_of_scope3.c

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ int main()
44
__CPROVER_assume(__CPROVER_r_ok(p));
55
{
66
int x;
7+
__CPROVER_assert(p != &x, "property 1"); // passes
78
}
8-
__CPROVER_assert(__CPROVER_r_ok(p), "property 1");
9+
__CPROVER_assert(__CPROVER_r_ok(p), "property 2"); // passes
910
}
Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,8 @@
1-
KNOWNBUG
1+
CORE
22
local_out_of_scope3.c
33

4-
^EXIT=10$
4+
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main\.pointer\.1\] line \d+ pointer p safe: SUCCESS$
6+
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
7+
^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$
78
--

0 commit comments

Comments
 (0)