diff options
| author |  Rustan Leino <unknown> | 2015-08-20 17:23:24 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2015-08-20 17:23:24 -0700 |
| commit | 566fdf1676e0d7d6060767febbfa7a0378300e99 (patch) | |
| tree | 48b9ddec4a84dd3242ebd39641f70a5d5cbd22c2 /Test/dafny0 | |
| parent | 270b34fc36dcfc781e8f49df5339cb2e10e69828 (diff) | |
Fixed compilation that involve enumeration over native-type newtype values.
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/RangeCompilation.dfy | 25 | ||||
| -rw-r--r-- | Test/dafny0/RangeCompilation.dfy.expect | 6 |
2 files changed, 31 insertions, 0 deletions
diff --git a/Test/dafny0/RangeCompilation.dfy b/Test/dafny0/RangeCompilation.dfy new file mode 100644 index 00000000..de8ca68e --- /dev/null +++ b/Test/dafny0/RangeCompilation.dfy @@ -0,0 +1,25 @@ +// RUN: %dafny /compile:3 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+newtype Byte = x | 0 <= x < 256
+predicate method GoodByte(b: Byte) {
+ b % 3 == 2
+}
+predicate method GoodInteger(i: int) {
+ i % 5 == 4
+}
+
+method Main() {
+ assert GoodByte(11) && GoodInteger(24);
+ var b: Byte :| GoodByte(b);
+ var i: int :| 0 <= i < 256 && GoodInteger(i);
+ print "b=", b, " i=", i, "\n";
+ var m0 := new MyClass;
+ var m17 := new M17.AnotherClass;
+}
+
+class MyClass { }
+
+module M17 {
+ class AnotherClass { }
+}
diff --git a/Test/dafny0/RangeCompilation.dfy.expect b/Test/dafny0/RangeCompilation.dfy.expect new file mode 100644 index 00000000..c3275d12 --- /dev/null +++ b/Test/dafny0/RangeCompilation.dfy.expect @@ -0,0 +1,6 @@ +
+Dafny program verifier finished with 5 verified, 0 errors
+Program compiled successfully
+Running...
+
+b=2 i=4 |