fix: Invalid declaration errors with /typeEncoding:m

Source/DafnyCore/Verifier/Translator.cs

@@ -4425,13 +4425,6 @@ void AddWellformednessCheck(Function f) {
         }
         Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcID, args);
 
-        DefineFrame(f.tok, f.Reads, bodyCheckBuilder
-                   , new List<Variable>() /* dummy local variable list, since frame axiom variable (and its definition)
-                                           * is already added. The only reason why we add the frame axiom definition
-                                           * again is to make boogie gives the same trace as before the change that
-                                           * makes reads clauses also guard the requires */
-                   , null);
-
         wfo = new WFOptions(null, true, true /* do delayed reads checks */);
         CheckWellformedWithResult(f.Body, wfo, funcAppl, f.ResultType, locals, bodyCheckBuilder, etran);
         if (f.Result != null) {

Test/dafny0/Fuel.dfy.expect

@@ -20,41 +20,41 @@ Fuel.dfy(324,21): Related location
 Fuel.dfy(313,41): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
-Fuel.dfy(314,93): Related location
+Fuel.dfy(314,46): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
 Fuel.dfy(312,58): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
-Fuel.dfy(314,72): Related location
+Fuel.dfy(312,43): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
-Fuel.dfy(314,46): Related location
+Fuel.dfy(314,72): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
-Fuel.dfy(312,43): Related location
+Fuel.dfy(314,93): Related location
 Fuel.dfy(335,49): Error: destructor 't' can only be applied to datatype values constructed by 'VTuple'
 Fuel.dfy(335,50): Error: index out of range
 Fuel.dfy(336,38): Error: index out of range
 Fuel.dfy(336,42): Error: destructor 'u' can only be applied to datatype values constructed by 'VUint64'
 Fuel.dfy(336,45): Error: function precondition could not be proved
 Fuel.dfy(329,21): Related location
-Fuel.dfy(312,43): Related location
+Fuel.dfy(311,43): Related location
 Fuel.dfy(336,45): Error: function precondition could not be proved
 Fuel.dfy(329,21): Related location
-Fuel.dfy(312,58): Related location
+Fuel.dfy(312,43): Related location
 Fuel.dfy(336,45): Error: function precondition could not be proved
 Fuel.dfy(329,21): Related location
 Fuel.dfy(314,93): Related location
 Fuel.dfy(336,45): Error: function precondition could not be proved
 Fuel.dfy(329,21): Related location
-Fuel.dfy(314,72): Related location
+Fuel.dfy(312,58): Related location
 Fuel.dfy(336,45): Error: function precondition could not be proved
 Fuel.dfy(329,21): Related location
-Fuel.dfy(311,43): Related location
+Fuel.dfy(313,41): Related location
 Fuel.dfy(336,45): Error: function precondition could not be proved
 Fuel.dfy(329,21): Related location
-Fuel.dfy(313,41): Related location
+Fuel.dfy(314,72): Related location
 Fuel.dfy(336,71): Error: index out of range
 Fuel.dfy(397,22): Error: assertion might not hold
 Fuel.dfy(398,22): Error: assertion might not hold

Test/dafny0/FunctionSpecifications.dfy

@@ -1,9 +1,9 @@
-// RUN: %exits-with 4 %dafny /compile:0 /deprecation:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %exits-with 4 %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 ghost function Fib(n: int): int
-  requires 0 <= n;
-  ensures 0 <= Fib(n);
+  requires 0 <= n
+  ensures 0 <= Fib(n)
 {
   if n < 2 then n else
   Fib(n-2) + Fib(n-1)
@@ -12,53 +12,61 @@ ghost function Fib(n: int): int
 datatype List = Nil | Cons(int, List)
 
 ghost function Sum(a: List): int
-  ensures 0 <= Sum(a);
+  ensures 0 <= Sum(a)
 {
   match a
   case Nil => 0
   case Cons(x, tail) => if x < 0 then 0 else Fib(x)
 }
 
 ghost function FibWithoutPost(n: int): int
-  requires 0 <= n;
+  requires 0 <= n
 {
   if n < 2 then n else
   FibWithoutPost(n-2) + FibWithoutPost(n-1)
 }
 
 ghost function SumBad(a: List): int
-  ensures 0 <= Sum(a);  // this is still okay, because this is calling the good Sum
-  ensures 0 <= SumBad(a);  // error: cannot prove postcondition
+  ensures 0 <= Sum(a)  // this is still okay, because this is calling the good Sum
+  ensures 0 <= SumBad(a)  // error: cannot prove postcondition
 {
   match a
   case Nil => 0
   case Cons(x, tail) => if x < 0 then 0 else FibWithoutPost(x)
 }
 
 ghost function FibWithExtraPost(n: int): int
-  ensures 2 <= n ==> 0 <= FibWithExtraPost(n-1); // This is fine, because the definition of the function is discovered via canCall
-  ensures 1 <= n ==> 0 <= FibWithExtraPost(n-1); // Error: In the current implementation of Dafny, one needs to actually call the
+  ensures 2 <= n ==> 0 <= FibWithExtraPost(n-1) // This is fine, because the definition of the function is discovered via canCall
+  ensures 1 <= n ==> 0 <= FibWithExtraPost(n-1) // Error: In the current implementation of Dafny, one needs to actually call the
                                                  // function in order to benefit from canCall.  This may be improved in the future.
-  ensures 0 <= FibWithExtraPost(n);
+  ensures 0 <= FibWithExtraPost(n)
 {
   if n < 0 then 0 else
   if n < 2 then n else
   FibWithExtraPost(n-2) + FibWithExtraPost(n-1)
 }
 
+ghost function GoodPost(n: int): int
+  requires 0 <= n
+  ensures 1 <= n ==> GoodPost(n-1) == GoodPost(n-1)
+  ensures GoodPost(2*n - n) == GoodPost(2*(n+5) - 10 - n)  // these are legal ways to denote the result value of the function
+{
+  assert 2*n - n == 2*(n+5) - 10 - n;
+  if n < 2 then n else
+  GoodPost(n-2) + GoodPost(n-1)
+}
+
 ghost function DivergentPost(n: int): int
-  requires 0 <= n;
-  ensures 1 <= n ==> DivergentPost(n-1) == DivergentPost(n-1);
-  ensures DivergentPost(2*n - n) == DivergentPost(2*(n+5) - 10 - n);  // these are legal ways to denote the result value of the function
-  ensures DivergentPost(n+1) == DivergentPost(n+1);  // error: call may not terminate
+  requires 0 <= n
+  ensures DivergentPost(n+1) == DivergentPost(n+1)  // error: call may not terminate
 {
   assert 2*n - n == 2*(n+5) - 10 - n;
   if n < 2 then n else
   DivergentPost(n-2) + DivergentPost(n-1)
 }
 
 ghost function HoldsAtLeastForZero(x: int): bool
-  ensures x == 0 ==> HoldsAtLeastForZero(x);
+  ensures x == 0 ==> HoldsAtLeastForZero(x)
 {
   x < -2  // error: this does not hold for 0
 }
@@ -67,7 +75,7 @@ ghost function HoldsAtLeastForZero(x: int): bool
 // ----- the subrange test (which they didn't always do).
 
 ghost function IncA(x: nat): nat
-  ensures x < IncA(x);
+  ensures x < IncA(x)
 {
   if x == 17 then
     18
@@ -87,7 +95,7 @@ ghost function IncB(i: nat): nat
 }
 
 ghost function IncC(i: nat): int
-  ensures IncC(i)>=0;
+  ensures IncC(i)>=0
 {
   var n :| n>i; n
 }
@@ -99,9 +107,9 @@ ghost function IncC(i: nat): int
 
 // Test basic function hiding
 ghost function {:opaque} secret(x:int, y:int) : int
-  requires 0 <= x < 5;
-  requires 0 <= y < 5;
-  ensures secret(x, y) < 10;
+  requires 0 <= x < 5
+  requires 0 <= y < 5
+  ensures secret(x, y) < 10
 { x + y }
 
 method test_secret()
@@ -115,7 +123,7 @@ method test_secret()
 // Check that opaque doesn't break recursion unrolling
 // Also checks that opaque functions that do terminate are verified as such
 ghost function {:opaque} recursive_f(x:int) : int
-  requires x >= 0;
+  requires x >= 0
 {
   if x == 0 then 0
   else 1 + recursive_f(x - 1)
@@ -134,22 +142,22 @@ method test_recursive_f()
 
 // Check that opaque doesn't interfere with ensures checking
 ghost function {:opaque} bad_ensures(x:int, y:int):int
-  requires x >= 0 && y >= 0;
-  ensures bad_ensures(x, y) > 0;
+  requires x >= 0 && y >= 0
+  ensures bad_ensures(x, y) > 0
 {
   x + y
 }
 
 // Check that opaque doesn't interfere with termination checking
 ghost function {:opaque} f(i:int):int
-  decreases i;
+  decreases i
 {
   f(i) + 1
 }
 
 // Try a sneakier (nested) version of the test above
 ghost function {:opaque} g(i:int):int
-  decreases i;
+  decreases i
 {
   h(i) + 1
 }

Test/dafny0/FunctionSpecifications.dfy.expect

@@ -2,17 +2,17 @@ FunctionSpecifications.dfy(35,24): Error: a postcondition could not be proved on
 FunctionSpecifications.dfy(31,12): Related location: this is the postcondition that could not be proved
 FunctionSpecifications.dfy(45,2): Error: a postcondition could not be proved on this return path
 FunctionSpecifications.dfy(40,23): Related location: this is the postcondition that could not be proved
-FunctionSpecifications.dfy(53,10): Error: cannot prove termination; try supplying a decreases clause
-FunctionSpecifications.dfy(60,15): Error: a postcondition could not be proved on this return path
-FunctionSpecifications.dfy(61,21): Related location: this is the postcondition that could not be proved
-FunctionSpecifications.dfy(109,22): Error: assertion might not hold
-FunctionSpecifications.dfy(112,22): Error: assertion might not hold
-FunctionSpecifications.dfy(127,26): Error: assertion might not hold
-FunctionSpecifications.dfy(131,26): Error: assertion might not hold
-FunctionSpecifications.dfy(136,25): Error: a postcondition could not be proved on this return path
-FunctionSpecifications.dfy(138,28): Related location: this is the postcondition that could not be proved
-FunctionSpecifications.dfy(147,2): Error: decreases clause might not decrease
-FunctionSpecifications.dfy(154,2): Error: decreases clause might not decrease
-FunctionSpecifications.dfy(159,2): Error: cannot prove termination; try supplying a decreases clause
+FunctionSpecifications.dfy(61,10): Error: cannot prove termination; try supplying a decreases clause
+FunctionSpecifications.dfy(68,15): Error: a postcondition could not be proved on this return path
+FunctionSpecifications.dfy(69,21): Related location: this is the postcondition that could not be proved
+FunctionSpecifications.dfy(117,22): Error: assertion might not hold
+FunctionSpecifications.dfy(120,22): Error: assertion might not hold
+FunctionSpecifications.dfy(135,26): Error: assertion might not hold
+FunctionSpecifications.dfy(139,26): Error: assertion might not hold
+FunctionSpecifications.dfy(144,25): Error: a postcondition could not be proved on this return path
+FunctionSpecifications.dfy(146,28): Related location: this is the postcondition that could not be proved
+FunctionSpecifications.dfy(155,2): Error: decreases clause might not decrease
+FunctionSpecifications.dfy(162,2): Error: decreases clause might not decrease
+FunctionSpecifications.dfy(167,2): Error: cannot prove termination; try supplying a decreases clause
 
-Dafny program verifier finished with 9 verified, 12 errors
+Dafny program verifier finished with 10 verified, 12 errors

docs/dev/news/inconsistent-ast-monomorphic.fix

@@ -0,0 +1 @@
+Fixes invalid declaration errors when verifying directly from Dafny using /typeEncoding:m.