diff options
author | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 23:14:18 -0600 |
---|---|---|
committer | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 23:14:18 -0600 |
commit | d652155ae013f36a1ee17653a8e458baad2d9c2c (patch) | |
tree | 067d600fe3cd1723afc11682935f0123a1eab653 /Test/test21/EmptySetBug.bpl | |
parent | d7fc0deb2ca6d7ebee094b6ea5430d9b41f163ec (diff) |
Merging complete. Everything looks good *crosses fingers*
Diffstat (limited to 'Test/test21/EmptySetBug.bpl')
-rw-r--r-- | Test/test21/EmptySetBug.bpl | 72 |
1 files changed, 36 insertions, 36 deletions
diff --git a/Test/test21/EmptySetBug.bpl b/Test/test21/EmptySetBug.bpl index e3feb16c..6c25ed95 100644 --- a/Test/test21/EmptySetBug.bpl +++ b/Test/test21/EmptySetBug.bpl @@ -1,36 +1,36 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
-// RUN: %diff "%s.n.expect" "%t"
-// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
-// RUN: %diff "%s.p.expect" "%t"
-// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
-// RUN: %diff "%s.a.expect" "%t"
-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
-}
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" +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 +} |