Test/test21/EmptySetBug.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
29
30

type ref;

const null: ref;

type Set T = [T]bool;

function Set#Empty<T>() returns (Set T);

axiom (forall<T> o: T :: { Set#Empty()[o] } !Set#Empty()[o]);

function Set#Singleton<T>(T) returns (Set T);

axiom (forall<T> r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]);

axiom (forall<T> r: T, o: T :: { Set#Singleton(r)[o] } Set#Singleton(r)[o] <==> r == o);

function Set#UnionOne<T>(Set T, T) returns (Set T);

axiom (forall<T> a: Set T, x: T, o: T :: { Set#UnionOne(a, x)[o] } Set#UnionOne(a, x)[o] <==> o == x || a[o]);

procedure Test(this: ref)
{
  var s: Set ref;

  s := Set#UnionOne(Set#Empty(), this);
  assert s[this];
  assert !Set#Empty()[this];

  assert Set#Singleton(this)[null];         // should not be provable
}