blob: 062b22ea3c95e90f317812c0bdce78df1a4a7ee1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
procedure {:checksum "-1"} Callee();
implementation {:id "Callee"} {:checksum "2"} Callee()
{
var r: int;
call r := Sum(42);
assert r != 0;
assert 42 <= r;
}
procedure {:checksum "1"} Sum(n: int) returns (r: int);
requires 0 <= n;
ensures n != 0 ==> 1 <= r;
|