Implement max_success/max_proof time also for summary output

README.md

@@ -142,15 +142,15 @@ Typical output would look like this:
 
 ```
 saatana-crypto.spark        => (Flow  => 9.0 ms,
-                                Proof => 6.8 s)
+                                Proof => 80.0 ms/80.0 ms/6.8 s)
 saatana-crypto-phelix.spark => (Flow  => 206.5 ms,
-                                Proof => 568.7 s)
+                                Proof => 174.3 s/206.4 s/568.7 s)
 saatana.spark               => (Flow  => 464.0 µs,
-                                Proof => 0.0 s)
+                                Proof => 0.0 s/0.0 s/0.0 s)
 saatana-crypto-lemmas.spark => (Flow  => 2.1 ms,
-                                Proof => 2.2 s)
+                                Proof => 210.0 ms/210.0 ms/2.2 s)
 test_phelix_api.spark       => (Flow  => 14.4 ms,
-                                Proof => 23.1 s)
+                                Proof => 240.0 ms/240.0 ms/23.1 s)
 ```
 
 You can use the `--sort-by` option with `--summary`, either for an alphabetical
@@ -160,6 +160,8 @@ so files with the most time needed by the provers come first).  The option
 warning that what you requested has not been implemented yet.  By default, no
 particular order is imposed on the output.
 
+For the meaning of the three timings after `Proof =>`, please see below.
+
 *Note* that the `--details` option has no effect on the output here, this
 option is designed to work with the `--report-mode` option only.
 

src/run_spat-print_summary.adb

@@ -37,6 +37,8 @@ begin
    for File of Files loop
       --  Can't use Files.Max_Length here, because we use the Simple_Name, not
       --  the actual string stored.
+      --  FIXME: This assumes that everything is displayed, the actual output
+      --         might be less and the tabulation is a bit wide.
       Second_Column :=
         Ada.Text_IO.Count'Max (Second_Column,
                                Ada.Directories.Simple_Name
@@ -66,10 +68,20 @@ begin
             New_Line => False);
          Ada.Text_IO.Set_Col (File => Ada.Text_IO.Standard_Output,
                               To   => Third_Column);
-         SPAT.Log.Message
-           (Message =>
-              "Proof => " &
-              SPAT.Image (Value => Info.Proof_Time (File => File)) & ")");
+
+         declare
+            Max_Success_Proof_Time : constant Duration :=
+              Info.Max_Success_Proof_Time (File => File);
+         begin
+            SPAT.Log.Message
+              (Message =>
+                 "Proof => " &
+                 (if Max_Success_Proof_Time = -1.0 --  nothing valid found
+                  then "--"
+                  else SPAT.Image (Value => Max_Success_Proof_Time)) & "/" &
+                 SPAT.Image (Value => Info.Max_Proof_Time (File => File)) & "/" &
+                 SPAT.Image (Value => Info.Proof_Time (File => File)) & ")");
+         end;
       end if;
    end loop;
 

src/spat-spark_info.adb

@@ -778,6 +778,39 @@ package body SPAT.Spark_Info is
       return Sentinel.Cache.Max_Proof_Time;
    end Max_Proof_Time;
 
+   ---------------------------------------------------------------------------
+   --  Max_Proof_Time
+   ---------------------------------------------------------------------------
+   not overriding
+   function Max_Proof_Time (This : in T;
+                            File : in File_Name) return Duration
+   is
+      Result      : Duration := -1.0;
+      File_Cursor : constant File_Sets.Cursor := This.Files.Find (Item => File);
+      use type File_Sets.Cursor;
+   begin
+      --  FIXME: We shouldn't need to iterate through all entities each time
+      --         this subprogram is called.
+      for Position in This.Entities.Iterate loop
+         if
+           Analyzed_Entities.Element (Position => Position).SPARK_File =
+             File_Cursor
+         then
+            declare
+               Reference : constant Analyzed_Entities.Constant_Reference_Type :=
+                 This.Entities.Constant_Reference (Position => Position);
+               Sentinel  : constant Proofs_Sentinel :=
+                 Get_Sentinel (Node => Reference);
+            begin
+               Result := Duration'Max (Result,
+                                       Sentinel.Cache.Max_Proof_Time);
+            end;
+         end if;
+      end loop;
+
+      return Result;
+   end Max_Proof_Time;
+
    ---------------------------------------------------------------------------
    --  Max_Success_Proof_Time
    ---------------------------------------------------------------------------
@@ -792,6 +825,43 @@ package body SPAT.Spark_Info is
       return Sentinel.Cache.Max_Success_Proof_Time;
    end Max_Success_Proof_Time;
 
