blob: d4741720e113e4b9b3af513a63e20ffb9b05bd91 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
function {:existential true} b1(x:bool, y:bool): bool;
function {:existential true} {:absdomain "Intervals"} b3(x:int): bool;
var g: int;
procedure main()
modifies g;
{
g := 0;
if(*) { g := 5; }
call foo();
}
procedure foo()
modifies g;
requires b1(g == 0, g == 5);
ensures b3(g);
{
assume g != 5;
}
|