blob: fac91dc8fb2bcea2301e800df5936976cba1d2e1 (
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
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
|
// RUN: %boogie -noVerify "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
type double;
function R(int) returns (bool);
function K(double, bool) returns (bool);
var y: int where R(y);
var g: int where h ==> g == 12;
var h: bool where g < 100;
var k: double where K(k, h);
procedure P(x: int where x > 0) returns (y: int where y < 0);
requires x < 100;
modifies g;
ensures -100 < y;
implementation P(xx: int) returns (yy: int)
{
var a: int where a == 10;
var b: int where a == b && b < g;
start:
a := xx;
call b := P(a);
yy := b;
return;
}
procedure Q(w: int where x < w || x > alpha/*error: out-parameter alpha is not in scope*/, x: int where x + w > 0)
returns (v: bool where v,
y: int where x + y + z < 0,
z: int where g == 12,
alpha: ref where old(alpha) != null, // error: cannot use old in where clause
beta: ref where (forall r: ref :: r == beta ==> beta == null))
requires x < 100;
modifies g;
ensures -100 < y;
{
var a: int;
var b: int;
start:
a := x;
call b := P(a);
y := b;
return;
}
const SomeConstant: ref;
procedure Cnst(n: ref where n != SomeConstant) returns (SomeConstant: int)
{
var m: ref where m != SomeConstant;
var k: int where k != SomeConstant;
var r: ref where (forall abc: ref :: abc == SomeConstant);
var b: bool;
start:
b := (forall l: ref :: l == SomeConstant);
return;
}
type ref;
const null : ref;
|