+   ---------------------------------------------------------------------------
+   --  Max_Success_Proof_Time
+   ---------------------------------------------------------------------------
+   not overriding
+   function Max_Success_Proof_Time (This : in T;
+                                    File : in File_Name) return Duration
+   is
+      Result      : Duration := -1.0;
+      File_Cursor : constant File_Sets.Cursor := This.Files.Find (Item => File);
+      use type File_Sets.Cursor;
+   begin
+      --  FIXME: We shouldn't need to iterate through all entities each time
+      --         this subprogram is called.
+      for Position in This.Entities.Iterate loop
+         if
+           Analyzed_Entities.Element (Position => Position).SPARK_File =
+             File_Cursor
+         then
+            declare
+               Reference : constant Analyzed_Entities.Constant_Reference_Type :=
+                 This.Entities.Constant_Reference (Position => Position);
+               Sentinel  : constant Proofs_Sentinel :=
+                 Get_Sentinel (Node => Reference);
+            begin
+               if Sentinel.Cache.Has_Unproved_Attempts then
+                  null; --  Unproved, so skip.
+               else
+                  Result := Duration'Max (Result,
+                                          Sentinel.Cache.Max_Success_Proof_Time);
+               end if;
+            end;
+         end if;
+      end loop;
+
+      return Result;
+   end Max_Success_Proof_Time;
+
    ---------------------------------------------------------------------------
    --  Num_Flows
    ---------------------------------------------------------------------------

src/spat-spark_info.ads

@@ -103,6 +103,23 @@ package SPAT.Spark_Info is
    function Proof_Time (This : in T;
                         File : in File_Name) return Duration;
 
+   ---------------------------------------------------------------------------
+   --  Max_Proof_Time
+   ---------------------------------------------------------------------------
+   not overriding
+   function Max_Proof_Time (This : in T;
+                            File : in File_Name) return Duration;
+
+   ---------------------------------------------------------------------------
+   --  Max_Success_Proof_Time
+   --
+   --  Reported time for the longest successful proof.
+   --  If the time returned is -1.0, then nothing is proven.
+   ---------------------------------------------------------------------------
+   not overriding
+   function Max_Success_Proof_Time (This : in T;
+                                    File : in File_Name) return Duration;
+
    ---------------------------------------------------------------------------
    --  Max_Proof_Time
    --

test/spat.test-issues.sca.template

@@ -1,2 +1,2 @@
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)

test/spat.test-issues.scs.template

@@ -1,3 +1,3 @@
 Warning: Sorting files by success time not implemented yet, falling back to maximum time.
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)

test/spat.test-issues.sct.template

@@ -1,3 +1,3 @@
 Warning: Sorting files by success time not implemented yet, falling back to maximum time.
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)

test/spat.test-issues.sdca.template

@@ -1,2 +1,2 @@
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)

test/spat.test-issues.sdcs.template

@@ -1,3 +1,3 @@
 Warning: Sorting files by success time not implemented yet, falling back to maximum time.
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)

test/spat.test-issues.sdct.template

@@ -1,3 +1,3 @@
 Warning: Sorting files by success time not implemented yet, falling back to maximum time.
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)

test/spat.test-issues.sraca.template

@@ -1,5 +1,5 @@
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)
 RFLX.RFLX_Types                          => 0.0 s/0.0 s/0.0 s
 RFLX.RFLX_Types.Byte_Index               => 10.0 ms/10.0 ms/30.0 ms
 RFLX.RFLX_Types.First_Bit_Index          => 0.0 s/0.0 s/0.0 s

test/spat.test-issues.sracs.template

@@ -1,6 +1,6 @@
 Warning: Sorting files by success time not implemented yet, falling back to maximum time.
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)
 RFLX.RFLX_Types.U64_Insert               => 54.2 s/120.0 s/1.6 ks
 RFLX.RFLX_Types.U64_Extract              => 37.9 s/120.0 s/1.8 ks
 RFLX.RFLX_Types.U64_Extract_Remaining    => 10.1 s/120.0 s/376.5 s

test/spat.test-issues.sract.template

@@ -1,6 +1,6 @@
 Warning: Sorting files by success time not implemented yet, falling back to maximum time.
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)
 RFLX.RFLX_Types.U64_Extract              => 37.9 s/120.0 s/1.8 ks
 RFLX.RFLX_Types.U64_Insert               => 54.2 s/120.0 s/1.6 ks
 RFLX.RFLX_Types.U64_Extract_Intermediate => 6.7 s/120.0 s/617.3 s

