diff options
| author |  Mike Barnett <mbarnett@microsoft.com> | 2011-10-30 11:44:48 -0700 |
|---|---|---|
| committer | Mike Barnett <mbarnett@microsoft.com> | 2011-10-30 11:44:48 -0700 |
| commit | 2901a36002b6b7ed31e925525e3eab1f63aaa848 (patch) | |
| tree | 841f2dff7145225989be08eaa696f27d6e5f9c3b | |
| parent | 937f5d2cbbf55ae5be84441b882b7a9d318d7dc8 (diff) | |
Removed prover option from runtest.bat because smtlib is now the default
in Boogie.
Added a test file for our encoding of .NET types in Boogie.
| -rw-r--r-- | Test/datatypes/runtest.bat | 2 | ||||
| -rw-r--r-- | Test/datatypes/t2.bpl | 36 |
2 files changed, 37 insertions, 1 deletions
diff --git a/Test/datatypes/runtest.bat b/Test/datatypes/runtest.bat index 7c605ae6..e796c905 100644 --- a/Test/datatypes/runtest.bat +++ b/Test/datatypes/runtest.bat @@ -7,6 +7,6 @@ set BPLEXE=%BOOGIEDIR%\Boogie.exe for %%f in (t1.bpl) do (
echo.
echo -------------------- %%f --------------------
- %BPLEXE% %* /prover:smtlib /typeEncoding:m %%f
+ %BPLEXE% %* /typeEncoding:m %%f
)
diff --git a/Test/datatypes/t2.bpl b/Test/datatypes/t2.bpl new file mode 100644 index 00000000..26ffd337 --- /dev/null +++ b/Test/datatypes/t2.bpl @@ -0,0 +1,36 @@ +
+type {:datatype} DotNetType;
+
+// class System.Object { ... }
+function {:constructor} System.Object() : DotNetType;
+
+// class NominalType2 : System.Object { ... }
+function {:constructor} NominalType2() : DotNetType;
+axiom $Subtype(NominalType2(), System.Object());
+
+// class GenericType1<T> : System.Object { ... }
+function {:constructor} GenericType1(T:DotNetType) : DotNetType;
+axiom (forall t : DotNetType :: $Subtype(GenericType1(t), System.Object()));
+
+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));
+
+procedure foo(t : DotNetType)
+{
+ assert System.Object() != GenericType1(t);
+ assert System.Object() != NominalType2();
+}
+
+procedure bar(t : DotNetType, u : DotNetType)
+ requires t != u;
+{
+ assert System.Object() != GenericType1(t);
+ assert System.Object() != NominalType2();
+ assert GenericType1(t) != GenericType1(u);
+}
+
|