diff options
| -rw-r--r-- | Source/Dafny/Translator.cs | 6 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 6 | ||||
| -rw-r--r-- | Test/dafny0/FunctionSpecifications.dfy | 6 |
3 files changed, 15 insertions, 3 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 1b8a23ee..c8cc11f6 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1605,8 +1605,10 @@ namespace Microsoft.Dafny { // check that postconditions hold
var ens = new Bpl.EnsuresSeq();
foreach (Expression p in f.Ens) {
- bool splitHappened; // we actually don't care
- foreach (var s in TrSplitExpr(p, etran, out splitHappened)) {
+ var functionHeight = currentModule.CallGraph.GetSCCRepresentativeId(f);
+ var splits = new List<SplitExprInfo>();
+ bool splitHappened/*we actually don't care*/ = TrSplitExpr(p, splits, true, functionHeight, etran);
+ foreach (var s in splits) {
if (!s.IsFree) {
ens.Add(Ensures(s.E.tok, s.IsFree, s.E, null, null));
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index f9b2c66e..ac5e6be5 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -486,8 +486,12 @@ Execution trace: (0,0): anon0
(0,0): anon9_Then
(0,0): anon3
+FunctionSpecifications.dfy(56,10): Error BP5003: A postcondition might not hold on this return path.
+FunctionSpecifications.dfy(57,22): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon5_Else
-Dafny program verifier finished with 3 verified, 3 errors
+Dafny program verifier finished with 3 verified, 4 errors
-------------------- ResolutionErrors.dfy --------------------
ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context
diff --git a/Test/dafny0/FunctionSpecifications.dfy b/Test/dafny0/FunctionSpecifications.dfy index 13171c47..44709ce8 100644 --- a/Test/dafny0/FunctionSpecifications.dfy +++ b/Test/dafny0/FunctionSpecifications.dfy @@ -52,3 +52,9 @@ function DivergentPost(n: int): int if n < 2 then n else
DivergentPost(n-2) + DivergentPost(n-1)
}
+
+function HoldsAtLeastForZero(x: int): bool
+ ensures x == 0 ==> HoldsAtLeastForZero(x);
+{
+ x < -2 // error: this does not hold for 0
+}
|