test/spat.test-issues.sradca.template

@@ -1,5 +1,5 @@
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)
 RFLX.RFLX_Types                          => 0.0 s/0.0 s/0.0 s
 RFLX.RFLX_Types.Byte_Index               => 10.0 ms/10.0 ms/30.0 ms
 `-VC_DIVISION_CHECK rflx-rflx_generic_types.ads:36:36 => 10.0 ms/10.0 ms/10.0 ms

test/spat.test-issues.sradcs.template

@@ -1,6 +1,6 @@
 Warning: Sorting files by success time not implemented yet, falling back to maximum time.
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)
 RFLX.RFLX_Types.U64_Insert               => 54.2 s/120.0 s/1.6 ks
 `-VC_PRECONDITION rflx-rflx_generic_types.adb:221:39 => 5.2 s/120.0 s/490.6 s
  `-CVC4: 120.0 s (Timeout,-1 steps)

test/spat.test-issues.sradct.template

@@ -1,6 +1,6 @@
 Warning: Sorting files by success time not implemented yet, falling back to maximum time.
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)
 RFLX.RFLX_Types.U64_Extract              => 37.9 s/120.0 s/1.8 ks
 `-VC_PRECONDITION rflx-rflx_generic_types.adb:131:29 => 37.9 s/120.0 s/1.1 ks
  `-Z3: 120.0 s (Timeout,-1 steps)

test/spat.test-issues.srfca.template

@@ -1,5 +1,5 @@
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)
 RFLX.RFLX_Types.U64_Extract              => 37.9 s/120.0 s/1.8 ks
 RFLX.RFLX_Types.U64_Extract.D            => 4.7 s/9.5 s/70.6 s
 RFLX.RFLX_Types.U64_Extract_Intermediate => 6.7 s/120.0 s/617.3 s

test/spat.test-issues.srfcs.template

@@ -1,6 +1,6 @@
 Warning: Sorting files by success time not implemented yet, falling back to maximum time.
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)
 RFLX.RFLX_Types.U64_Insert               => 54.2 s/120.0 s/1.6 ks
 RFLX.RFLX_Types.U64_Extract              => 37.9 s/120.0 s/1.8 ks
 RFLX.RFLX_Types.U64_Extract_Remaining    => 10.1 s/120.0 s/376.5 s

test/spat.test-issues.srfct.template

@@ -1,6 +1,6 @@
 Warning: Sorting files by success time not implemented yet, falling back to maximum time.
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)
 RFLX.RFLX_Types.U64_Extract              => 37.9 s/120.0 s/1.8 ks
 RFLX.RFLX_Types.U64_Insert               => 54.2 s/120.0 s/1.6 ks
 RFLX.RFLX_Types.U64_Extract_Intermediate => 6.7 s/120.0 s/617.3 s

test/spat.test-issues.srfdca.template

@@ -1,5 +1,5 @@
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)
 RFLX.RFLX_Types.U64_Extract              => 37.9 s/120.0 s/1.8 ks
 `-VC_PRECONDITION rflx-rflx_generic_types.adb:131:29 => 37.9 s/120.0 s/1.1 ks
  `-Z3: 120.0 s (Timeout,-1 steps)

test/spat.test-issues.srfdcs.template

@@ -1,6 +1,6 @@
 Warning: Sorting files by success time not implemented yet, falling back to maximum time.
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)
 RFLX.RFLX_Types.U64_Insert               => 54.2 s/120.0 s/1.6 ks
 `-VC_PRECONDITION rflx-rflx_generic_types.adb:221:39 => 5.2 s/120.0 s/490.6 s
  `-CVC4: 120.0 s (Timeout,-1 steps)

test/spat.test-issues.srfdct.template

@@ -1,6 +1,6 @@
 Warning: Sorting files by success time not implemented yet, falling back to maximum time.
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)
 RFLX.RFLX_Types.U64_Extract              => 37.9 s/120.0 s/1.8 ks
 `-VC_PRECONDITION rflx-rflx_generic_types.adb:131:29 => 37.9 s/120.0 s/1.1 ks
  `-Z3: 120.0 s (Timeout,-1 steps)

test/spat.test-issues.srjca.template

@@ -1,2 +1,2 @@
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)

test/spat.test-issues.srjcs.template

@@ -1,3 +1,3 @@
 Warning: Sorting files by success time not implemented yet, falling back to maximum time.
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)

test/spat.test-issues.srjct.template

@@ -1,3 +1,3 @@
 Warning: Sorting files by success time not implemented yet, falling back to maximum time.
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)

test/spat.test-issues.srjdca.template

@@ -1,2 +1,2 @@
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)

test/spat.test-issues.srjdcs.template

@@ -1,3 +1,3 @@
 Warning: Sorting files by success time not implemented yet, falling back to maximum time.
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)

test/spat.test-issues.srjdct.template

@@ -1,3 +1,3 @@
 Warning: Sorting files by success time not implemented yet, falling back to maximum time.
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)

test/spat.test-issues.sruca.template

@@ -1,2 +1,2 @@
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)

test/spat.test-issues.srucs.template

@@ -1,3 +1,3 @@
 Warning: Sorting files by success time not implemented yet, falling back to maximum time.
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)

test/spat.test-issues.sruct.template

@@ -1,3 +1,3 @@
 Warning: Sorting files by success time not implemented yet, falling back to maximum time.
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)

test/spat.test-issues.srudca.template

@@ -1,2 +1,2 @@
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)

test/spat.test-issues.srudcs.template

@@ -1,3 +1,3 @@
 Warning: Sorting files by success time not implemented yet, falling back to maximum time.
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)

test/spat.test-issues.srudct.template

@@ -1,3 +1,3 @@
 Warning: Sorting files by success time not implemented yet, falling back to maximum time.
 rflx-rflx_types.spark => (Flow  => 7.2 ms,
-                          Proof => 4.5 ks)
+                          Proof => 54.2 s/120.0 s/4.5 ks)

test/spat.test-saatana.sca.template

@@ -1,10 +1,10 @@
 saatana.spark               => (Flow  => 464.0 µs,
-                                Proof => 0.0 s)
+                                Proof => 0.0 s/0.0 s/0.0 s)
 saatana-crypto.spark        => (Flow  => 9.0 ms,
-                                Proof => 6.8 s)
+                                Proof => 80.0 ms/80.0 ms/6.8 s)
 saatana-crypto-lemmas.spark => (Flow  => 2.1 ms,
-                                Proof => 2.2 s)
+                                Proof => 210.0 ms/210.0 ms/2.2 s)
 saatana-crypto-phelix.spark => (Flow  => 206.5 ms,
-                                Proof => 568.7 s)
+                                Proof => 174.3 s/206.4 s/568.7 s)
 test_phelix_api.spark       => (Flow  => 14.4 ms,
-                                Proof => 23.1 s)
+                                Proof => 240.0 ms/240.0 ms/23.1 s)

test/spat.test-saatana.scs.template

@@ -1,11 +1,11 @@
 Warning: Sorting files by success time not implemented yet, falling back to maximum time.
 saatana-crypto-phelix.spark => (Flow  => 206.5 ms,
-                                Proof => 568.7 s)
+                                Proof => 174.3 s/206.4 s/568.7 s)
 test_phelix_api.spark       => (Flow  => 14.4 ms,
-                                Proof => 23.1 s)
+                                Proof => 240.0 ms/240.0 ms/23.1 s)
 saatana-crypto.spark        => (Flow  => 9.0 ms,
-                                Proof => 6.8 s)
+                                Proof => 80.0 ms/80.0 ms/6.8 s)
 saatana-crypto-lemmas.spark => (Flow  => 2.1 ms,
-                                Proof => 2.2 s)
+                                Proof => 210.0 ms/210.0 ms/2.2 s)
 saatana.spark               => (Flow  => 464.0 µs,
-                                Proof => 0.0 s)
+                                Proof => 0.0 s/0.0 s/0.0 s)

test/spat.test-saatana.sct.template

@@ -1,11 +1,11 @@
 Warning: Sorting files by success time not implemented yet, falling back to maximum time.
 saatana-crypto-phelix.spark => (Flow  => 206.5 ms,
-                                Proof => 568.7 s)
+                                Proof => 174.3 s/206.4 s/568.7 s)
 test_phelix_api.spark       => (Flow  => 14.4 ms,
-                                Proof => 23.1 s)
+                                Proof => 240.0 ms/240.0 ms/23.1 s)
 saatana-crypto.spark        => (Flow  => 9.0 ms,
-                                Proof => 6.8 s)
+                                Proof => 80.0 ms/80.0 ms/6.8 s)
 saatana-crypto-lemmas.spark => (Flow  => 2.1 ms,
-                                Proof => 2.2 s)
+                                Proof => 210.0 ms/210.0 ms/2.2 s)
 saatana.spark               => (Flow  => 464.0 µs,
-                                Proof => 0.0 s)
+                                Proof => 0.0 s/0.0 s/0.0 s)