diff options
Diffstat (limited to 'Test/datatypes/t2.bpl')
| -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 |