blob: bd57329f8ceb421e251710939a6d518023089dd3 (
plain)
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
29
30
31
32
33
34
35
36
|
var g: bool;
procedure {:inline 1} bar() returns (l: bool)
{
l := g;
}
procedure A1()
modifies g;
{
g := true;
assert |{ var l: bool; A: call l := bar(); return l; }|;
assert (exists p: bool :: |{ var l: bool; A: call l := bar(); return l; }|);
assert (forall p: bool :: |{ var l: bool; A: call l := bar(); return l; }|);
}
procedure A2()
{
assert |{ var l: bool; A: assume g; call l := bar(); return l; }|;
assert g ==> |{ var l: bool; A: call l := bar(); return l; }|;
assert (exists p: bool :: g ==> |{ var l: bool; A: call l := bar(); return l; }|);
assert (forall p: bool :: g ==> |{ var l: bool; A: call l := bar(); return l; }|);
}
procedure A3()
{
assume |{ var l: bool; A: call l := bar(); return l; }|;
assert |{ var l: bool; A: call l := bar(); return l; }|;
}
procedure A4()
modifies g;
{
g := true;
assert |{ var l: bool; A: call l := bar(); return !l; }|;
}
|