diff options
| author |  Mike Barnett <mbarnett@microsoft.com> | 2011-11-10 15:43:33 -0800 |
|---|---|---|
| committer | Mike Barnett <mbarnett@microsoft.com> | 2011-11-10 15:43:33 -0800 |
| commit | 277d5007f1b5d6988014d758e7ca1a486e1c6395 (patch) | |
| tree | 0e01d31f349903b0bc7ea714d527572c7c056fd3 /Test/datatypes | |
| parent | 4b18a65874f9e8d4c7ea042f22f7b57c512c6c71 (diff) | |
Many, many bug fixes related to generics and some other random problems.
Diffstat (limited to 'Test/datatypes')
| -rw-r--r-- | Test/datatypes/t2.bpl | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/Test/datatypes/t2.bpl b/Test/datatypes/t2.bpl index 2bca4e83..f794b227 100644 --- a/Test/datatypes/t2.bpl +++ b/Test/datatypes/t2.bpl @@ -38,6 +38,7 @@ axiom (forall u : DotNetType :: $Subtype(D(u), GenericType1(u))); function {:constructor} GenericType2(T:DotNetType, U:DotNetType) : DotNetType;
axiom (forall t : DotNetType, u : DotNetType :: $Subtype(GenericType2(t,u), System.Object()));
+
procedure foo(t : DotNetType)
{
assert System.Object() != GenericType1(t);
@@ -52,3 +53,10 @@ procedure bar(t : DotNetType, u : DotNetType) assert GenericType1(t) != GenericType1(u);
}
+function IntToType(x : int) : DotNetType;
+procedure baz(i : int)
+{
+ var t : DotNetType;
+ t := IntToType(i);
+ assert T#GenericType1(t) == System.Object();
+}
\ No newline at end of file |