Test/test20/Prog1.bpl


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

// RUN: %boogie -noVerify "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// Let's test some Boogie 2 features ...

type elements;

type Field a;
var heap : <a> [ref, Field a] a;


procedure p (x:int, y:ref, z:<a> [ref, Field a] a) returns (newHeap : <a> [ref, Field a] a) {

  var f : Field int;
  var g : Field bool;

  var heap : <a> [ref, Field a] a;
  
  assert z[y, f] >= 0;
  assert z[x, f] >= 0;   // error: x has wrong type
  assert z[y, x] >= 0;   // error: x has wrong type
  assert z[y, g] >= 0;   // error: result of map select has wrong type

  heap[y, g] := false;

}

type ref;