blob: 35f7d48a938ee3391706fd743e7c0737b2f635e9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
type ref;
const A100INT4_name:int;
function Match(a:int, t:int) returns (int);
function Array(int, int, int) returns (bool);
axiom(forall a:int :: {Match(a, A100INT4_name)} Array(a, 4, 100));
const myNull: int;
var p: int;
procedure main()
modifies p;
ensures p!=myNull;
{
p:=myNull;
}
|