1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
CORE
main.c
--enforce-contract foo --enforce-contract bar --enforce-contract baz _ --no-standard-checks
^EXIT=0$
^SIGNAL=0$
^\[bar.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
^\[baz.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
^\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
^\[bar.assigns.\d+\] line \d+ Check that p->y is assignable: SUCCESS$
^\[foo.assigns.\d+\] line \d+ Check that \*p->y is assignable: SUCCESS$
^\[foo.assigns.\d+\] line \d+ Check that z is assignable: SUCCESS$
^\[main.assertion.\d+\] line \d+ assertion \*\(p->y\) == 7: SUCCESS$
^\[main.assertion.\d+\] line \d+ assertion \*\(p->y\) == -1: SUCCESS$
^VERIFICATION SUCCESSFUL$
--
--
This test checks that history variables are supported for structs, symbols, and
struct members. By using the --enforce-contract flag, the postcondition
(with history variable) is asserted. In this case, this assertion should pass.
Note: A function is always authorized to assign the variables that store
its arguments, there is no need to mention them in the assigns clause.
|
