diff options
| author |  leino <unknown> | 2015-11-11 17:36:24 -0800 |
|---|---|---|
| committer | leino <unknown> | 2015-11-11 17:36:24 -0800 |
| commit | 7cc9a11d13a1d43d6e7beb4f874bb086f73804c4 (patch) | |
| tree | 2a1053b087323964ccb7505d983806045da778b0 /Test/dafny0 | |
| parent | 3a5f8c7e20671a8e4eb706239b8d071f98846bf1 (diff) | |
Fixed compilation of equality between reference types
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/Compilation.dfy | 55 | ||||
| -rw-r--r-- | Test/dafny0/Compilation.dfy.expect | 6 |
2 files changed, 59 insertions, 2 deletions
diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy index 7f9169da..965f0787 100644 --- a/Test/dafny0/Compilation.dfy +++ b/Test/dafny0/Compilation.dfy @@ -45,7 +45,7 @@ module CoRecursion { // 42
// 9
// 9
- method Main() {
+ method TestMain() {
var m := 17;
var cell := new Cell;
cell.data := 40;
@@ -260,3 +260,56 @@ class DigitUnderscore_Names { this.10 := 20;
}
}
+
+// ------------------------------------------------------------------
+
+method Main()
+{
+ CoRecursion.TestMain();
+ EqualityTests.TestMain();
+}
+
+// ------------------------------------------------------------------
+
+module EqualityTests {
+ class C<T> {
+ }
+
+ method TestMain()
+ {
+ // regression tests:
+ var a: C<int>, b: C<int> := null, null;
+ if a == null {
+ print "a is null\n";
+ }
+ if a != null {
+ print "a is not null\n";
+ }
+ if a == b {
+ print "a and b are equal\n";
+ }
+ if a != b {
+ print "a and b are not equal\n";
+ }
+
+ var H := new real[10];
+ ArrayTests(H);
+ }
+
+ method ArrayTests<T>(H: array<T>)
+ {
+ var G := new int[10];
+ if G == H { // this comparison is allowed in Dafny, but requires a cast in C#
+ print "this would be highly suspicious\n";
+ }
+ if G != H { // this comparison is allowed in Dafny, but requires a cast in C#
+ print "good world order\n";
+ }
+ if null == H {
+ print "given array is null\n";
+ }
+ if null != H {
+ print "given array is non-null\n";
+ }
+ }
+}
diff --git a/Test/dafny0/Compilation.dfy.expect b/Test/dafny0/Compilation.dfy.expect index 2b76b107..0a934a63 100644 --- a/Test/dafny0/Compilation.dfy.expect +++ b/Test/dafny0/Compilation.dfy.expect @@ -1,5 +1,5 @@ -Dafny program verifier finished with 50 verified, 0 errors
+Dafny program verifier finished with 56 verified, 0 errors
Program compiled successfully
Running...
@@ -10,3 +10,7 @@ Running... 42 9 9 +a is null +a and b are equal +good world order +given array is non-null |