Bring back ReportEndVerifyImplementation (#705)

boogie-org · Mar 9, 2023 · 6f2d102 · 6f2d102
1 parent 5af8ea2
commit 6f2d102
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 5 deletions.
diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props
@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>2.16.2</Version>
+    <Version>2.16.3</Version>
     <TargetFramework>net6.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -831,9 +831,11 @@ private IObservable<IVerificationStatus> VerifyImplementation(
       var afterRunningStates = VerifyImplementationWithoutCaching(processedProgram, stats, er, cancellationToken,
         programId, implementation, traceWriter).Do(status =>
       {
-        if (status is Completed completed && 0 < Options.VerifySnapshots && !string.IsNullOrEmpty(implementation.Checksum))
-        {
-          Cache.Insert(implementation, completed.Result);
+        if (status is Completed completed) {
+          if (0 < Options.VerifySnapshots && !string.IsNullOrEmpty(implementation.Checksum)) {
+            Cache.Insert(implementation, completed.Result);
+          }
+          Options.Printer.ReportEndVerifyImplementation(implementation, completed.Result);
         }
       });
       return Observable.Return(new Running()).Concat(afterRunningStates);

diff --git a/Source/ExecutionEngine/OutputPrinter.cs b/Source/ExecutionEngine/OutputPrinter.cs
@@ -14,4 +14,5 @@ public interface OutputPrinter
   void WriteTrailer(TextWriter textWriter, PipelineStatistics stats);
   void WriteErrorInformation(ErrorInformation errorInfo, TextWriter tw, bool skipExecutionTrace = true);
   void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null);
+  void ReportEndVerifyImplementation(Implementation implementation, VerificationResult result);
 }
diff --git a/Source/UnitTests/ExecutionEngineTests/NullPrinter.cs b/Source/UnitTests/ExecutionEngineTests/NullPrinter.cs
@@ -29,4 +29,8 @@ public void WriteErrorInformation(ErrorInformation errorInfo, TextWriter tw, boo
 
   public void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null) {
   }
-}
+
+  public void ReportEndVerifyImplementation(Implementation implementation, VerificationResult result)
+  {
+  }
+}
-Original file line number
+Diff line change
@@ Expand Up @@
       public void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null) {
       }
-    }
+      public void ReportEndVerifyImplementation(Implementation implementation, VerificationResult result)
+      {
+      }
+    }