Fix: Opaque functions with frame condition supported as follow-up of #…

…3779

Source/DafnyCore/Verifier/Translator.cs

@@ -4010,6 +4010,11 @@ void AddFrameAxiom(Function f) {
       // This is the general case
       Bpl.Expr prevH = null;
       Bpl.BoundVariable prevHVar = null;
+      Bpl.Expr reveal = null;
+      Bpl.BoundVariable revealVar = null;
+      if (f.IsOpaque) {
+        revealVar = BplBoundVar("$reveal", Bpl.Type.Bool, out reveal);
+      }
       if (f is TwoStateFunction) {
         // The previous-heap argument is the same for both function arguments.  That is,
         // the frame axiom says nothing about functions invoked with different previous heaps.
@@ -4050,6 +4055,11 @@ void AddFrameAxiom(Function f) {
         f0args.Add(s); f1args.Add(s);  // but don't add to f0argsCanCall or f1argsCanCall
       }
 
+      if (reveal != null) {
+        bvars.Add(revealVar);
+        f0args.Add(reveal); f1args.Add(reveal);
+      }
+
       if (prevH != null) {
         bvars.Add(prevHVar);
         f0args.Add(prevH); f1args.Add(prevH); f0argsCanCall.Add(prevH); f1argsCanCall.Add(prevH);

Test/git-issues/git-issue-3955.dfy

@@ -16,4 +16,14 @@ datatype B = B(
   {
     a.Valid()
   }
+}
+
+class C {
+  var a: A
+  constructor()
+  opaque twostate predicate Valid()
+    reads this`a, a
+  {
+    a.Valid() && old(a.Valid())
+  }
 }

Test/git-issues/git-issue-3955.dfy.expect

@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with TODO verified, TODO errors
+Dafny program verifier finished with 3 verified, 0 errors

docs/dev/news/3955.fix

@@ -0,0 +1 @@
+Opaque functions with frame condition supported as follow-up of #3779