fixed problems with datatypes

removed stale contracts in stratified inlining
added test to datatypes

3 files changed, 33 insertions, 57 deletions

diff --git a/Test/datatypes/Answer b/Test/datatypes/Answer
new file mode 100644
index 00000000..7b7b411a
--- /dev/null
+++ b/Test/datatypes/Answer
@@ -0,0 +1,14 @@
+

+-------------------- t1.bpl --------------------

+t1.bpl(23,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    t1.bpl(16,3): anon0

+

+Boogie program verifier finished with 0 verified, 1 error

+

+-------------------- t2.bpl --------------------

+t2.bpl(23,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    t2.bpl(16,3): anon0

+

+Boogie program verifier finished with 0 verified, 1 error

diff --git a/Test/datatypes/runtest.bat b/Test/datatypes/runtest.bat
index e796c905..fe2aa09d 100644
--- a/Test/datatypes/runtest.bat
+++ b/Test/datatypes/runtest.bat
@@ -4,7 +4,7 @@ setlocal
 set BOOGIEDIR=..\..\Binaries

 set BPLEXE=%BOOGIEDIR%\Boogie.exe

 

-for %%f in (t1.bpl) do (

+for %%f in (t1.bpl t2.bpl) do (

   echo.

   echo -------------------- %%f --------------------

   %BPLEXE% %* /typeEncoding:m %%f

diff --git a/Test/datatypes/t2.bpl b/Test/datatypes/t2.bpl
index f794b227..d4d2bf3f 100644
--- a/Test/datatypes/t2.bpl
+++ b/Test/datatypes/t2.bpl
@@ -1,62 +1,24 @@
+type TT;

+type {:datatype} Tree;

+function {:constructor} leaf`0() : Tree;

+function {:constructor} node`2(value:TT, children:TreeList) : Tree;

 

-type {:datatype} DotNetType;

+type {:datatype} TreeList;

+function {:constructor} cons`2(car:Tree, cdr:TreeList) : TreeList;

+function {:constructor} nil`0() : TreeList;

 

-/*\

- *  Subtype Axioms

-\*/

-function $Subtype(DotNetType, DotNetType) : bool;

-// reflexive

-axiom (forall t: DotNetType :: $Subtype(t, t));

-// anti-symmetric

-axiom (forall t0: DotNetType, t1: DotNetType :: { $Subtype(t0, t1), $Subtype(t1, t0) } $Subtype(t0, t1) && $Subtype(t1, t0) ==> t0 == t1);

-// transitive

-axiom (forall t0: DotNetType, t1: DotNetType, t2: DotNetType :: { $Subtype(t0, t1), $Subtype(t1, t2) } $Subtype(t0, t1) && $Subtype(t1, t2) ==> $Subtype(t0, t2));

-

-/*\

- *  Type Declarations

-\*/

-// class System.Object { ... }

-function {:constructor} System.Object() : DotNetType;

-

-// class B : System.Object { ... }

-function {:constructor} B() : DotNetType;

-axiom $Subtype(B(), System.Object());

-

-// class GenericType1<T> : System.Object { ... }

-function {:constructor} GenericType1(T:DotNetType) : DotNetType;

-axiom (forall t : DotNetType :: $Subtype(GenericType1(t), System.Object()));

-

-// class C : GenericType1<object>

-function {:constructor} C() : DotNetType;

-axiom $Subtype(C(), GenericType1(System.Object()));

-

-// class D<U> : GenericType1<U>

-function {:constructor} D(U:DotNetType) : DotNetType;

-axiom (forall u : DotNetType :: $Subtype(D(u), GenericType1(u)));

-

-// class GenericType2<T,U> : System.Object { ... }

-function {:constructor} GenericType2(T:DotNetType, U:DotNetType) : DotNetType;

-axiom (forall t : DotNetType, u : DotNetType :: $Subtype(GenericType2(t,u), System.Object()));

-

-

-procedure foo(t : DotNetType) 

+procedure foo() 

 {

-  assert System.Object() != GenericType1(t);

-  assert System.Object() != B();

-}

+  var a: Tree;

+  var b: TreeList;

+  var x: TT;

 

-procedure bar(t : DotNetType, u : DotNetType) 

-  requires t != u;

-{

-  assert System.Object() != GenericType1(t);

-  assert System.Object() != B();

-  assert GenericType1(t) != GenericType1(u);

-}

+  assert value#node`2(node`2(x, nil`0())) == x;

+  assert children#node`2(node`2(x, nil`0())) == nil`0();

+  

+  assert (cons`2(leaf`0(), nil`0()) != nil`0());

 

-function IntToType(x : int) : DotNetType;

-procedure baz(i : int)

-{

-  var t : DotNetType;

-  t := IntToType(i);

-  assert T#GenericType1(t) == System.Object();

+  assert is#nil`0(nil`0());

+

+  assert is#node`2(leaf`0());

 }
\ No newline at end of file