diff --git a/Source/DafnyCore/Generic/LazyConcurrentDictionary.cs b/Source/DafnyCore/Generic/LazyConcurrentDictionary.cs index 8d5971df2a..0bae551cba 100644 --- a/Source/DafnyCore/Generic/LazyConcurrentDictionary.cs +++ b/Source/DafnyCore/Generic/LazyConcurrentDictionary.cs @@ -62,4 +62,8 @@ public bool TryGetValue(TKey key, out TValue? value) { } public TValue this[TKey key] => underlyingDictionary[key].Value; + + public bool Remove(TKey key) { + return underlyingDictionary.TryRemove(key, out _); + } } \ No newline at end of file diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs index f55690dfb4..45bbd1c55d 100644 --- a/Source/DafnyCore/Options/CommonOptionBag.cs +++ b/Source/DafnyCore/Options/CommonOptionBag.cs @@ -14,10 +14,12 @@ public class CommonOptionBag { public static void EnsureStaticConstructorHasRun() { } - public static readonly Option ProgressOption = - new("--progress", "While verifying, output information that helps track progress") { - IsHidden = true - }; + public enum ProgressLevel { None, Symbol, VerificationJobs } + public static readonly Option ProgressOption = + new("--progress", $"While verifying, output information that helps track progress. " + + $"Use '{ProgressLevel.Symbol}' to show progress across symbols such as methods and functions. " + + $"Verification of a symbol is usually split across several jobs. " + + $"Use {ProgressLevel.VerificationJobs} to additionally show progress across jobs."); public static readonly Option LogLocation = new("--log-location", "Sets the directory where to store log files") { diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs index cd289504fc..ecafc2dc95 100644 --- a/Source/DafnyCore/Pipeline/Compilation.cs +++ b/Source/DafnyCore/Pipeline/Compilation.cs @@ -332,9 +332,6 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT tasksForModule = await translatedModules.GetOrAdd(containingModule, async () => { var result = await verifier.GetVerificationTasksAsync(boogieEngine, resolution, containingModule, cancellationSource.Token); - foreach (var task in result) { - cancellationSource.Token.Register(task.Cancel); - } return result.GroupBy(t => ((IToken)t.ScopeToken).GetFilePosition()).ToDictionary( g => g.Key, @@ -433,6 +430,11 @@ private void HandleStatusUpdate(ICanVerify canVerify, IVerificationTask verifica public void CancelPendingUpdates() { cancellationSource.Cancel(); + foreach (var (_, tasks) in tasksPerVerifiable) { + foreach (var task in tasks) { + task.Cancel(); + } + } } public async Task GetTextEditToFormatCode(Uri uri) { @@ -507,7 +509,7 @@ public static void ReportDiagnosticsInResult(DafnyOptions options, string name, // This reports problems that are not captured by counter-examples, like a time-out // The Boogie API forces us to create a temporary engine here to report the outcome, even though it only uses the options. - var boogieEngine = new ExecutionEngine(options, new VerificationResultCache(), + var boogieEngine = new ExecutionEngine(options, new EmptyVerificationResultCache(), CustomStackSizePoolTaskScheduler.Create(0, 0)); boogieEngine.ReportOutcome(null, outcome, outcomeError => errorReporter.ReportBoogieError(outcomeError, null, false), name, token, null, TextWriter.Null, @@ -579,4 +581,12 @@ public static VcOutcome GetOutcome(SolverOutcome outcome) { throw new ArgumentOutOfRangeException(nameof(outcome), outcome, null); } } + + public void ClearModuleCache(ModuleDefinition moduleDefinition) { + translatedModules.Remove(moduleDefinition); + } + + public void ClearCanVerifyCache(ICanVerify canVerify) { + tasksPerVerifiable.Remove(canVerify); + } } \ No newline at end of file diff --git a/Source/DafnyDriver/CliCanVerifyState.cs b/Source/DafnyDriver/CliCanVerifyState.cs index e74c060d73..0a1fa89084 100644 --- a/Source/DafnyDriver/CliCanVerifyState.cs +++ b/Source/DafnyDriver/CliCanVerifyState.cs @@ -10,5 +10,5 @@ public record CliCanVerifyState { public Func TaskFilter = _ => true; public readonly TaskCompletionSource Finished = new(); public readonly ConcurrentQueue<(IVerificationTask Task, Completed Result)> CompletedParts = new(); - public readonly ConcurrentBag Tasks = new(); + public int TaskCount; } \ No newline at end of file diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index 52f4ee0fad..7b90a78802 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/Source/DafnyDriver/CliCompilation.cs @@ -45,7 +45,7 @@ private CliCompilation( options.RunningBoogieFromCommandLine = true; var input = new CompilationInput(options, 0, options.DafnyProject); - var executionEngine = new ExecutionEngine(options, new VerificationResultCache(), DafnyMain.LargeThreadScheduler); + var executionEngine = new ExecutionEngine(options, new EmptyVerificationResultCache(), DafnyMain.LargeThreadScheduler); Compilation = createCompilation(executionEngine, input); } @@ -162,10 +162,10 @@ public async IAsyncEnumerable VerifyAllLazily(int? randomSeed) if (ev is CanVerifyPartsIdentified canVerifyPartsIdentified) { var canVerifyResult = canVerifyResults[canVerifyPartsIdentified.CanVerify]; foreach (var part in canVerifyPartsIdentified.Parts.Where(canVerifyResult.TaskFilter)) { - canVerifyResult.Tasks.Add(part); + Interlocked.Increment(ref canVerifyResult.TaskCount); } - if (canVerifyResult.CompletedParts.Count == canVerifyResult.Tasks.Count) { + if (canVerifyResult.CompletedParts.Count == canVerifyResult.TaskCount) { canVerifyResult.Finished.SetResult(); } } @@ -184,17 +184,17 @@ public async IAsyncEnumerable VerifyAllLazily(int? randomSeed) var canVerifyResult = canVerifyResults[boogieUpdate.CanVerify]; canVerifyResult.CompletedParts.Enqueue((boogieUpdate.VerificationTask, completed)); - if (Options.Get(CommonOptionBag.ProgressOption)) { + if (Options.Get(CommonOptionBag.ProgressOption) == CommonOptionBag.ProgressLevel.VerificationJobs) { var token = BoogieGenerator.ToDafnyToken(false, boogieUpdate.VerificationTask.Split.Token); var runResult = completed.Result; var timeString = runResult.RunTime.ToString("g"); Options.OutputWriter.WriteLine( - $"Verified part #{boogieUpdate.VerificationTask.Split.SplitIndex}, {canVerifyResult.CompletedParts.Count}/{canVerifyResult.Tasks.Count} of {boogieUpdate.CanVerify.FullDafnyName}" + + $"Verified part #{boogieUpdate.VerificationTask.Split.SplitIndex}, {canVerifyResult.CompletedParts.Count}/{canVerifyResult.TaskCount} of {boogieUpdate.CanVerify.FullDafnyName}" + $", on line {token.line}, " + $"{DescribeOutcome(Compilation.GetOutcome(runResult.Outcome))}" + $" (time: {timeString}, resource count: {runResult.ResourceCount})"); } - if (canVerifyResult.CompletedParts.Count == canVerifyResult.Tasks.Count) { + if (canVerifyResult.CompletedParts.Count == canVerifyResult.TaskCount) { canVerifyResult.Finished.TrySetResult(); } } @@ -216,42 +216,53 @@ public async IAsyncEnumerable VerifyAllLazily(int? randomSeed) canVerifies = FilterCanVerifies(canVerifies, out var line); VerifiedAssertions = line != null; - var orderedCanVerifies = canVerifies.OrderBy(v => v.Tok.pos).ToList(); - foreach (var canVerify in orderedCanVerifies) { - var results = new CliCanVerifyState(); - canVerifyResults[canVerify] = results; - if (line != null) { - results.TaskFilter = t => KeepVerificationTask(t, line.Value); - } + int done = 0; - var shouldVerify = await Compilation.VerifyCanVerify(canVerify, results.TaskFilter, randomSeed); - if (!shouldVerify) { - orderedCanVerifies.Remove(canVerify); - } - } + var canVerifiesPerModule = canVerifies.ToList().GroupBy(c => c.ContainingModule).ToList(); + foreach (var canVerifiesForModule in canVerifiesPerModule. + OrderBy(v => v.Key.Tok.pos)) { + var orderedCanVerifies = canVerifiesForModule.OrderBy(v => v.Tok.pos).ToList(); + foreach (var canVerify in orderedCanVerifies) { + var results = new CliCanVerifyState(); + canVerifyResults[canVerify] = results; + if (line != null) { + results.TaskFilter = t => KeepVerificationTask(t, line.Value); + } - int done = 0; - foreach (var canVerify in orderedCanVerifies) { - var results = canVerifyResults[canVerify]; - try { - if (Options.Get(CommonOptionBag.ProgressOption)) { - await Options.OutputWriter.WriteLineAsync($"Verified {done}/{orderedCanVerifies.Count} symbols. Waiting for {canVerify.FullDafnyName} to verify."); + var shouldVerify = await Compilation.VerifyCanVerify(canVerify, results.TaskFilter, randomSeed); + if (!shouldVerify) { + canVerifies.ToList().Remove(canVerify); } - await results.Finished.Task; - done++; - } catch (ProverException e) { - Compilation.Reporter.Error(MessageSource.Verifier, ResolutionErrors.ErrorId.none, canVerify.Tok, e.Message); - yield break; - } catch (OperationCanceledException) { - - } catch (Exception e) { - Compilation.Reporter.Error(MessageSource.Verifier, ResolutionErrors.ErrorId.none, canVerify.Tok, - $"Internal error occurred during verification: {e.Message}\n{e.StackTrace}"); - throw; } - yield return new CanVerifyResult(canVerify, results.CompletedParts.Select(c => new VerificationTaskResult(c.Task, c.Result.Result)).ToList()); - canVerifyResults.Remove(canVerify); // Free memory + foreach (var canVerify in orderedCanVerifies) { + var results = canVerifyResults[canVerify]; + try { + if (Options.Get(CommonOptionBag.ProgressOption) > CommonOptionBag.ProgressLevel.None) { + await Options.OutputWriter.WriteLineAsync( + $"Verified {done}/{canVerifies.ToList().Count} symbols. Waiting for {canVerify.FullDafnyName} to verify."); + } + + await results.Finished.Task; + done++; + } catch (ProverException e) { + Compilation.Reporter.Error(MessageSource.Verifier, ResolutionErrors.ErrorId.none, canVerify.Tok, e.Message); + yield break; + } catch (OperationCanceledException) { + + } catch (Exception e) { + Compilation.Reporter.Error(MessageSource.Verifier, ResolutionErrors.ErrorId.none, canVerify.Tok, + $"Internal error occurred during verification: {e.Message}\n{e.StackTrace}"); + throw; + } + + yield return new CanVerifyResult(canVerify, + results.CompletedParts.Select(c => new VerificationTaskResult(c.Task, c.Result.Result)).ToList()); + + canVerifyResults.Remove(canVerify); // Free memory + Compilation.ClearCanVerifyCache(canVerify); + } + Compilation.ClearModuleCache(canVerifiesForModule.Key); } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Iterators.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Iterators.dfy.expect index 90f6be73f0..2e9399ffca 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Iterators.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Iterators.dfy.expect @@ -11,15 +11,6 @@ Iterators.dfy(177,27): Error: assertion might not hold Iterators.dfy(208,6): Error: an assignment to _new is only allowed to shrink the set Iterators.dfy(212,20): Error: assertion might not hold Iterators.dfy(234,20): Error: assertion might not hold -Iterators.dfy(251,9): Error: decreases clause might not decrease -Iterators.dfy(274,9): Error: decreases clause might not decrease -Iterators.dfy(284,31): Error: decreases clause might not decrease -Iterators.dfy(296,9): Error: cannot prove termination; try supplying a decreases clause -Iterators.dfy(317,9): Error: cannot prove termination; try supplying a decreases clause -Iterators.dfy(326,31): Error: cannot prove termination; try supplying a decreases clause -Iterators.dfy(343,9): Error: decreases clause might not decrease -Iterators.dfy(353,31): Error: cannot prove termination; try supplying a decreases clause -Iterators.dfy(370,9): Error: decreases clause might not decrease Iterators.dfy(413,16): Error: this invariant could not be proved to be maintained by the loop Related message: loop invariant violation Iterators.dfy(414,21): Error: this invariant could not be proved to be maintained by the loop @@ -40,5 +31,14 @@ Iterators.dfy(461,21): Error: this invariant could not be proved to be maintaine Related message: loop invariant violation Iterators.dfy(470,4): Error: possible violation of yield-ensures condition Iterators.dfy(451,21): Related location: this proposition could not be proved +Iterators.dfy(251,9): Error: decreases clause might not decrease +Iterators.dfy(274,9): Error: decreases clause might not decrease +Iterators.dfy(284,31): Error: decreases clause might not decrease +Iterators.dfy(296,9): Error: cannot prove termination; try supplying a decreases clause +Iterators.dfy(317,9): Error: cannot prove termination; try supplying a decreases clause +Iterators.dfy(326,31): Error: cannot prove termination; try supplying a decreases clause +Iterators.dfy(343,9): Error: decreases clause might not decrease +Iterators.dfy(353,31): Error: cannot prove termination; try supplying a decreases clause +Iterators.dfy(370,9): Error: decreases clause might not decrease Dafny program verifier finished with 35 verified, 30 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/OpaqueFunctions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/OpaqueFunctions.dfy.expect index f2f690b95d..5f2b32d289 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/OpaqueFunctions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/OpaqueFunctions.dfy.expect @@ -1,3 +1,5 @@ +OpaqueFunctions.dfy(214,15): Error: assertion might not hold +OpaqueFunctions.dfy(229,19): Error: assertion might not hold OpaqueFunctions.dfy(38,15): Error: assertion might not hold OpaqueFunctions.dfy(69,7): Error: a precondition for this call could not be proved OpaqueFunctions.dfy(35,15): Related location: this is the precondition that could not be proved @@ -20,8 +22,6 @@ OpaqueFunctions.dfy(157,20): Error: assertion might not hold OpaqueFunctions.dfy(160,20): Error: assertion might not hold OpaqueFunctions.dfy(165,31): Error: assertion might not hold OpaqueFunctions.dfy(181,12): Error: assertion might not hold -OpaqueFunctions.dfy(214,15): Error: assertion might not hold -OpaqueFunctions.dfy(229,19): Error: assertion might not hold OpaqueFunctions.dfy(246,11): Error: assertion might not hold OpaqueFunctions.dfy(261,11): Error: assertion might not hold OpaqueFunctions.dfy(326,16): Error: assertion might not hold diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.expect index 0106799b5a..f04a5ed0bc 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.expect @@ -4,7 +4,6 @@ Termination.dfy(126,16): Error: decreases expression must be bounded below by 0 Termination.dfy(255,34): Error: cannot prove termination; try supplying a decreases clause Termination.dfy(296,2): Error: decreases expression might not decrease Termination.dfy(361,46): Error: decreases clause might not decrease -Termination.dfy[TerminationRefinement1](441,5): Error: decreases clause might not decrease Termination.dfy(534,2): Error: decreases expression might not decrease Termination.dfy(542,2): Error: decreases expression might not decrease Termination.dfy(549,2): Error: decreases expression might not decrease @@ -21,5 +20,6 @@ Termination.dfy(730,2): Error: decreases expression might not decrease Termination.dfy(806,2): Error: cannot prove termination; try supplying a decreases clause for the loop Termination.dfy(1178,2): Error: cannot prove termination; try supplying a decreases clause for the loop Termination.dfy(1194,2): Error: cannot prove termination; try supplying a decreases clause for the loop +Termination.dfy[TerminationRefinement1](441,5): Error: decreases clause might not decrease Dafny program verifier finished with 108 verified, 23 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.refresh.expect index e617b14d52..68e96bebe1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.refresh.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.refresh.expect @@ -4,7 +4,6 @@ Termination.dfy(126,16): Error: decreases expression must be bounded below by 0 Termination.dfy(255,34): Error: cannot prove termination; try supplying a decreases clause Termination.dfy(296,2): Error: decreases expression might not decrease Termination.dfy(361,46): Error: decreases clause might not decrease -Termination.dfy[TerminationRefinement1](441,5): Error: decreases clause might not decrease Termination.dfy(534,2): Error: decreases expression might not decrease Termination.dfy(542,2): Error: decreases expression might not decrease Termination.dfy(549,2): Error: decreases expression might not decrease @@ -22,5 +21,6 @@ Termination.dfy(806,2): Error: cannot prove termination; try supplying a decreas Termination.dfy(923,2): Error: cannot prove termination; try supplying a decreases clause for the loop Termination.dfy(1178,2): Error: cannot prove termination; try supplying a decreases clause for the loop Termination.dfy(1194,2): Error: cannot prove termination; try supplying a decreases clause for the loop +Termination.dfy[TerminationRefinement1](441,5): Error: decreases clause might not decrease Dafny program verifier finished with 107 verified, 24 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy.expect index 0844dd8c4c..a09670b9fe 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy.expect @@ -1,9 +1,9 @@ TypeInferenceRefresh.dfy(445,11): Warning: the modify statement with a block statement is deprecated TypeInferenceRefresh.dfy(807,4): Warning: this branch is redundant -TypeInferenceRefresh.dfy(102,31): Error: value does not satisfy the subset constraints of 'SubsetType' -TypeInferenceRefresh.dfy(107,31): Error: value does not satisfy the subset constraints of 'SubsetType' TypeInferenceRefresh.dfy(145,30): Error: element might not be in domain TypeInferenceRefresh.dfy(216,26): Error: result of operation might violate newtype constraint for 'int8' +TypeInferenceRefresh.dfy(102,31): Error: value does not satisfy the subset constraints of 'SubsetType' +TypeInferenceRefresh.dfy(107,31): Error: value does not satisfy the subset constraints of 'SubsetType' TypeInferenceRefresh.dfy(630,40): Error: value does not satisfy the subset constraints of 'nat' TypeInferenceRefresh.dfy(630,43): Error: value does not satisfy the subset constraints of 'nat' TypeInferenceRefresh.dfy(630,47): Error: value does not satisfy the subset constraints of 'nat' diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-977.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-977.dfy.expect index a88c141945..cb8bfddc60 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-977.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-977.dfy.expect @@ -36,7 +36,6 @@ git-issue-977.dfy(71,4): Info: ensures RicochetOrd(m, num) git-issue-977.dfy(110,9): Info: Some instances of this call are not inlined. git-issue-977.dfy(143,9): Info: Some instances of this call are not inlined. git-issue-977.dfy(162,2): Info: Some instances of this call are not inlined. -git-issue-977.dfy(220,11): Info: Some instances of this call are not inlined. git-issue-977.dfy(39,11): Error: assertion might not hold git-issue-977.dfy(14,20): Related location: this proposition could not be proved git-issue-977.dfy(9,7): Related location: this proposition could not be proved @@ -46,5 +45,6 @@ git-issue-977.dfy(9,7): Related location: this proposition could not be proved git-issue-977.dfy(43,11): Error: assertion might not hold git-issue-977.dfy(30,20): Related location: this proposition could not be proved git-issue-977.dfy(9,7): Related location: this proposition could not be proved +git-issue-977.dfy(220,11): Info: Some instances of this call are not inlined. Dafny program verifier finished with 20 verified, 3 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/VerboseName.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/VerboseName.dfy index 8567235715..4ea12ecb8d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/VerboseName.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/VerboseName.dfy @@ -1,4 +1,4 @@ -// RUN: %verify --progress --cores 1 "%s" > "%t" +// RUN: %verify --progress Symbol --cores 1 "%s" > "%t" // RUN: %OutputCheck --file-to-check "%t" "%s" // CHECK-L:Verified 0/5 symbols. Waiting for smallPrime to verify. // CHECK-L:Verified 2/5 symbols. Waiting for posIdMeth to verify. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter-symbol.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter-symbol.dfy.expect index f8f2da9d39..701d65563a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter-symbol.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter-symbol.dfy.expect @@ -1,19 +1,19 @@ Dafny program verifier finished with 0 verified, 0 errors -filter-symbol.dfy(12,29): Error: a postcondition could not be proved on this return path -filter-symbol.dfy(12,23): Related location: this is the postcondition that could not be proved filter-symbol.dfy(14,27): Error: a postcondition could not be proved on this return path filter-symbol.dfy(14,21): Related location: this is the postcondition that could not be proved +filter-symbol.dfy(12,29): Error: a postcondition could not be proved on this return path +filter-symbol.dfy(12,23): Related location: this is the postcondition that could not be proved filter-symbol.dfy(19,29): Error: a postcondition could not be proved on this return path filter-symbol.dfy(19,23): Related location: this is the postcondition that could not be proved Dafny program verifier finished with 0 verified, 3 errors filter-symbol.dfy(12,29): Error: a postcondition could not be proved on this return path filter-symbol.dfy(12,23): Related location: this is the postcondition that could not be proved -filter-symbol.dfy(19,29): Error: a postcondition could not be proved on this return path -filter-symbol.dfy(19,23): Related location: this is the postcondition that could not be proved filter-symbol.dfy(21,27): Error: a postcondition could not be proved on this return path filter-symbol.dfy(21,21): Related location: this is the postcondition that could not be proved +filter-symbol.dfy(19,29): Error: a postcondition could not be proved on this return path +filter-symbol.dfy(19,23): Related location: this is the postcondition that could not be proved Dafny program verifier finished with 0 verified, 3 errors filter-symbol.dfy(12,29): Error: a postcondition could not be proved on this return path diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy index 9fdfcd621b..45d489f1cf 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy @@ -1,4 +1,4 @@ -// RUN: %verify --progress --cores=1 %s &> %t +// RUN: %verify --progress VerificationJobs --cores=1 %s &> %t // RUN: %OutputCheck --file-to-check "%t" "%s" // CHECK:Verified part #0, 1/2 of Foo, on line 9, verified successfully \(time: .*, resource count: .*\) // CHECK:Verified part #1, 2/2 of Foo, on line 10, verified successfully \(time: .*, resource count: .*\) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy index 89b2e46ac9..6f0f4714bf 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy @@ -1,4 +1,4 @@ -// RUN: ! %verify --isolate-assertions --cores=1 --progress "%s" &> "%t" +// RUN: ! %verify --isolate-assertions --cores=1 --progress VerificationJobs "%s" &> "%t" // RUN: %OutputCheck --file-to-check "%t" "%S/Inputs/outOfResourceAndIsolateAssertions.check" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy index dc479d31aa..96b0f4a086 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy @@ -1,4 +1,4 @@ -// RUN: %verify --progress --isolate-assertions --cores=1 %s > %t +// RUN: %verify --progress VerificationJobs --isolate-assertions --cores=1 %s > %t // RUN: %OutputCheck --file-to-check %t "%S/Inputs/progressFirstSequence.check" // RUN: %OutputCheck --file-to-check %t "%S/Inputs/progressSecondSequence.check" diff --git a/docs/dev/news/5827.fix b/docs/dev/news/5827.fix new file mode 100644 index 0000000000..a86341ede8 --- /dev/null +++ b/docs/dev/news/5827.fix @@ -0,0 +1 @@ +Improve performance of `dafny verify` for large applications, by removing memory leaks \ No newline at end of file