Test/forro/prog0.forro


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

procedure a, b, c := P(x, y, z)
  requires 10
  ensures 20
do
  if 30 then else end;
  if 31 then else end;
  while x < z
    invariant x <= z
    invariant b.valid and 1
  do
    k := x + 1;
  end;
  (x+5).head := c.tail;
  a := new (17, 18);
  assert a != null;
  m := k + a + null;
  c := m;
  call Q(x, y, y);
  if x then
    call a, c, b := P(a, b, c);
  else
    call R();
  end;
end;


procedure Q(x, y, z)
  requires 10
  ensures 20
do
  if 40 then else end;
end;


procedure R()
  requires 10
  ensures 20
do
end;