From fe501d243c0413db8ae85bda174d0761da00d330 Mon Sep 17 00:00:00 2001
From: Michael Lowell Roberts <mirobert@microsoft.com>
Date: Mon, 13 Jul 2015 10:40:35 -0700
Subject: [IronDafny] implemented workaround for "import opened" bug(s).

---
 Test/irondafny0/FIFO.dfy                     |  2 +-
 Test/irondafny0/LIFO.dfy                     |  2 +-
 Test/irondafny0/opened_workaround.dfy        | 21 +++++++++++++++++++++
 Test/irondafny0/opened_workaround.dfy.expect |  3 +++
 Test/irondafny0/xrefine0.dfy                 |  2 +-
 Test/irondafny0/xrefine1.dfy                 |  2 +-
 Test/irondafny0/xrefine2.dfy                 |  2 +-
 Test/irondafny0/xrefine3.dfy                 |  2 +-
 8 files changed, 30 insertions(+), 6 deletions(-)
 create mode 100644 Test/irondafny0/opened_workaround.dfy
 create mode 100644 Test/irondafny0/opened_workaround.dfy.expect

(limited to 'Test/irondafny0')

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 {
-- 
cgit v1.2.3