blob: 8d8b215b591c61c6e2dcab536e8d027d4160f0cf (
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
|
method M(x: int)
{
assert x < 20 || 10 <= x; // always true
assert x < 10; // error
Other(x); // error: precondition violation
assert x == 7; // error: this is a new error in v1
}
method Other(y: int)
requires 0 <= y
{
}
method Posty() returns (z: int)
ensures 2 <= z // error: postcondition violation
{
var t := 20;
if t < z {
assert true; // this is a new assert
} else { // the postcondition violation occurs on this 'else' branch
}
}
method NoChangeWhazzoeva(u: int)
{
assert u != 53; // error
}
method NoChangeAndCorrect() { assert true; }
|
