blob: 881a6222c8f57b1bd006e90209189c9370c16c11 (
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
|
// RUN: %boogie -noinfer %s > %t
// RUN: %diff %s.expect %t
// This file has been created to test some of the formula/term issues in Zap.
// However, the test harness does not specify any particular prover to be used,
// since these tests should pass regardless of which prover is used.
procedure P()
{
var a: int, b: int, t: bool;
start:
assume a == b;
t := a == b;
assert t;
return;
}
function f(bool) returns (int);
const A: int;
const B: int;
axiom f(A < B) == 5;
procedure Q()
{
start:
assume A < B;
assert f(true) == 5;
return;
}
// ----- and now some erroneous procedures
procedure PX()
{
var a: int, b: int, t: bool;
start:
assume a == b;
t := a == b;
assert !t; // error
return;
}
procedure QX()
{
start:
assume A < B;
assert f(true) < 2; // error
return;
}
|