summaryrefslogtreecommitdiff
path: root/Test/irondafny0
diff options
context:
space:
mode:
Diffstat (limited to 'Test/irondafny0')
-rw-r--r--Test/irondafny0/FIFO.dfy2
-rw-r--r--Test/irondafny0/LIFO.dfy2
-rw-r--r--Test/irondafny0/opened_workaround.dfy21
-rw-r--r--Test/irondafny0/opened_workaround.dfy.expect3
-rw-r--r--Test/irondafny0/xrefine0.dfy2
-rw-r--r--Test/irondafny0/xrefine1.dfy2
-rw-r--r--Test/irondafny0/xrefine2.dfy2
-rw-r--r--Test/irondafny0/xrefine3.dfy2
8 files changed, 30 insertions, 6 deletions
diff --git a/Test/irondafny0/FIFO.dfy b/Test/irondafny0/FIFO.dfy
index 1256b55d..ded8f567 100644
--- a/Test/irondafny0/FIFO.dfy
+++ b/Test/irondafny0/FIFO.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
include "Queue.dfyi"
diff --git a/Test/irondafny0/LIFO.dfy b/Test/irondafny0/LIFO.dfy
index bac08fba..8c0a08e8 100644
--- a/Test/irondafny0/LIFO.dfy
+++ b/Test/irondafny0/LIFO.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
include "Queue.dfyi"
diff --git a/Test/irondafny0/opened_workaround.dfy b/Test/irondafny0/opened_workaround.dfy
new file mode 100644
index 00000000..7464c346
--- /dev/null
+++ b/Test/irondafny0/opened_workaround.dfy
@@ -0,0 +1,21 @@
+// RUN: %dafny /ironDafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module A {
+
+ predicate P()
+
+ class C
+ {
+ static method{:axiom} M()
+ ensures P();
+ }
+}
+
+abstract module B {
+ import opened A
+}
+
+abstract module C {
+ import Bee as B // Works
+}
diff --git a/Test/irondafny0/opened_workaround.dfy.expect b/Test/irondafny0/opened_workaround.dfy.expect
new file mode 100644
index 00000000..0be94b4c
--- /dev/null
+++ b/Test/irondafny0/opened_workaround.dfy.expect
@@ -0,0 +1,3 @@
+
+Dafny program verifier finished with 3 verified, 0 errors
+Compilation error: Function _0_A_Compile._default.P has no body
diff --git a/Test/irondafny0/xrefine0.dfy b/Test/irondafny0/xrefine0.dfy
index 35993ce8..b849111c 100644
--- a/Test/irondafny0/xrefine0.dfy
+++ b/Test/irondafny0/xrefine0.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /ironDafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
abstract module Delicious {}
diff --git a/Test/irondafny0/xrefine1.dfy b/Test/irondafny0/xrefine1.dfy
index 10d25f53..4b085e6b 100644
--- a/Test/irondafny0/xrefine1.dfy
+++ b/Test/irondafny0/xrefine1.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
abstract module ProtocolSpec {
diff --git a/Test/irondafny0/xrefine2.dfy b/Test/irondafny0/xrefine2.dfy
index 7578b424..1de4e201 100644
--- a/Test/irondafny0/xrefine2.dfy
+++ b/Test/irondafny0/xrefine2.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
abstract module ProtocolSpec {
diff --git a/Test/irondafny0/xrefine3.dfy b/Test/irondafny0/xrefine3.dfy
index 69c5bc27..44add7cc 100644
--- a/Test/irondafny0/xrefine3.dfy
+++ b/Test/irondafny0/xrefine3.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
abstract module AlphaSpec {