diff options
| -rw-r--r-- | Dafny/Translator.cs | 5 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 15 | ||||
| -rw-r--r-- | Test/dafny1/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny1/Induction.dfy | 13 | ||||
| -rw-r--r-- | Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyLanguageService.cs | 43 |
6 files changed, 60 insertions, 20 deletions
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index 19272ef4..54a51d11 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -3067,7 +3067,8 @@ namespace Microsoft.Dafny { Bpl.Expr Si = FunctionCall(stmt.Tok, BuiltinFunction.SeqIndex, predef.BoxType, S, i);
Bpl.Trigger tr = new Bpl.Trigger(stmt.Tok, true, new Bpl.ExprSeq(Si));
// TODO: in the next line, the == should be replaced by something that understands extensionality, for sets and sequences
- oInS = new Bpl.ExistsExpr(stmt.Tok, new Bpl.VariableSeq(iVar), tr, Bpl.Expr.And(range, Bpl.Expr.Eq(Si, o)));
+ var boxO = etran.BoxIfNecessary(stmt.Tok, o, ((SeqType)s.Collection.Type).Arg);
+ oInS = new Bpl.ExistsExpr(stmt.Tok, new Bpl.VariableSeq(iVar), tr, Bpl.Expr.And(range, Bpl.Expr.Eq(Si, boxO)));
}
oInS = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), oInS);
@@ -5533,7 +5534,7 @@ namespace Microsoft.Dafny { // consider automatically applying induction
var inductionVariables = new List<BoundVar>();
foreach (var n in e.BoundVars) {
- if (VarOccursInArgumentToRecursiveFunction(e.LogicalBody(), n, null)) {
+ if (!n.Type.IsTypeParameter && VarOccursInArgumentToRecursiveFunction(e.LogicalBody(), n, null)) {
if (CommandLineOptions.Clo.Trace) {
Console.Write("Applying automatic induction on variable '{0}' of: ", n.Name);
new Printer(Console.Out).PrintExpression(e);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 1a3218eb..05250fa8 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -201,7 +201,7 @@ Execution trace: (0,0): anon15
(0,0): anon25_Else
-Dafny program verifier finished with 41 verified, 14 errors
+Dafny program verifier finished with 43 verified, 14 errors
-------------------- Definedness.dfy --------------------
Definedness.dfy(8,7): Error: possible division by zero
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index b4dc6599..ac7286e9 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -308,7 +308,7 @@ method QuantifierRange2<T>(a: seq<T>, x: T, y: T, N: int) }
}
-// ----------------------- tests that involve sequences of boxed booleans --------
+// ----------------------- tests that involve sequences of boxes --------
ghost method M(zeros: seq<bool>, Z: bool)
requires 1 <= |zeros| && Z == false;
@@ -317,3 +317,16 @@ ghost method M(zeros: seq<bool>, Z: bool) var x := [Z];
assert zeros[0..1] == [Z];
}
+
+class SomeType
+{
+ var x: int;
+ method DoIt(stack: seq<SomeType>)
+ modifies stack;
+ {
+ // the following line once gave rise to a crash in the translation
+ foreach (n in stack) {
+ n.x := 10;
+ }
+ }
+}
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index 0111f9af..5ee9f921 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -81,7 +81,7 @@ Dafny program verifier finished with 6 verified, 0 errors -------------------- Induction.dfy --------------------
-Dafny program verifier finished with 26 verified, 0 errors
+Dafny program verifier finished with 29 verified, 0 errors
-------------------- Rippling.dfy --------------------
diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy index de5a3358..15cc1ffe 100644 --- a/Test/dafny1/Induction.dfy +++ b/Test/dafny1/Induction.dfy @@ -153,6 +153,19 @@ class DatatypeInduction<T> { }
// see also Test/dafny0/DTypes.dfy for more variations of this example
+
+ function OccurrenceCount<T>(tree: Tree<T>, x: T): int
+ {
+ match tree
+ case Leaf(t) => if x == t then 1 else 0
+ case Branch(left, right) => OccurrenceCount(left, x) + OccurrenceCount(right, x)
+ }
+ method RegressionTest(tree: Tree<T>)
+ // the translation of the following line once crashed Dafny
+ requires forall y :: 0 <= OccurrenceCount(tree, y);
+ {
+ }
+
}
// ----------------------- Induction and case splits -----------------
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyLanguageService.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyLanguageService.cs index b9a0ca22..ce43e6e4 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyLanguageService.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyLanguageService.cs @@ -176,21 +176,25 @@ namespace Demo // the lines of interest have the form "filename(line,col): some_error_label: error_message"
// where "some_error_label" is "Error" or "syntax error" or "Error BP5003" or "Related location"
if (line.Equals("")) continue;
- if (line.StartsWith("Dafny program verifier finished with") && line.Contains("time out"))
+ if (line.StartsWith("Dafny program verifier finished with"))
{
- try
+ if (line.Contains("time out"))
{
AddErrorBecauseOfToolProblems(req, "Verification timed out.");
}
- catch (System.FormatException)
+ else
{
- continue;
+ if (!line.Contains("inconclusive") && !line.Contains("out of memory"))
+ {
+ if (line.Contains(" 0 errors"))
+ AddMessage(req, "Verification successful.");
+ }
+ else
+ {
+ AddErrorBecauseOfToolProblems(req, "Internal verification fault.");
+ }
}
- catch (System.OverflowException)
- {
- continue;
- }
- continue;
+ break;
}
string message;
int n = line.IndexOf("): ", 2); // we start at 2, to avoid problems with "C:\..."
@@ -271,12 +275,21 @@ namespace Demo return new AuthoringScope(source.ParseResult);
}
- private static void AddErrorBecauseOfToolProblems(ParseRequest req, string msg) {
- TextSpan span = new TextSpan();
- span.iStartLine = span.iEndLine = 1;
- span.iStartIndex = 1;
- span.iEndIndex = 2;
- req.Sink.AddError(req.FileName, msg, span, Severity.Error);
+ private static void AddErrorBecauseOfToolProblems(ParseRequest req, string msg)
+ {
+ TextSpan span = new TextSpan();
+ span.iStartLine = span.iEndLine = 0;
+ span.iStartIndex = 0;
+ span.iEndIndex = 0;
+ req.Sink.AddError(req.FileName, msg, span, Severity.Error);
+ }
+ private static void AddMessage(ParseRequest req, string msg)
+ {
+ TextSpan span = new TextSpan();
+ span.iStartLine = span.iEndLine = 0;
+ span.iStartIndex = 0;
+ span.iEndIndex = 1;
+ req.Sink.AddError(req.FileName, msg, span, Severity.Hint);
}
/// <summary>
|