Don't expand {:opaque} for inherited functions. (Note, more design is still needed to handle the combination of opaque and refinement well.)

3 files changed, 13 insertions, 4 deletions

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 3ed26d96..23d427d9 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -414,7 +414,7 @@ namespace Microsoft.Dafny
         if (member is Function) {

           var f = (Function)member;

 

-          if (Attributes.Contains(f.Attributes, "opaque")) {

+          if (Attributes.Contains(f.Attributes, "opaque") && !RefinementToken.IsInherited(f.tok, c.Module)) {

             // Create a copy, which will be the internal version with a full body

             // which will allow us to verify that the ensures are true

             var cloner = new Cloner();

@@ -485,7 +485,7 @@ namespace Microsoft.Dafny
             List<Attributes.Argument/*!*/> argList = new List<Attributes.Argument/*!*/>();

             Attributes lemma_attrs = new Attributes("axiom", argList, null);

 

-            var reveal = new Method(f.tok, "reveal_" + f.Name, f.IsStatic, true, f.TypeArgs, new List<Formal>(), new List<Formal>(), new List<MaybeFreeExpression>(),

+            var reveal = new Lemma(f.tok, "reveal_" + f.Name, f.IsStatic, f.TypeArgs, new List<Formal>(), new List<Formal>(), new List<MaybeFreeExpression>(),

                                     new Specification<FrameExpression>(new List<FrameExpression>(), null), newEnsuresList,

                                     new Specification<Expression>(new List<Expression>(), null), null, lemma_attrs, false);

             newDecls.Add(reveal);

@@ -516,7 +516,7 @@ namespace Microsoft.Dafny
 

           if (e.Function == context.original) { // Attempting to call the original opaque function

             // Redirect the call to the full version

-            e.Function = context.full;            

+            e.Function = context.full;

           }

         }

         return true;

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 569cb961..a1dd639f 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1793,7 +1793,7 @@ OpaqueFunctions.dfy(135,12): Error: assertion violation
 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 37 verified, 19 errors

+Dafny program verifier finished with 41 verified, 19 errors

 

 -------------------- Maps.dfy --------------------

 Maps.dfy(76,8): Error: element may not be in domain

diff --git a/Test/dafny0/OpaqueFunctions.dfy b/Test/dafny0/OpaqueFunctions.dfy
index 9879c66b..6bff4ef3 100644
--- a/Test/dafny0/OpaqueFunctions.dfy
+++ b/Test/dafny0/OpaqueFunctions.dfy
@@ -142,3 +142,12 @@ module OpaqueFunctionsAreNotInlined {
     assert F(x);

   }

 }

+

+// --------------------------------- opaque and refinement

+

+module M0 {

+  function {:opaque} F(): int

+  { 12 }

+}

+module M1 refines M0 {

+}