From e0f36b606687fabf52b087a85a0d68c38a6b5358 Mon Sep 17 00:00:00 2001 From: Phil Thornley Date: Fri, 13 Aug 2010 14:34:27 +0100 Subject: [PATCH 1/2] Commit modified files. Commit the changes made to existing files. --- pogs/banner-get_version.adb | 4 +- pogs/pogs.idx | 5 + pogs/pogs.smf | 5 +- pogs/toppackage.adb | 16 + pogs/total.adb | 4052 ++++++++++++++++++++------------------- pogs/total.ads | 5 + pogs/vcs-analysesimplogfile.adb | 15 +- pogs/vcs.adb | 8 + pogs/vcs.ads | 3 + 9 files changed, 2095 insertions(+), 2018 deletions(-) diff --git a/pogs/banner-get_version.adb b/pogs/banner-get_version.adb index 105e7d7..7e6d77d 100644 --- a/pogs/banner-get_version.adb +++ b/pogs/banner-get_version.adb @@ -30,12 +30,12 @@ is begin if CommandLine.Data.PlainOutput then R := CreateBannerLine - (FromText => "POGS " & Version.Toolset_Distribution & " Edition", + (FromText => "Phil's POGS " & Version.Toolset_Distribution & " Edition", WithJustification => J, FillChar => ' '); else R := CreateBannerLine - (FromText => "POGS " & Version.Toolset_Banner_Line, + (FromText => "Phil's POGS " & Version.Toolset_Banner_Line, WithJustification => J, FillChar => ' '); end if; diff --git a/pogs/pogs.idx b/pogs/pogs.idx index 4c1c271..397b76d 100644 --- a/pogs/pogs.idx +++ b/pogs/pogs.idx @@ -44,3 +44,8 @@ toppackage specification is in toppackage.ads xmlsummary specification is in xmlsummary.ads xmlsummary body is in xmlsummary.adb slg_parser specification is in slg_parser.ads +-- +-- for Phil's added files +-- +rulelistadt specification is in rulelistadt.ads +total body is in total.adb diff --git a/pogs/pogs.smf b/pogs/pogs.smf index 840c3ff..e947750 100644 --- a/pogs/pogs.smf +++ b/pogs/pogs.smf @@ -23,4 +23,7 @@ vcs-processnewrangeline.adb vcs-writevcinfo.adb toppackage.adb xmlsummary.adb -slg_parser.adb \ No newline at end of file +slg_parser.adb +-- +-- Phil's added file +total-rulesusedforfile.adb diff --git a/pogs/toppackage.adb b/pogs/toppackage.adb index b042543..f2de52f 100644 --- a/pogs/toppackage.adb +++ b/pogs/toppackage.adb @@ -61,6 +61,7 @@ is TempUserFile : SPARK_IO.File_Type := SPARK_IO.Null_File; TempRluErrorFile : SPARK_IO.File_Type := SPARK_IO.Null_File; TempRluUsedFile : SPARK_IO.File_Type := SPARK_IO.Null_File; + TempRulesUsedFile : SPARK_IO.File_Type := SPARK_IO.Null_File; TempPRVerrFile : SPARK_IO.File_Type := SPARK_IO.Null_File; TempWarnErrorFile : SPARK_IO.File_Type := SPARK_IO.Null_File; Temp_SDP_Error_File : SPARK_IO.File_Type := SPARK_IO.Null_File; @@ -178,6 +179,17 @@ is FatalErrors.Process (FatalErrors.ProblemCreatingTempFile, ELStrings.Empty_String); end if; + -- create temporary file to store identities of user rules used + -- for proof + SPARK_IO.Create (TempRulesUsedFile, + 0, + "", + "", + StatusTemp); + if StatusTemp /= SPARK_IO.Ok then + FatalErrors.Process (FatalErrors.ProblemCreatingTempFile, ELStrings.Empty_String); + end if; + -- create temporary file to store names of review files containing errors SPARK_IO.Create (TempPRVerrFile, 0, @@ -251,6 +263,7 @@ is TempUserFile, TempRluErrorFile, TempRluUsedFile, + TempRulesUsedFile, TempPRVerrFile, TempWarnErrorFile, Temp_SDP_Error_File, @@ -266,6 +279,7 @@ is TempUserFile, TempRluErrorFile, TempRluUsedFile, + TempRulesUsedFile, TempPRVerrFile, TempWarnErrorFile, Temp_SDP_Error_File, @@ -304,6 +318,7 @@ is --# F, 10, TempUserFile, "TempUserFile unused here" & --# F, 10, TempRluErrorFile, "TempRluErrorFile unused here" & --# F, 10, TempRluUsedFile, "TempRluUsedFile unused here" & + --# F, 10, TempRulesUsedFile, "TempRulesUsedFile unused here" & --# F, 10, TempWarnErrorFile, "TempPRVerrFile unused here" & --# F, 10, TempPRVerrFile, "TempPRVerrFile unused here" & --# F, 10, Temp_DPC_Error_File, "Temp_DPC_Error_File unused here" & @@ -316,6 +331,7 @@ is TempUserFile, TempRluErrorFile, TempRluUsedFile, + TempRulesUsedFile, TempPRVerrFile, TempWarnErrorFile, Temp_SDP_Error_File, diff --git a/pogs/total.adb b/pogs/total.adb index 70523e8..1470abf 100644 --- a/pogs/total.adb +++ b/pogs/total.adb @@ -1,2014 +1,2038 @@ --- $Id: total.adb 16001 2010-02-09 09:18:07Z dean kuo $ --------------------------------------------------------------------------------- --- (C) Altran Praxis Limited --------------------------------------------------------------------------------- --- --- The SPARK toolset is free software; you can redistribute it and/or modify it --- under terms of the GNU General Public License as published by the Free --- Software Foundation; either version 3, or (at your option) any later --- version. The SPARK toolset is distributed in the hope that it will be --- useful, but WITHOUT ANY WARRANTY; without even the implied warranty of --- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General --- Public License for more details. You should have received a copy of the GNU --- General Public License distributed with the SPARK toolset; see file --- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of --- the license. --- ---============================================================================== - - --------------------------------------------------------------------------------- ---Synopsis: -- --- -- ---Package providing data structure to store running totals, and a procedure -- ---to print them. -- --- -- --------------------------------------------------------------------------------- -with Banner, - CommandLine, - ELStrings, - EStrings, - FatalErrors, - Heap, - VCHeap, - VCDetails, - XMLSummary; - -use type VCDetails.VC_State_T; -use type VCDetails.DPC_State_T; - -package body Total ---# own State is TheTotals; -is - - type VCCounter is array (VCDetails.TerminalPointType) of Natural; - - NullVCCounter : constant VCCounter := - VCCounter'(others => 0); - - -- if adding more entries to this type, you must alter the procedure - -- Output below to display the results, and add code in the appropriate - -- analysis routines to increment the counter(s). You must also alter - -- the aggregate in Initialize below to initialize the new counter - type TotalType is record - - -- Subprograms without errors (all subprograms have vcs). - SubprogramsWithVCs : Natural; - - -- Subprograms with errors. - SubprogramsWhereMissingSLGFile : Natural; - Subprograms_Where_VC_Analysis_Abandoned : Natural; - Subprograms_Where_DPC_Analysis_Abandoned : Natural; - - -- A subprogram with At Least One (ALO) Undischarged VC. - SubprogramsWithALOUndischargedVC : Natural; - - -- The following fields record the number of subprograms, - -- which are not necessarily fully proved, but have at least - -- one VC proved by each of the following strategies: - - -- A subprogram with At Least One (ALO) VC proved by - -- the Examiner. - SubprogramsWithALOExaminerVC : Natural; - - -- A subprogram with At Least One (ALO) VC proved by the - -- simplifier without a user defined rule. - SubprogramsWithALOSimplifierVC : Natural; - - -- A subprogram with At Least One (ALO) VC proved using - -- a using proof by contradiction. - SubprogramsWithALOContradictionVC : Natural; - - -- A subprogram with At Least One (ALO) VC proved using - -- a user defined rule. - SubprogramsWithALOUserRuleVC : Natural; - - -- A subprogram with At Least One (ALO) VC proved using - -- the Checker. - SubprogramsWithALOCheckerVC : Natural; - - -- A subprogram with At Least One (ALO) VC discharged by review - SubprogramsWithALOReviewVC : Natural; - - -- A subprogram with At Least One (ALO) false VC. - SubprogramsWithALOFalseVC : Natural; - - -- The following fields represent the use of a hierachy of - -- proof strategies: - -- Examiner -> Simplifier -> User Rules -> Checker -> Review - -- When a subprogram is proved, the strategy latest in the hierarchy - -- is considered to have been used to complete the proof, even - -- if earlier strategies have also been applied. - -- The hierachy gives a measure of the extent of the strategies - -- required in proving a subprogram. - -- The definitions of the hierarchical strategies is given below: - -- A subprogram proof is completed by the examiner if: - -- o at LEAST one VC was proved by the examiner and - -- o ZERO VCs were proved by the simplifier, - -- checker, review file or left Undischarged and - -- o the subprogram has no false VCs. - SubprogramsProvedByExaminer : Natural; - - -- A subprogram proof is completed by the simplifier if: - -- o at LEAST one VC was proved by the simplifier and - -- o ZERO VCs were proved by the checker, review file - -- or left Undischarged and - -- o the subprogram has no false VCs. - SubprogramsProvedBySimplifier : Natural; - - -- A subprogram proof is completed by a user defined proof rule if: - -- o at least one VC was proved by the simplifier and - -- o at least one user defined rule has been used in the proof of a VC and - -- o ZERO VCs were proved by the checker, review file - -- or left Undischarged and - -- o the subprogram has no false VCs. - SubprogramsProvedWithUserProofRule : Natural; - - -- A subprogram proof is completed by the checker if: - -- o at LEAST one VC was proved by the checker and - -- o ZERO VCs were proved by the review file or - -- left Undischarged and - -- o the subprogram has no false VCs. - SubprogramsProvedByChecker : Natural; - - -- A subprogram proof is completed by review if: - -- o at LEAST one VC was proved in the review file and - -- o ZERO VCs were left Undischarged and - -- o the subprogram has no false VCs. - SubprogramsProvedByReview : Natural; - - -- The following fields record the number of VCs proved by - -- each strategy grouped by the sort of origin (the terminal point) - -- of the VC. - VCsTotal : VCCounter; - VCsProvedByExaminer : VCCounter; - VCsProvedBySimplifier : VCCounter; - VCsProvedByChecker : VCCounter; - VCsProvedWithUserProofRule : VCCounter; - VCsProvedByReview : VCCounter; - VCsProvedFalse : VCCounter; - VCsUndischarged : VCCounter; - - -- Record number of subprograms with DPCs - Subprograms_With_DPCs : Natural; - - -- The following fields record the number of dead paths ZombieScope - -- has found. - Number_Of_Dead_Paths : Natural; - Subprograms_With_Dead_Paths : Natural; - end record; - - TheTotals : TotalType; - - function Sum (T : in VCCounter) return Natural - is - Result : Natural := 0; - begin - for I in VCDetails.TerminalPointType loop - Result := Result + T (I); - end loop; - return Result; - end Sum; - - -- The calculation of percentages is factored out, to keep the - -- standard and XML summary output consistent. - procedure CalcuatePercentages (TheTotals : in TotalType; - PercentUndischargedStr : out EStrings.T; - PercentProvedByExaminerStr : out EStrings.T; - PercentProvedByCheckerStr : out EStrings.T; - PercentProvedByReviewStr : out EStrings.T; - PercentSimplifiedStr : out EStrings.T; - PercentWithUserRuleStr : out EStrings.T; - PercentProvedFalseStr : out EStrings.T) - --#derives PercentUndischargedStr, - --# PercentProvedByExaminerStr, - --# PercentProvedByCheckerStr, - --# PercentProvedByReviewStr, - --# PercentSimplifiedStr, - --# PercentWithUserRuleStr, - --# PercentProvedFalseStr from TheTotals; - is - subtype Percentage is Natural range 0 .. 100; - - VCsTotal : Natural; - - PercentUndischarged : Percentage; - PercentUndischargedC : Character; - PercentProvedByExaminer : Percentage; - PercentProvedByExaminerC : Character; - PercentProvedByChecker : Percentage; - PercentProvedByCheckerC : Character; - PercentProvedByReview : Percentage; - PercentProvedByReviewC : Character; - PercentSimplified : Percentage; - PercentSimplifiedC : Character; - PercentWithUserRule : Percentage; - PercentWithUserRuleC : Character; - PercentProvedFalse : Percentage; - PercentProvedFalseC : Character; - - procedure TotalAndValueToPercentage (OverallTotal : in Natural; - Value : in Natural; - Percent : out Percentage; - PercentC : out Character) - --# derives Percent, PercentC from OverallTotal, Value; - --# pre (OverallTotal/=0); - is - PercisePercentValue : Float; - RoundedPercentValue : Percentage; - begin - PercisePercentValue := (Float (Value) * 100.0) / Float (OverallTotal); - RoundedPercentValue := Percentage (PercisePercentValue); - - case RoundedPercentValue is - - -- If the rounded percentage value is zero, but the actual - -- value is non-zero, then the rounded value is forced to be 1. - -- This behaviour ensures that a zero percentage really means - -- zero. - when 0 => - if (Value /= 0) then - Percent := 1; - - -- If the actual percent is less than 0.5 then this is - -- indicated with an appropriate leading character. - if (PercisePercentValue < 0.5) then - PercentC := '<'; - else - PercentC := ' '; - end if; - else - Percent := 0; - PercentC := ' '; - end if; - - -- If the rounded percentage value is 100, but the actual value - -- is not equal to the total, then the rounded value is forced - -- to be 99. This behaviour ensures that a hundred percent - -- really means all. - when 100 => - if (Value /= OverallTotal) then - Percent := 99; - - -- If the actual percent is greater than 99.5 then this is - -- indicated with an appropriate leading character. - if (PercisePercentValue > 99.5) then - PercentC := '>'; - else - PercentC := ' '; - end if; - else - Percent := 100; - PercentC := ' '; - end if; - - -- In all other cases, accept the rounding approximation. - when 1 .. 99 => - Percent := RoundedPercentValue; - PercentC := ' '; - end case; - end TotalAndValueToPercentage; - - procedure GeneratePercentString (Percent : in Percentage; - PercentC : in Character; - PercentStr : out EStrings.T) - --# derives PercentStr from Percent, PercentC; - is - subtype StringLength is Integer range 1 .. 10; - subtype TempString is String (StringLength); - PercentPart : TempString; - DummySuccess : Boolean; - begin - --Initialise to empty string. - PercentStr := EStrings.Empty_String; - - --# accept F, 10, DummySuccess, "Error status ignored as number always fits."; - --# accept F, 33, DummySuccess, "Error status ignored as number always fits."; - - --For alingment: if percent is one digit, add two spaces. - -- : if percent is two digits, add one spaces. - case Percent is - when 0 .. 9 => - EStrings.Append_String (E_Str => PercentStr, - Str => " "); - when 10 .. 99 => - EStrings.Append_String (E_Str => PercentStr, - Str => " "); - when 100 => - null; - end case; - - --Append the: '>','<',' ' prefix. (max length "X": 1) - EStrings.Append_Char (E_Str => PercentStr, - Ch => PercentC, - Success => DummySuccess); - - --Append the: percent number. (max length "XYYY": 4) - SPARK_IO.Put_Int_To_String (PercentPart, Percent, 1, 10); - EStrings.Append_Examiner_String - (E_Str1 => PercentStr, - E_Str2 => EStrings.Trim - (EStrings.Copy_String (Str => PercentPart))); - - --Append the: symbol '%'. (max length "XYYY%": 5) - EStrings.Append_Char (E_Str => PercentStr, - Ch => '%', - Success => DummySuccess); - - end GeneratePercentString; - - begin - - VCsTotal := Sum (TheTotals.VCsTotal); - - TotalAndValueToPercentage (VCsTotal, - Sum (TheTotals.VCsUndischarged), - PercentUndischarged, - PercentUndischargedC); - GeneratePercentString (PercentUndischarged, - PercentUndischargedC, - PercentUndischargedStr); - - TotalAndValueToPercentage (VCsTotal, - Sum (TheTotals.VCsProvedByExaminer), - PercentProvedByExaminer, - PercentProvedByExaminerC); - GeneratePercentString (PercentProvedByExaminer, - PercentProvedByExaminerC, - PercentProvedByExaminerStr); - - TotalAndValueToPercentage (VCsTotal, - Sum (TheTotals.VCsProvedByChecker), - PercentProvedByChecker, - PercentProvedByCheckerC); - GeneratePercentString (PercentProvedByChecker, - PercentProvedByCheckerC, - PercentProvedByCheckerStr); - - TotalAndValueToPercentage (VCsTotal, - Sum (TheTotals.VCsProvedByReview), - PercentProvedByReview, - PercentProvedByReviewC); - GeneratePercentString (PercentProvedByReview, - PercentProvedByReviewC, - PercentProvedByReviewStr); - - TotalAndValueToPercentage (VCsTotal, - Sum (TheTotals.VCsProvedBySimplifier), - PercentSimplified, - PercentSimplifiedC); - GeneratePercentString (PercentSimplified, - PercentSimplifiedC, - PercentSimplifiedStr); - - TotalAndValueToPercentage (VCsTotal, - Sum (TheTotals.VCsProvedWithUserProofRule), - PercentWithUserRule, - PercentWithUserRuleC); - GeneratePercentString (PercentWithUserRule, - PercentWithUserRuleC, - PercentWithUserRuleStr); - - TotalAndValueToPercentage (VCsTotal, - Sum (TheTotals.VCsProvedFalse), - PercentProvedFalse, - PercentProvedFalseC); - GeneratePercentString (PercentProvedFalse, - PercentProvedFalseC, - PercentProvedFalseStr); - end CalcuatePercentages; - - -- Never returns from this subprogram. - -- Null dependency relation used to avoid propagation - -- of FatalErrors.State impacting existing clients of Total. - -- FatalErrors.State is of little interest in this context. - procedure FatalError (Error : in FatalErrors.ErrorType) - --# derives null from Error; - is - --# hide FatalError; - begin - FatalErrors.Process (Error, ELStrings.Empty_String); - end FatalError; - - function TotalsAreBalanced return Boolean - --# global in TheTotals; - is - TotalSubprogramsProved : Natural; - TotalSubprogramsAtLeastOneFalseVC : Natural; - TotalSubprogramsNoFalseAtLeastOneUndischarged : Natural; - TotalSubprograms : Natural; - begin - -- Total all of the subprogram that have been fully proved. - TotalSubprogramsProved := ((((TheTotals.SubprogramsProvedByExaminer + - TheTotals.SubprogramsProvedBySimplifier) + - TheTotals.SubprogramsProvedWithUserProofRule) + - TheTotals.SubprogramsProvedByChecker) + - TheTotals.SubprogramsProvedByReview); - - -- Total all of the subprogram that have at least one false vc. - TotalSubprogramsAtLeastOneFalseVC := TheTotals.SubprogramsWithALOFalseVC; - - -- Total all of the subprogram that have no false vcs, and at least one - -- undischarged vc. - TotalSubprogramsNoFalseAtLeastOneUndischarged := TheTotals.SubprogramsWithALOUndischargedVC; - - -- Total all of the subprograms. - TotalSubprograms := ((TotalSubprogramsProved + - TotalSubprogramsAtLeastOneFalseVC) + - TotalSubprogramsNoFalseAtLeastOneUndischarged); - - -- Return true if the total matches the recorded total number of Subprograms - -- with VCs and false otherwise. - return (TotalSubprograms = TheTotals.SubprogramsWithVCs); - end TotalsAreBalanced; - - procedure UpdateTotals (VCG : in Boolean; DPC : in Boolean) - --# global in VCHeap.State; - --# in out TheTotals; - --# derives TheTotals from *, - --# VCG, - --# DPC, - --# VCHeap.State; - is - SubProgramIsUndischarged : Boolean; - SubProgramHasVCProvedByExaminer : Boolean; - SubProgramHasVCProvedBySimplifier : Boolean; - SubProgramHasVCProvedByContradiction : Boolean; - SubProgramHasVCProvedWithUserProofRule : Boolean; - SubProgramHasVCProvedByChecker : Boolean; - SubProgramHasVCProvedByReview : Boolean; - SubProgramHasVCProvedFalse : Boolean; - Subprogram_Contains_Dead_Paths : Boolean; - MoreVCs : Boolean; - - HeapIndex : Heap.Atom; - NextIndex : Heap.Atom; - - UnusedVCName : EStrings.T; - UnusedPathStart : EStrings.T; - UnusedPathEnd : EStrings.T; - EndType : VCDetails.TerminalPointType; - - VC_State : VCDetails.VC_State_T; - DPC_State : VCDetails.DPC_State_T; - - begin - - --Always count missing SLG files. - if VCHeap.ErrorRaised (VCDetails.MissingSLGFile) then - TheTotals.SubprogramsWhereMissingSLGFile := TheTotals.SubprogramsWhereMissingSLGFile + 1; - end if; - - --Only perform detailed analysis of subprogram if it did not have an - --associated corrupt file. - if VCHeap.ErrorRaised (VCDetails.Corrupt_VC_File) then - TheTotals.Subprograms_Where_VC_Analysis_Abandoned := - TheTotals.Subprograms_Where_VC_Analysis_Abandoned + 1; - end if; - - if VCHeap.ErrorRaised (VCDetails.Corrupt_DPC_File) then - TheTotals.Subprograms_Where_DPC_Analysis_Abandoned := - TheTotals.Subprograms_Where_DPC_Analysis_Abandoned + 1; - end if; - - MoreVCs := True; - HeapIndex := VCHeap.FirstEntry; - - SubProgramIsUndischarged := False; - SubProgramHasVCProvedByExaminer := False; - SubProgramHasVCProvedBySimplifier := False; - SubProgramHasVCProvedByContradiction := False; - SubProgramHasVCProvedByChecker := False; - SubProgramHasVCProvedWithUserProofRule := False; - SubProgramHasVCProvedByReview := False; - SubProgramHasVCProvedFalse := False; - Subprogram_Contains_Dead_Paths := False; - - if VCG and (not VCHeap.ErrorRaised (VCDetails.Corrupt_VC_File)) then - TheTotals.SubprogramsWithVCs := TheTotals.SubprogramsWithVCs + 1; - end if; - - if DPC and (not VCHeap.ErrorRaised (VCDetails.Corrupt_DPC_File)) then - TheTotals.Subprograms_With_DPCs := TheTotals.Subprograms_With_DPCs + 1; - end if; - - while MoreVCs and not Heap.IsNullPointer (HeapIndex) loop - - -- Get the details for the next VC. - --# accept F, 10, UnusedPathEnd, "UnusedPathEnd unused here" & - --# F, 10, UnusedPathStart, "UnusedPathStart unused here" & - --# F, 10, UnusedVCName, "UnusedPVCName unused here" ; - VCHeap.Details (ListIndex => HeapIndex, - VCName => UnusedVCName, - PathStart => UnusedPathStart, - PathEnd => UnusedPathEnd, - EndType => EndType, - VC_State => VC_State, - DPC_State => DPC_State); - - --# end accept; - - --# accept F, 41, "Expression is stable"; - if VCG and (not VCHeap.ErrorRaised (VCDetails.Corrupt_VC_File)) then - --# end accept; - TheTotals.VCsTotal (EndType) := TheTotals.VCsTotal (EndType) + 1; - - case VC_State is - when VCDetails.VC_False => - TheTotals.VCsProvedFalse (EndType) := - TheTotals.VCsProvedFalse (EndType) + 1; - SubProgramHasVCProvedFalse := True; - SubProgramIsUndischarged := True; - when VCDetails.VC_Proved_By_Examiner => - SubProgramHasVCProvedByExaminer := True; - TheTotals.VCsProvedByExaminer (EndType) := - TheTotals.VCsProvedByExaminer (EndType) + 1; - when VCDetails.VC_Proved_By_Inference => - SubProgramHasVCProvedBySimplifier := True; - TheTotals.VCsProvedBySimplifier (EndType) := - TheTotals.VCsProvedBySimplifier (EndType) + 1; - when VCDetails.VC_Proved_By_Contradiction => - SubProgramHasVCProvedByContradiction := True; - SubProgramHasVCProvedBySimplifier := True; - TheTotals.VCsProvedBySimplifier (EndType) := - TheTotals.VCsProvedBySimplifier (EndType) + 1; - when VCDetails.VC_Proved_By_Checker => - SubProgramHasVCProvedByChecker := True; - - TheTotals.VCsProvedByChecker (EndType) := - TheTotals.VCsProvedByChecker (EndType) + 1; - when VCDetails.VC_Proved_By_Review => - SubProgramHasVCProvedByReview := True; - - TheTotals.VCsProvedByReview (EndType) := - TheTotals.VCsProvedByReview (EndType) + 1; - when VCDetails.VC_Proved_Using_User_Proof_Rules => - SubProgramHasVCProvedWithUserProofRule := True; - SubProgramHasVCProvedBySimplifier := True; - TheTotals.VCsProvedWithUserProofRule (EndType) := - TheTotals.VCsProvedWithUserProofRule (EndType) + 1; - TheTotals.VCsProvedBySimplifier (EndType) := - TheTotals.VCsProvedBySimplifier (EndType) + 1; - when VCDetails.VC_SIV_Not_Present | VCDetails.VC_Undischarged => - TheTotals.VCsUndischarged (EndType) := - TheTotals.VCsUndischarged (EndType) + 1; - SubProgramIsUndischarged := True; - when others => -- VC_Not_Present - -- No VC is present. - null; - end case; - end if; - - --# accept F, 41, "Expression is stable"; - if DPC and (not VCHeap.ErrorRaised (VCDetails.Corrupt_DPC_File)) then - --# end accept; - if DPC_State = VCDetails.DPC_Dead then - -- Update the total number of subprograms containing - -- dead paths. - if not Subprogram_Contains_Dead_Paths then - TheTotals.Subprograms_With_Dead_Paths := - TheTotals.Subprograms_With_Dead_Paths + 1; - end if; - Subprogram_Contains_Dead_Paths := True; - -- Update the total number of dead paths found. - TheTotals.Number_Of_Dead_Paths := - TheTotals.Number_Of_Dead_Paths + 1; - end if; - end if; - - VCHeap.Next (AfterThis => HeapIndex, - Success => MoreVCs, - NextOne => NextIndex); - - HeapIndex := NextIndex; - - end loop; - - --# assert True; - - -- Update the At Least One Counts - if SubProgramIsUndischarged then - if SubProgramHasVCProvedFalse then - TheTotals.SubprogramsWithALOFalseVC := - TheTotals.SubprogramsWithALOFalseVC + 1; - else - TheTotals.SubprogramsWithALOUndischargedVC := - TheTotals.SubprogramsWithALOUndischargedVC + 1; - end if; - end if; - - --# assert True; - - - if SubProgramHasVCProvedByExaminer then - TheTotals.SubprogramsWithALOExaminerVC := - TheTotals.SubprogramsWithALOExaminerVC + 1; - end if; - - --# assert True; - - if SubProgramHasVCProvedBySimplifier then - TheTotals.SubprogramsWithALOSimplifierVC := - TheTotals.SubprogramsWithALOSimplifierVC + 1; - end if; - - --# assert True; - - if SubProgramHasVCProvedByContradiction then - TheTotals.SubprogramsWithALOContradictionVC := - TheTotals.SubprogramsWithALOContradictionVC + 1; - end if; - - --# assert True; - - if SubProgramHasVCProvedWithUserProofRule then - TheTotals.SubprogramsWithALOUserRuleVC := - TheTotals.SubprogramsWithALOUserRuleVC + 1; - end if; - - --# assert True; - - if SubProgramHasVCProvedByChecker then - TheTotals.SubprogramsWithALOCheckerVC := - TheTotals.SubprogramsWithALOCheckerVC + 1; - end if; - - --# assert True; - - if SubProgramHasVCProvedByReview then - TheTotals.SubprogramsWithALOReviewVC := - TheTotals.SubprogramsWithALOReviewVC + 1; - end if; - - --# assert True; - - -- Update the proof strategy use hierarchy (See declaration of TotalType) - -- Examiner -> Simplifier -> User Rules -> Checker -> Review - if not SubProgramIsUndischarged then - if SubProgramHasVCProvedByReview then - TheTotals.SubprogramsProvedByReview := - TheTotals.SubprogramsProvedByReview + 1; - - elsif SubProgramHasVCProvedByChecker then - TheTotals.SubprogramsProvedByChecker := - TheTotals.SubprogramsProvedByChecker + 1; - - elsif SubProgramHasVCProvedWithUserProofRule then - TheTotals.SubprogramsProvedWithUserProofRule := - TheTotals.SubprogramsProvedWithUserProofRule + 1; - - elsif SubProgramHasVCProvedBySimplifier then - TheTotals.SubprogramsProvedBySimplifier := - TheTotals.SubprogramsProvedBySimplifier + 1; - - elsif SubProgramHasVCProvedByExaminer then - TheTotals.SubprogramsProvedByExaminer := - TheTotals.SubprogramsProvedByExaminer + 1; - end if; - end if; - - --# assert True; - - --# accept F, 33, UnusedPathEnd, "UnusedPathEnd unused here" & - --# F, 33, UnusedPathStart, "UnusedPathStart unused here" & - --# F, 33, UnusedVCName, "UnusedPVCName unused here"; - end UpdateTotals; - - procedure Output (ReportFile : in SPARK_IO.File_Type; - TempFile : in out SPARK_IO.File_Type; - TempFalseFile : in out SPARK_IO.File_Type; - TempContraFile : in out SPARK_IO.File_Type; - TempUserFile : in out SPARK_IO.File_Type; - TempRluErrorFile : in out SPARK_IO.File_Type; - TempRluUsedFile : in out SPARK_IO.File_Type; - TempPRVerrFile : in out SPARK_IO.File_Type; - TempWarnErrorFile : in out SPARK_IO.File_Type; - TempSDPErrorFile : in out SPARK_IO.File_Type; - TempDPCErrorFile : in out SPARK_IO.File_Type) - --# global in CommandLine.Data; - --# in TheTotals; - --# in out SPARK_IO.File_Sys; - --# derives SPARK_IO.File_Sys from *, - --# CommandLine.Data, - --# ReportFile, - --# TempContraFile, - --# TempDPCErrorFile, - --# TempFalseFile, - --# TempFile, - --# TempPRVerrFile, - --# TempRluErrorFile, - --# TempRluUsedFile, - --# TempSDPErrorFile, - --# TempUserFile, - --# TempWarnErrorFile, - --# TheTotals & - --# TempContraFile, - --# TempDPCErrorFile, - --# TempFalseFile, - --# TempFile, - --# TempPRVerrFile, - --# TempRluErrorFile, - --# TempRluUsedFile, - --# TempSDPErrorFile, - --# TempUserFile, - --# TempWarnErrorFile from *; - is - PercentUndischargedStr : EStrings.T; - PercentProvedByExaminerStr : EStrings.T; - PercentProvedByCheckerStr : EStrings.T; - PercentProvedByReviewStr : EStrings.T; - PercentSimplifiedStr : EStrings.T; - PercentWithUserRuleStr : EStrings.T; - PercentProvedFalseStr : EStrings.T; - - TotalSubprogramsProved : Natural; - - TempStoreInt : Integer; - TempStoreString : EStrings.T; - TempStoreBool : Boolean; - TempStatus : SPARK_IO.File_Status; - - - begin - SPARK_IO.Put_Line (ReportFile, Banner.MajorSeparatorLine, 0); - SPARK_IO.Put_Line (ReportFile, "Summary:", 0); - SPARK_IO.New_Line (ReportFile, 1); - - --# accept F, 10, TempStatus, "TempStatus not used here" & - --# F, 10, TempStoreBool, "TempStoreBool not used here"; - - -- print out the names of files containing warnings or errors - SPARK_IO.Reset (TempWarnErrorFile, SPARK_IO.In_File, TempStatus); - if not SPARK_IO.End_Of_File (TempWarnErrorFile) then - SPARK_IO.Put_Line (ReportFile, "***WARNING: The following files, or their absence, raised warnings or errors:", 0); - SPARK_IO.New_Line (ReportFile, 1); - while not SPARK_IO.End_Of_File (TempWarnErrorFile) loop - SPARK_IO.Get_Integer (TempWarnErrorFile, TempStoreInt, 4, TempStoreBool); - SPARK_IO.Put_Integer (ReportFile, TempStoreInt, 4, 10); - SPARK_IO.Put_String (ReportFile, " ", 0); - EStrings.Get_Line (File => TempWarnErrorFile, - E_Str => TempStoreString); - EStrings.Put_String (File => ReportFile, - E_Str => TempStoreString); - SPARK_IO.New_Line (ReportFile, 1); - end loop; - SPARK_IO.New_Line (ReportFile, 1); - end if; - - --# assert True; - - -- print out the names of any user rule files containing syntax errors - SPARK_IO.Reset (TempRluErrorFile, SPARK_IO.In_File, TempStatus); - if not SPARK_IO.End_Of_File (TempRluErrorFile) then - SPARK_IO.Put_Line (ReportFile, "***WARNING: The following user defined rule files contain syntax errors:", 0); - SPARK_IO.New_Line (ReportFile, 1); - while not SPARK_IO.End_Of_File (TempRluErrorFile) loop - -- Note no number output here (not possible to know earlier) - EStrings.Get_Line (File => TempRluErrorFile, - E_Str => TempStoreString); - -- Switching back and forth between Append and Input modes - -- causes empty lines to be created - if EStrings.Get_Length (E_Str => TempStoreString) /= 0 then - SPARK_IO.Put_String (ReportFile, " ", 0); - EStrings.Put_String (File => ReportFile, - E_Str => TempStoreString); - SPARK_IO.New_Line (ReportFile, 1); - end if; - end loop; - SPARK_IO.New_Line (ReportFile, 1); - end if; - - --# assert True; - - -- print out any used user-defined rule files - SPARK_IO.Reset (TempRluUsedFile, SPARK_IO.In_File, TempStatus); - if not SPARK_IO.End_Of_File (TempRluUsedFile) then - SPARK_IO.Put_Line (ReportFile, "The following user-defined rule files have been used:", 0); - SPARK_IO.New_Line (ReportFile, 1); - while not SPARK_IO.End_Of_File (TempRluUsedFile) loop - -- Note no number output here (difficult to calculate earlier) - EStrings.Get_Line (File => TempRluUsedFile, - E_Str => TempStoreString); - -- Switching back and forth between Append and Input modes - -- causes empty lines to be created - if EStrings.Get_Length (E_Str => TempStoreString) /= 0 then - SPARK_IO.Put_String (ReportFile, " ", 0); - EStrings.Put_String (File => ReportFile, - E_Str => TempStoreString); - SPARK_IO.New_Line (ReportFile, 1); - end if; - end loop; - SPARK_IO.New_Line (ReportFile, 1); - end if; - - --# assert True; - - -- print out the file names and numbers of any false VC - SPARK_IO.Reset (TempFalseFile, SPARK_IO.In_File, TempStatus); - if not SPARK_IO.End_Of_File (TempFalseFile) then - SPARK_IO.Put_Line (ReportFile, "The following subprograms have VCs proved false:", 0); - SPARK_IO.New_Line (ReportFile, 1); - while not SPARK_IO.End_Of_File (TempFalseFile) loop - SPARK_IO.Get_Integer (TempFalseFile, TempStoreInt, 4, TempStoreBool); - SPARK_IO.Put_Integer (ReportFile, TempStoreInt, 4, 10); - SPARK_IO.Put_String (ReportFile, " ", 0); - EStrings.Get_Line (File => TempFalseFile, - E_Str => TempStoreString); - EStrings.Put_String (File => ReportFile, - E_Str => TempStoreString); - SPARK_IO.New_Line (ReportFile, 1); - end loop; - SPARK_IO.New_Line (ReportFile, 1); - end if; - - --# assert True; - - -- print out the file names and numbers of any undischarged VC (excluding those proved false) - SPARK_IO.Reset (TempFile, SPARK_IO.In_File, TempStatus); - if not SPARK_IO.End_Of_File (TempFile) then - SPARK_IO.Put_Line (ReportFile, "The following subprograms have undischarged VCs (excluding those proved false):", 0); - SPARK_IO.New_Line (ReportFile, 1); - while not SPARK_IO.End_Of_File (TempFile) loop - SPARK_IO.Get_Integer (TempFile, TempStoreInt, 4, TempStoreBool); - SPARK_IO.Put_Integer (ReportFile, TempStoreInt, 4, 10); - SPARK_IO.Put_String (ReportFile, " ", 0); - EStrings.Get_Line (File => TempFile, - E_Str => TempStoreString); - EStrings.Put_String (File => ReportFile, - E_Str => TempStoreString); - SPARK_IO.New_Line (ReportFile, 1); - end loop; - SPARK_IO.New_Line (ReportFile, 1); - end if; - - --# assert True; - - -- print out the file names and numbers of any VC proved by contradiction - SPARK_IO.Reset (TempContraFile, SPARK_IO.In_File, TempStatus); - if not SPARK_IO.End_Of_File (TempContraFile) then - SPARK_IO.Put_Line (ReportFile, "The following subprograms have VCs proved by contradiction:", 0); - SPARK_IO.New_Line (ReportFile, 1); - while not SPARK_IO.End_Of_File (TempContraFile) loop - SPARK_IO.Get_Integer (TempContraFile, TempStoreInt, 4, TempStoreBool); - SPARK_IO.Put_Integer (ReportFile, TempStoreInt, 4, 10); - SPARK_IO.Put_String (ReportFile, " ", 0); - EStrings.Get_Line (File => TempContraFile, - E_Str => TempStoreString); - EStrings.Put_String (File => ReportFile, - E_Str => TempStoreString); - SPARK_IO.New_Line (ReportFile, 1); - end loop; - SPARK_IO.New_Line (ReportFile, 1); - end if; - - --# assert True; - - -- print out the file names and numbers of any VC proved by a user-defined proof rule - SPARK_IO.Reset (TempUserFile, SPARK_IO.In_File, TempStatus); - if not SPARK_IO.End_Of_File (TempUserFile) then - SPARK_IO.Put_Line (ReportFile, "The following subprograms have VCs proved using a user-defined proof rule:", 0); - SPARK_IO.New_Line (ReportFile, 1); - while not SPARK_IO.End_Of_File (TempUserFile) loop - SPARK_IO.Get_Integer (TempUserFile, TempStoreInt, 4, TempStoreBool); - SPARK_IO.Put_Integer (ReportFile, TempStoreInt, 4, 10); - SPARK_IO.Put_String (ReportFile, " ", 0); - EStrings.Get_Line (File => TempUserFile, - E_Str => TempStoreString); - EStrings.Put_String (File => ReportFile, - E_Str => TempStoreString); - SPARK_IO.New_Line (ReportFile, 1); - end loop; - SPARK_IO.New_Line (ReportFile, 1); - end if; - - --# assert True; - - -- print out the file names and numbers of any files with review errors - SPARK_IO.Reset (TempPRVerrFile, SPARK_IO.In_File, TempStatus); - if not SPARK_IO.End_Of_File (TempPRVerrFile) then - SPARK_IO.Put_Line (ReportFile, "***WARNING: The PRV file(s) associated with the following subprograms may be out of date", 0); - SPARK_IO.Put_Line (ReportFile, "The following subprograms have review files containing VCs already proved elsewhere:", 0); - SPARK_IO.New_Line (ReportFile, 1); - while not SPARK_IO.End_Of_File (TempPRVerrFile) loop - SPARK_IO.Get_Integer (TempPRVerrFile, TempStoreInt, 4, TempStoreBool); - SPARK_IO.Put_Integer (ReportFile, TempStoreInt, 4, 10); - SPARK_IO.Put_String (ReportFile, " ", 0); - EStrings.Get_Line (File => TempPRVerrFile, - E_Str => TempStoreString); - EStrings.Put_String (File => ReportFile, - E_Str => TempStoreString); - SPARK_IO.New_Line (ReportFile, 1); - end loop; - SPARK_IO.New_Line (ReportFile, 1); - end if; - - -- print out the names of any missing SDP files - SPARK_IO.Reset (TempSDPErrorFile, SPARK_IO.In_File, TempStatus); - if not SPARK_IO.End_Of_File (TempSDPErrorFile) then - SPARK_IO.Put_Line (ReportFile, "***WARNING: The following DPC files have not been ZombieScoped:", 0); - SPARK_IO.New_Line (ReportFile, 1); - while not SPARK_IO.End_Of_File (TempSDPErrorFile) loop - EStrings.Get_Line (File => TempSDPErrorFile, - E_Str => TempStoreString); - -- Switching back and forth between Append and Input modes - -- causes empty lines to be created - if EStrings.Get_Length (E_Str => TempStoreString) /= 0 then - SPARK_IO.Put_String (ReportFile, " ", 0); - EStrings.Put_String (File => ReportFile, - E_Str => TempStoreString); - SPARK_IO.New_Line (ReportFile, 1); - end if; - end loop; - SPARK_IO.New_Line (ReportFile, 1); - end if; - - -- print out the names of any missing DPC files - SPARK_IO.Reset (TempDPCErrorFile, SPARK_IO.In_File, TempStatus); - if not SPARK_IO.End_Of_File (TempDPCErrorFile) then - SPARK_IO.Put_Line (ReportFile, "***WARNING: The following DPC files are missing:", 0); - SPARK_IO.New_Line (ReportFile, 1); - while not SPARK_IO.End_Of_File (TempDPCErrorFile) loop - EStrings.Get_Line (File => TempDPCErrorFile, - E_Str => TempStoreString); - -- Switching back and forth between Append and Input modes - -- causes empty lines to be created - if EStrings.Get_Length (E_Str => TempStoreString) /= 0 then - SPARK_IO.Put_String (ReportFile, " ", 0); - EStrings.Put_String (File => ReportFile, - E_Str => TempStoreString); - SPARK_IO.New_Line (ReportFile, 1); - end if; - end loop; - SPARK_IO.New_Line (ReportFile, 1); - end if; - --# end accept; - - --# assert True; - - -- Print a summary of the number of subprograms conatining at - -- least one instance of the following: - SPARK_IO.Put_Line - (ReportFile, - "Proof strategies used by subprograms", 0); - SPARK_IO.Put_Line - (ReportFile, - "-------------------------------------------------------------------------", 0); - SPARK_IO.Put_String - (ReportFile, - "Total subprograms with at least one VC proved by examiner: ", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.SubprogramsWithALOExaminerVC, 4, 10); - SPARK_IO.New_Line (ReportFile, 1); - - SPARK_IO.Put_String - (ReportFile, - "Total subprograms with at least one VC proved by simplifier: ", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.SubprogramsWithALOSimplifierVC, 4, 10); - SPARK_IO.New_Line (ReportFile, 1); - - SPARK_IO.Put_String - (ReportFile, - "Total subprograms with at least one VC proved by contradiction: ", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.SubprogramsWithALOContradictionVC, 4, 10); - SPARK_IO.New_Line (ReportFile, 1); - - SPARK_IO.Put_String - (ReportFile, - "Total subprograms with at least one VC proved with user proof rule: ", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.SubprogramsWithALOUserRuleVC, 4, 10); - SPARK_IO.New_Line (ReportFile, 1); - - SPARK_IO.Put_String - (ReportFile, - "Total subprograms with at least one VC proved using checker: ", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.SubprogramsWithALOCheckerVC, 4, 10); - SPARK_IO.New_Line (ReportFile, 1); - - SPARK_IO.Put_String - (ReportFile, - "Total subprograms with at least one VC discharged by review: ", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.SubprogramsWithALOReviewVC, 4, 10); - SPARK_IO.New_Line (ReportFile, 1); - - --# assert True; - - -- Print out hierarchy of proof strategy use (see declaration of TotalType) - -- Examiner -> Simplifier -> User Rules -> Checker -> Review - SPARK_IO.New_Line (ReportFile, 1); - SPARK_IO.Put_Line - (ReportFile, - "Maximum extent of strategies used for fully proved subprograms:", 0); - SPARK_IO.Put_Line - (ReportFile, - "-------------------------------------------------------------------------", 0); - SPARK_IO.Put_String - (ReportFile, - "Total subprograms with proof completed by examiner: ", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.SubprogramsProvedByExaminer, 4, 10); - SPARK_IO.New_Line (ReportFile, 1); - - SPARK_IO.Put_String - (ReportFile, - "Total subprograms with proof completed by simplifier: ", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.SubprogramsProvedBySimplifier, 4, 10); - SPARK_IO.New_Line (ReportFile, 1); - - SPARK_IO.Put_String - (ReportFile, - "Total subprograms with proof completed with user defined rules: ", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.SubprogramsProvedWithUserProofRule, 4, 10); - SPARK_IO.New_Line (ReportFile, 1); - - SPARK_IO.Put_String - (ReportFile, - "Total subprograms with proof completed by checker: ", 0); - SPARK_IO.Put_Integer (ReportFile, TheTotals.SubprogramsProvedByChecker, 4, 10); - SPARK_IO.New_Line (ReportFile, 1); - - SPARK_IO.Put_String - (ReportFile, - "Total subprograms with VCs discharged by review: ", 0); - SPARK_IO.Put_Integer (ReportFile, TheTotals.SubprogramsProvedByReview, 4, 10); - SPARK_IO.New_Line (ReportFile, 1); - - TotalSubprogramsProved := (((( - TheTotals.SubprogramsProvedByExaminer + - TheTotals.SubprogramsProvedBySimplifier) + - TheTotals.SubprogramsProvedWithUserProofRule) + - TheTotals.SubprogramsProvedByChecker) + - TheTotals.SubprogramsProvedByReview); - - --# assert True; - - SPARK_IO.New_Line (ReportFile, 1); - SPARK_IO.Put_Line - (ReportFile, - "Overall subprogram summary:", 0); - SPARK_IO.Put_Line - (ReportFile, - "-------------------------------------------------------------------------", 0); - SPARK_IO.Put_String - (ReportFile, - "Total subprograms fully proved: ", 0); - SPARK_IO.Put_Integer - (ReportFile, TotalSubprogramsProved, 4, 10); - SPARK_IO.New_Line (ReportFile, 1); - - SPARK_IO.Put_String - (ReportFile, - "Total subprograms with at least one undischarged VC: ", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.SubprogramsWithALOUndischargedVC, 4, 10); - - if TheTotals.SubprogramsWithALOUndischargedVC > 0 then - SPARK_IO.Put_String (ReportFile, " <<<", 0); - end if; - SPARK_IO.New_Line (ReportFile, 1); - - SPARK_IO.Put_String - (ReportFile, - "Total subprograms with at least one false VC: ", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.SubprogramsWithALOFalseVC, 4, 10); - - if TheTotals.SubprogramsWithALOFalseVC > 0 then - SPARK_IO.Put_String (ReportFile, " <<<", 0); - end if; - SPARK_IO.New_Line (ReportFile, 1); - - SPARK_IO.Put_String - (ReportFile, - " -----", 0); - - SPARK_IO.New_Line (ReportFile, 1); - SPARK_IO.Put_String - (ReportFile, - "Total subprograms for which VCs have been generated: ", 0); - SPARK_IO.Put_Integer (ReportFile, TheTotals.SubprogramsWithVCs, 4, 10); - SPARK_IO.New_Line (ReportFile, 2); - - -- Only report errors if there are some. - if (TheTotals.Subprograms_Where_VC_Analysis_Abandoned > 0) or - (TheTotals.Subprograms_Where_DPC_Analysis_Abandoned > 0) or - (TheTotals.SubprogramsWhereMissingSLGFile > 0) then - SPARK_IO.Put_Line - (ReportFile, - "WARNING: Overall error summary:", 0); - SPARK_IO.Put_Line - (ReportFile, - "-------------------------------------------------------------------------", 0); - SPARK_IO.Put_String - (ReportFile, - "Total simplified subprograms with missing slg file: ", 0); - SPARK_IO.Put_Integer (ReportFile, TheTotals.SubprogramsWhereMissingSLGFile, 7, 10); - SPARK_IO.New_Line (ReportFile, 1); - SPARK_IO.Put_String - (ReportFile, - "Total subprograms where VC analysis was abandoned due to errors: ", 0); - SPARK_IO.Put_Integer (ReportFile, TheTotals.Subprograms_Where_VC_Analysis_Abandoned, 4, 10); - SPARK_IO.New_Line (ReportFile, 1); - SPARK_IO.Put_String - (ReportFile, - "Total subprograms where DPC analysis was abandoned due to errors: ", 0); - SPARK_IO.Put_Integer (ReportFile, TheTotals.Subprograms_Where_DPC_Analysis_Abandoned, 3, 10); - SPARK_IO.New_Line (ReportFile, 2); - else - -- One blank line between each table in this group, but double blank line - -- after the last table. - SPARK_IO.New_Line (ReportFile, 1); - end if; - - -- The sum of the subprograms fully proved, - -- the subprograms with at least undischarged VC and - -- the subprograms with at least 1 false VC must equal - -- the number of subprograms for which VCs have been generated. - - SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1); - - --# assert TotalSubprogramsProved + - --# TheTotals.SubprogramsWithALOUndischargedVC + - --# TheTotals.SubprogramsWithALOFalseVC - --# = TheTotals.SubprogramsWithVCs; - - -- Check the totals are balanced. - if not TotalsAreBalanced then - FatalError (FatalErrors.SubprogramTotalsInconsistent); - end if; - - --# assert True; - - SPARK_IO.Put_Line - (ReportFile, - "ZombieScope Summary:", 0); - SPARK_IO.Put_Line - (ReportFile, - "-------------------------------------------------------------------------", 0); - SPARK_IO.Put_String - (ReportFile, - "Total subprograms for which DPCs have been generated:", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.Subprograms_With_DPCs, 20, 10); - SPARK_IO.New_Line (ReportFile, 1); - SPARK_IO.Put_String - (ReportFile, - "Total number subprograms with dead paths found:", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.Subprograms_With_Dead_Paths, 26, 10); - SPARK_IO.New_Line (ReportFile, 1); - SPARK_IO.Put_String - (ReportFile, - "Total number of dead paths found:", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.Number_Of_Dead_Paths, 40, 10); - SPARK_IO.New_Line (ReportFile, 3); - - -- Issue warning message if some DPC files have not been analysed. - - --# assert True; - - SPARK_IO.Put_Line - (ReportFile, - "VC summary:", 0); - SPARK_IO.Put_Line - (ReportFile, - "-------------------------------------------------------------------------", 0); - SPARK_IO.Put_Line - (ReportFile, - "Note: U/R denotes where the Simplifier has proved VCs using one or more " & - "user-", 0); - SPARK_IO.Put_Line - (ReportFile, "defined proof rules.", 0); - - SPARK_IO.New_Line (ReportFile, 1); - - SPARK_IO.Put_String - (ReportFile, - "Total VCs by type: ", 0); - - SPARK_IO.New_Line (ReportFile, 1); - - SPARK_IO.Put_Line - (ReportFile, - " -----------Proved By Or Using------------", 0); - SPARK_IO.Put_String - (ReportFile, - " Total Examiner Simp(U/R) Checker Review False Undiscgd", 0); - - SPARK_IO.New_Line (ReportFile, 1); - - SPARK_IO.Put_String - (ReportFile, "Assert or Post: ", 0); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsTotal (VCDetails.Assert_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedByExaminer (VCDetails.Assert_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedBySimplifier (VCDetails.Assert_Point), 7, 10); - - if TheTotals.VCsProvedWithUserProofRule (VCDetails.Assert_Point) > 0 then - SPARK_IO.Put_String (ReportFile, "(", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedWithUserProofRule (VCDetails.Assert_Point), 4, 10); - SPARK_IO.Put_String (ReportFile, ")", 0); - else - SPARK_IO.Put_String (ReportFile, " ", 0); - end if; - - --# assert True; - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedByChecker (VCDetails.Assert_Point), 9, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedByReview (VCDetails.Assert_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedFalse (VCDetails.Assert_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsUndischarged (VCDetails.Assert_Point), 8, 10); - - SPARK_IO.New_Line (ReportFile, 1); - - SPARK_IO.Put_String - (ReportFile, "Precondition check:", 0); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsTotal (VCDetails.Precondition_Check_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedByExaminer (VCDetails.Precondition_Check_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedBySimplifier (VCDetails.Precondition_Check_Point), 7, 10); - - if TheTotals.VCsProvedWithUserProofRule (VCDetails.Precondition_Check_Point) > 0 then - SPARK_IO.Put_String (ReportFile, "(", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedWithUserProofRule (VCDetails.Precondition_Check_Point), 4, 10); - SPARK_IO.Put_String (ReportFile, ")", 0); - else - SPARK_IO.Put_String (ReportFile, " ", 0); - end if; - - --# assert True; - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedByChecker (VCDetails.Precondition_Check_Point), 9, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedByReview (VCDetails.Precondition_Check_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedFalse (VCDetails.Precondition_Check_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsUndischarged (VCDetails.Precondition_Check_Point), 8, 10); - - SPARK_IO.New_Line (ReportFile, 1); - - SPARK_IO.Put_String - (ReportFile, "Check statement: ", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsTotal (VCDetails.Check_Statement_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedByExaminer (VCDetails.Check_Statement_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedBySimplifier (VCDetails.Check_Statement_Point), 7, 10); - - if TheTotals.VCsProvedWithUserProofRule (VCDetails.Check_Statement_Point) > 0 then - SPARK_IO.Put_String (ReportFile, "(", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedWithUserProofRule (VCDetails.Check_Statement_Point), 4, 10); - SPARK_IO.Put_String (ReportFile, ")", 0); - else - SPARK_IO.Put_String (ReportFile, " ", 0); - end if; - - --# assert True; - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedByChecker (VCDetails.Check_Statement_Point), 9, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedByReview (VCDetails.Check_Statement_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedFalse (VCDetails.Check_Statement_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsUndischarged (VCDetails.Check_Statement_Point), 8, 10); - - SPARK_IO.New_Line (ReportFile, 1); - - SPARK_IO.Put_String - (ReportFile, "Runtime check: ", 0); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsTotal (VCDetails.Runtime_Check_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedByExaminer (VCDetails.Runtime_Check_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedBySimplifier (VCDetails.Runtime_Check_Point), 7, 10); - - if TheTotals.VCsProvedWithUserProofRule (VCDetails.Runtime_Check_Point) > 0 then - SPARK_IO.Put_String (ReportFile, "(", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedWithUserProofRule (VCDetails.Runtime_Check_Point), 4, 10); - SPARK_IO.Put_String (ReportFile, ")", 0); - else - SPARK_IO.Put_String (ReportFile, " ", 0); - end if; - - --# assert True; - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedByChecker (VCDetails.Runtime_Check_Point), 9, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedByReview (VCDetails.Runtime_Check_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedFalse (VCDetails.Runtime_Check_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsUndischarged (VCDetails.Runtime_Check_Point), 8, 10); - - SPARK_IO.New_Line (ReportFile, 1); - - - SPARK_IO.Put_String - (ReportFile, "Refinement VCs: ", 0); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsTotal (VCDetails.Refinement_VC_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedByExaminer (VCDetails.Refinement_VC_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedBySimplifier (VCDetails.Refinement_VC_Point), 7, 10); - - if TheTotals.VCsProvedWithUserProofRule (VCDetails.Refinement_VC_Point) > 0 then - SPARK_IO.Put_String (ReportFile, "(", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedWithUserProofRule (VCDetails.Refinement_VC_Point), 4, 10); - SPARK_IO.Put_String (ReportFile, ")", 0); - else - SPARK_IO.Put_String (ReportFile, " ", 0); - end if; - - --# assert True; - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedByChecker (VCDetails.Refinement_VC_Point), 9, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedByReview (VCDetails.Refinement_VC_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedFalse (VCDetails.Refinement_VC_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsUndischarged (VCDetails.Refinement_VC_Point), 8, 10); - - SPARK_IO.New_Line (ReportFile, 1); - - SPARK_IO.Put_String - (ReportFile, "Inheritance VCs: ", 0); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsTotal (VCDetails.Inheritance_VC_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedByExaminer (VCDetails.Inheritance_VC_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedBySimplifier (VCDetails.Inheritance_VC_Point), 7, 10); - - if TheTotals.VCsProvedWithUserProofRule (VCDetails.Inheritance_VC_Point) > 0 then - SPARK_IO.Put_String (ReportFile, "(", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedWithUserProofRule (VCDetails.Inheritance_VC_Point), 4, 10); - SPARK_IO.Put_String (ReportFile, ")", 0); - else - SPARK_IO.Put_String (ReportFile, " ", 0); - end if; - - --# assert True; - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedByChecker (VCDetails.Undetermined_Point), 9, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedFalse (VCDetails.Inheritance_VC_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedByReview (VCDetails.Inheritance_VC_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsUndischarged (VCDetails.Inheritance_VC_Point), 8, 10); - - SPARK_IO.New_Line (ReportFile, 1); - - -- Assuming a well-structured set of VCG, SIV and PLG files, - -- the number of Undetermined_Point VCs should always be - -- zero. - -- - -- A corrupt VCG file might lead to an Undetermined_Point - -- VC, so we only output the total if it's non-zero... - - if TheTotals.VCsTotal (VCDetails.Undetermined_Point) > 0 then - SPARK_IO.Put_String - (ReportFile, "Undetermined: ", 0); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsTotal (VCDetails.Undetermined_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedByExaminer (VCDetails.Undetermined_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedBySimplifier (VCDetails.Undetermined_Point), 7, 10); - - if TheTotals.VCsProvedWithUserProofRule (VCDetails.Undetermined_Point) > 0 then - SPARK_IO.Put_String (ReportFile, "(", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedWithUserProofRule (VCDetails.Undetermined_Point), 4, 10); - SPARK_IO.Put_String (ReportFile, ")", 0); - else - SPARK_IO.Put_String (ReportFile, " ", 0); - end if; - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedByChecker (VCDetails.Undetermined_Point), 9, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedByReview (VCDetails.Undetermined_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsProvedFalse (VCDetails.Undetermined_Point), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, TheTotals.VCsUndischarged (VCDetails.Undetermined_Point), 8, 10); - - SPARK_IO.New_Line (ReportFile, 1); - end if; - - --# assert True; - - SPARK_IO.Put_String - (ReportFile, Banner.MajorSeparatorLine, 0); - - SPARK_IO.New_Line (ReportFile, 1); - - SPARK_IO.Put_String - (ReportFile, "Totals: ", 0); - - SPARK_IO.Put_Integer - (ReportFile, Sum (TheTotals.VCsTotal), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, Sum (TheTotals.VCsProvedByExaminer), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, Sum (TheTotals.VCsProvedBySimplifier), 7, 10); - - if Sum (TheTotals.VCsProvedWithUserProofRule) > 0 then - SPARK_IO.Put_String (ReportFile, "(", 0); - SPARK_IO.Put_Integer - (ReportFile, Sum (TheTotals.VCsProvedWithUserProofRule), 4, 10); - SPARK_IO.Put_String (ReportFile, ")", 0); - else - SPARK_IO.Put_String (ReportFile, " ", 0); - end if; - - --# assert True; - - SPARK_IO.Put_Integer - (ReportFile, Sum (TheTotals.VCsProvedByChecker), 9, 10); - - SPARK_IO.Put_Integer - (ReportFile, Sum (TheTotals.VCsProvedByReview), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, Sum (TheTotals.VCsProvedFalse), 7, 10); - - SPARK_IO.Put_Integer - (ReportFile, Sum (TheTotals.VCsUndischarged), 8, 10); - - if Sum (TheTotals.VCsUndischarged) > 0 then - SPARK_IO.Put_String (ReportFile, " <<<", 0); - end if; - - --# assert True; - - SPARK_IO.New_Line (ReportFile, 1); - - if CommandLine.Data.OutputPercentUndischarged and then - Sum (TheTotals.VCsTotal) /= 0 then - - CalcuatePercentages (TheTotals, - PercentUndischargedStr, - PercentProvedByExaminerStr, - PercentProvedByCheckerStr, - PercentProvedByReviewStr, - PercentSimplifiedStr, - PercentWithUserRuleStr, - PercentProvedFalseStr); - - SPARK_IO.Put_String (ReportFile, "% Totals: ", 0); - EStrings.Put_String (File => ReportFile, - E_Str => PercentProvedByExaminerStr); - SPARK_IO.Put_String (ReportFile, " ", 0); - EStrings.Put_String (File => ReportFile, - E_Str => PercentSimplifiedStr); - - if Sum (TheTotals.VCsProvedWithUserProofRule) > 0 then - SPARK_IO.Put_String (ReportFile, "(", 0); -- 1 char - EStrings.Put_String (File => ReportFile, - E_Str => PercentWithUserRuleStr); -- 5 char - SPARK_IO.Put_String (ReportFile, ")", 0); -- 1 char - else - SPARK_IO.Put_String (ReportFile, " ", 0); -- 1+5+1 = 7 char - end if; - - SPARK_IO.Put_String (ReportFile, " ", 0); - EStrings.Put_String (File => ReportFile, - E_Str => PercentProvedByCheckerStr); - SPARK_IO.Put_String (ReportFile, " ", 0); - EStrings.Put_String (File => ReportFile, - E_Str => PercentProvedByReviewStr); - SPARK_IO.Put_String (ReportFile, " ", 0); - EStrings.Put_String (File => ReportFile, - E_Str => PercentProvedFalseStr); - SPARK_IO.Put_String (ReportFile, " ", 0); - EStrings.Put_String (File => ReportFile, - E_Str => PercentUndischargedStr); - - -- Only suppress the 'look out' tag if everything has been proved, and - -- there are no false VCs. - if not ((EStrings.Eq1_String (E_Str => PercentUndischargedStr, - Str => " 0%") and then - EStrings.Eq1_String (E_Str => PercentProvedFalseStr, - Str => " 0%"))) then - SPARK_IO.Put_String (ReportFile, " <<<", 0); - end if; - SPARK_IO.New_Line (ReportFile, 1); - end if; - - --# assert True; - - -- Only report errors if there are some. - if TheTotals.Subprograms_Where_VC_Analysis_Abandoned > 0 then - SPARK_IO.Put_String - (ReportFile, "!!! ERRORS IN SIV FILES !!!", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.Subprograms_Where_VC_Analysis_Abandoned, 8, 10); - SPARK_IO.New_Line (ReportFile, 1); - end if; - - if TheTotals.Subprograms_Where_DPC_Analysis_Abandoned > 0 then - SPARK_IO.Put_String - (ReportFile, "!!! ERRORS IN DPC FILES !!!", 0); - SPARK_IO.Put_Integer - (ReportFile, TheTotals.Subprograms_Where_DPC_Analysis_Abandoned, 8, 10); - SPARK_IO.New_Line (ReportFile, 1); - end if; - - --# assert True; - - --# accept F, 33, TempStatus, "TempStatus not used here" & - --# F, 33, TempStoreBool, "TempStoreBool not used here"; - end Output; - - - procedure XMLOutput (ReportFile : in SPARK_IO.File_Type) - --# global in TheTotals; - --# in out SPARK_IO.File_Sys; - --# in out XMLSummary.State; - --# derives SPARK_IO.File_Sys from *, - --# ReportFile, - --# TheTotals, - --# XMLSummary.State & - --# XMLSummary.State from *, - --# TheTotals; - is - PercentUndischargedStr : EStrings.T; - PercentProvedByExaminerStr : EStrings.T; - PercentProvedByCheckerStr : EStrings.T; - PercentProvedByReviewStr : EStrings.T; - PercentSimplifiedStr : EStrings.T; - PercentWithUserRuleStr : EStrings.T; - PercentProvedFalseStr : EStrings.T; - begin - - -- Check the totals are balanced. - if not TotalsAreBalanced then - FatalError (FatalErrors.SubprogramTotalsInconsistent); - end if; - - XMLSummary.StartSummary (ReportFile); - - XMLSummary.StartSubprogramSummary (TheTotals.SubprogramsWithVCs, - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITExaminer, - TheTotals.SubprogramsProvedByExaminer, - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITSimplifier, - TheTotals.SubprogramsProvedBySimplifier, - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITChecker, - TheTotals.SubprogramsProvedByChecker, - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITReview, - TheTotals.SubprogramsProvedByReview, - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITFalse, - TheTotals.SubprogramsWithALOFalseVC, - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITUndischarged, - TheTotals.SubprogramsWithALOUndischargedVC, - ReportFile); - - XMLSummary.EndSubprogramSummary (ReportFile); - - --# assert True; - - -- In XML always report number of errors, even if they are zero. - -- (It seems better for parsing not to hide XML entries.) - -- This is deliberately not nested inside the subprograms tag above, as - -- this is implicitly describing only well-formed subprograms. - XMLSummary.StartSubprogramsInErrorSummary (TheTotals.Subprograms_Where_VC_Analysis_Abandoned, - ReportFile); - ---- Nothing inside this tag just now. - XMLSummary.EndSubprogramsInErrorSummary (ReportFile); - - --# assert True; - - XMLSummary.StartVCSummary (ReportFile); - - XMLSummary.StartSummarySection (XMLSummary.SSAssert_Post, - TheTotals.VCsTotal (VCDetails.Assert_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITExaminer, - TheTotals.VCsProvedByExaminer (VCDetails.Assert_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITSimplifier, - TheTotals.VCsProvedBySimplifier (VCDetails.Assert_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITChecker, - TheTotals.VCsProvedByChecker (VCDetails.Assert_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITReview, - TheTotals.VCsProvedByReview (VCDetails.Assert_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITFalse, - TheTotals.VCsProvedFalse (VCDetails.Assert_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITUndischarged, - TheTotals.VCsUndischarged (VCDetails.Assert_Point), - ReportFile); - - XMLSummary.EndSummarySection (ReportFile); - - --# assert True; - - XMLSummary.StartSummarySection (XMLSummary.SSPrecondition, - TheTotals.VCsTotal (VCDetails.Precondition_Check_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITExaminer, - TheTotals.VCsProvedByExaminer (VCDetails.Precondition_Check_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITSimplifier, - TheTotals.VCsProvedBySimplifier (VCDetails.Precondition_Check_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITChecker, - TheTotals.VCsProvedByChecker (VCDetails.Precondition_Check_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITReview, - TheTotals.VCsProvedByReview (VCDetails.Precondition_Check_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITFalse, - TheTotals.VCsProvedFalse (VCDetails.Precondition_Check_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITUndischarged, - TheTotals.VCsUndischarged (VCDetails.Precondition_Check_Point), - ReportFile); - - XMLSummary.EndSummarySection (ReportFile); - - --# assert True; - - XMLSummary.StartSummarySection (XMLSummary.SSCheck, - TheTotals.VCsTotal (VCDetails.Check_Statement_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITExaminer, - TheTotals.VCsProvedByExaminer (VCDetails.Check_Statement_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITSimplifier, - TheTotals.VCsProvedBySimplifier (VCDetails.Check_Statement_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITChecker, - TheTotals.VCsProvedByChecker (VCDetails.Check_Statement_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITReview, - TheTotals.VCsProvedByReview (VCDetails.Check_Statement_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITFalse, - TheTotals.VCsProvedFalse (VCDetails.Check_Statement_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITUndischarged, - TheTotals.VCsUndischarged (VCDetails.Check_Statement_Point), - ReportFile); - - XMLSummary.EndSummarySection (ReportFile); - - --# assert True; - - XMLSummary.StartSummarySection (XMLSummary.SSRuntime, - TheTotals.VCsTotal (VCDetails.Runtime_Check_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITExaminer, - TheTotals.VCsProvedByExaminer (VCDetails.Runtime_Check_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITSimplifier, - TheTotals.VCsProvedBySimplifier (VCDetails.Runtime_Check_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITChecker, - TheTotals.VCsProvedByChecker (VCDetails.Runtime_Check_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITReview, - TheTotals.VCsProvedByReview (VCDetails.Runtime_Check_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITFalse, - TheTotals.VCsProvedFalse (VCDetails.Runtime_Check_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITUndischarged, - TheTotals.VCsUndischarged (VCDetails.Runtime_Check_Point), - ReportFile); - - XMLSummary.EndSummarySection (ReportFile); - - --# assert True; - - - XMLSummary.StartSummarySection (XMLSummary.SSRefinement, - TheTotals.VCsTotal (VCDetails.Refinement_VC_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITExaminer, - TheTotals.VCsProvedByExaminer (VCDetails.Refinement_VC_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITSimplifier, - TheTotals.VCsProvedBySimplifier (VCDetails.Refinement_VC_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITChecker, - TheTotals.VCsProvedByChecker (VCDetails.Refinement_VC_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITReview, - TheTotals.VCsProvedByReview (VCDetails.Refinement_VC_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITFalse, - TheTotals.VCsProvedFalse (VCDetails.Refinement_VC_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITUndischarged, - TheTotals.VCsUndischarged (VCDetails.Refinement_VC_Point), - ReportFile); - - XMLSummary.EndSummarySection (ReportFile); - - - --# assert True; - - XMLSummary.StartSummarySection (XMLSummary.SSInheritance, - TheTotals.VCsTotal (VCDetails.Inheritance_VC_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITExaminer, - TheTotals.VCsProvedByExaminer (VCDetails.Inheritance_VC_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITSimplifier, - TheTotals.VCsProvedBySimplifier (VCDetails.Inheritance_VC_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITChecker, - TheTotals.VCsProvedByChecker (VCDetails.Inheritance_VC_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITReview, - TheTotals.VCsProvedByReview (VCDetails.Inheritance_VC_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITFalse, - TheTotals.VCsProvedFalse (VCDetails.Inheritance_VC_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITUndischarged, - TheTotals.VCsUndischarged (VCDetails.Inheritance_VC_Point), - ReportFile); - - XMLSummary.EndSummarySection (ReportFile); - - - --# assert True; - - XMLSummary.StartSummarySection (XMLSummary.SSUndetermined, - TheTotals.VCsTotal (VCDetails.Undetermined_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITExaminer, - TheTotals.VCsProvedByExaminer (VCDetails.Undetermined_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITSimplifier, - TheTotals.VCsProvedBySimplifier (VCDetails.Undetermined_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITChecker, - TheTotals.VCsProvedByChecker (VCDetails.Undetermined_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITReview, - TheTotals.VCsProvedByReview (VCDetails.Undetermined_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITFalse, - TheTotals.VCsProvedFalse (VCDetails.Undetermined_Point), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITUndischarged, - TheTotals.VCsUndischarged (VCDetails.Undetermined_Point), - ReportFile); - - XMLSummary.EndSummarySection (ReportFile); - - - --# assert True; - - XMLSummary.StartSummarySection (XMLSummary.SSTotals, - Sum (TheTotals.VCsTotal), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITExaminer, - Sum (TheTotals.VCsProvedByExaminer), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITSimplifier, - Sum (TheTotals.VCsProvedBySimplifier), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITChecker, - Sum (TheTotals.VCsProvedByChecker), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITReview, - Sum (TheTotals.VCsProvedByReview), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITFalse, - Sum (TheTotals.VCsProvedFalse), - ReportFile); - - XMLSummary.SummaryItemInt (XMLSummary.ITUndischarged, - Sum (TheTotals.VCsUndischarged), - ReportFile); - - XMLSummary.EndSummarySection (ReportFile); - - --# assert True; - - if Sum (TheTotals.VCsTotal) /= 0 then - - CalcuatePercentages (TheTotals, - PercentUndischargedStr, - PercentProvedByExaminerStr, - PercentProvedByCheckerStr, - PercentProvedByReviewStr, - PercentSimplifiedStr, - PercentWithUserRuleStr, - PercentProvedFalseStr); - - XMLSummary.StartSummarySection (XMLSummary.SSPercentages, - Sum (TheTotals.VCsTotal), - ReportFile); - - XMLSummary.SummaryItemStr (XMLSummary.ITExaminer, - EStrings.Trim (PercentProvedByExaminerStr), - ReportFile); - - XMLSummary.SummaryItemStr (XMLSummary.ITSimplifier, - EStrings.Trim (PercentSimplifiedStr), - ReportFile); - - XMLSummary.SummaryItemStr (XMLSummary.ITSimplifierUserRule, - EStrings.Trim (PercentWithUserRuleStr), - ReportFile); - - XMLSummary.SummaryItemStr (XMLSummary.ITChecker, - EStrings.Trim (PercentProvedByCheckerStr), - ReportFile); - - XMLSummary.SummaryItemStr (XMLSummary.ITReview, - EStrings.Trim (PercentProvedByReviewStr), - ReportFile); - - XMLSummary.SummaryItemStr (XMLSummary.ITFalse, - EStrings.Trim (PercentProvedFalseStr), - ReportFile); - - XMLSummary.SummaryItemStr (XMLSummary.ITUndischarged, - EStrings.Trim (PercentUndischargedStr), - ReportFile); - - XMLSummary.EndSummarySection (ReportFile); - - end if; - - XMLSummary.EndVCSummary (ReportFile); - - XMLSummary.EndSummary (ReportFile); - - end XMLOutput; - -begin - TheTotals := TotalType'(SubprogramsWithVCs => 0, - SubprogramsWhereMissingSLGFile => 0, - Subprograms_Where_VC_Analysis_Abandoned => 0, - Subprograms_Where_DPC_Analysis_Abandoned => 0, - SubprogramsWithALOUndischargedVC => 0, - SubprogramsWithALOExaminerVC => 0, - SubprogramsWithALOSimplifierVC => 0, - SubprogramsWithALOContradictionVC => 0, - SubprogramsWithALOUserRuleVC => 0, - SubprogramsWithALOCheckerVC => 0, - SubprogramsWithALOReviewVC => 0, - SubprogramsWithALOFalseVC => 0, - SubprogramsProvedByExaminer => 0, - SubprogramsProvedBySimplifier => 0, - SubprogramsProvedByChecker => 0, - SubprogramsProvedWithUserProofRule => 0, - SubprogramsProvedByReview => 0, - VCsTotal => NullVCCounter, - VCsProvedByExaminer => NullVCCounter, - VCsProvedBySimplifier => NullVCCounter, - VCsProvedByChecker => NullVCCounter, - VCsProvedWithUserProofRule => NullVCCounter, - VCsProvedByReview => NullVCCounter, - VCsProvedFalse => NullVCCounter, - VCsUndischarged => NullVCCounter, - Subprograms_With_DPCs => 0, - Subprograms_With_Dead_Paths => 0, - Number_Of_Dead_Paths => 0); -end Total; +-- $Id: total.adb 16001 2010-02-09 09:18:07Z dean kuo $ +-------------------------------------------------------------------------------- +-- (C) Altran Praxis Limited +-------------------------------------------------------------------------------- +-- +-- The SPARK toolset is free software; you can redistribute it and/or modify it +-- under terms of the GNU General Public License as published by the Free +-- Software Foundation; either version 3, or (at your option) any later +-- version. The SPARK toolset is distributed in the hope that it will be +-- useful, but WITHOUT ANY WARRANTY; without even the implied warranty of +-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General +-- Public License for more details. You should have received a copy of the GNU +-- General Public License distributed with the SPARK toolset; see file +-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of +-- the license. +-- +--============================================================================== + + +-------------------------------------------------------------------------------- +--Synopsis: -- +-- -- +--Package providing data structure to store running totals, and a procedure -- +--to print them. -- +-- -- +-------------------------------------------------------------------------------- +with Banner, + CommandLine, + ELStrings, + EStrings, + FatalErrors, + Heap, + VCHeap, + VCDetails, + XMLSummary; + +use type VCDetails.VC_State_T; +use type VCDetails.DPC_State_T; + +use type EStrings.T; + +package body Total +--# own State is TheTotals; +is + + type VCCounter is array (VCDetails.TerminalPointType) of Natural; + + NullVCCounter : constant VCCounter := + VCCounter'(others => 0); + + -- if adding more entries to this type, you must alter the procedure + -- Output below to display the results, and add code in the appropriate + -- analysis routines to increment the counter(s). You must also alter + -- the aggregate in Initialize below to initialize the new counter + type TotalType is record + + -- Subprograms without errors (all subprograms have vcs). + SubprogramsWithVCs : Natural; + + -- Subprograms with errors. + SubprogramsWhereMissingSLGFile : Natural; + Subprograms_Where_VC_Analysis_Abandoned : Natural; + Subprograms_Where_DPC_Analysis_Abandoned : Natural; + + -- A subprogram with At Least One (ALO) Undischarged VC. + SubprogramsWithALOUndischargedVC : Natural; + + -- The following fields record the number of subprograms, + -- which are not necessarily fully proved, but have at least + -- one VC proved by each of the following strategies: + + -- A subprogram with At Least One (ALO) VC proved by + -- the Examiner. + SubprogramsWithALOExaminerVC : Natural; + + -- A subprogram with At Least One (ALO) VC proved by the + -- simplifier without a user defined rule. + SubprogramsWithALOSimplifierVC : Natural; + + -- A subprogram with At Least One (ALO) VC proved using + -- a using proof by contradiction. + SubprogramsWithALOContradictionVC : Natural; + + -- A subprogram with At Least One (ALO) VC proved using + -- a user defined rule. + SubprogramsWithALOUserRuleVC : Natural; + + -- A subprogram with At Least One (ALO) VC proved using + -- the Checker. + SubprogramsWithALOCheckerVC : Natural; + + -- A subprogram with At Least One (ALO) VC discharged by review + SubprogramsWithALOReviewVC : Natural; + + -- A subprogram with At Least One (ALO) false VC. + SubprogramsWithALOFalseVC : Natural; + + -- The following fields represent the use of a hierachy of + -- proof strategies: + -- Examiner -> Simplifier -> User Rules -> Checker -> Review + -- When a subprogram is proved, the strategy latest in the hierarchy + -- is considered to have been used to complete the proof, even + -- if earlier strategies have also been applied. + -- The hierachy gives a measure of the extent of the strategies + -- required in proving a subprogram. + -- The definitions of the hierarchical strategies is given below: + -- A subprogram proof is completed by the examiner if: + -- o at LEAST one VC was proved by the examiner and + -- o ZERO VCs were proved by the simplifier, + -- checker, review file or left Undischarged and + -- o the subprogram has no false VCs. + SubprogramsProvedByExaminer : Natural; + + -- A subprogram proof is completed by the simplifier if: + -- o at LEAST one VC was proved by the simplifier and + -- o ZERO VCs were proved by the checker, review file + -- or left Undischarged and + -- o the subprogram has no false VCs. + SubprogramsProvedBySimplifier : Natural; + + -- A subprogram proof is completed by a user defined proof rule if: + -- o at least one VC was proved by the simplifier and + -- o at least one user defined rule has been used in the proof of a VC and + -- o ZERO VCs were proved by the checker, review file + -- or left Undischarged and + -- o the subprogram has no false VCs. + SubprogramsProvedWithUserProofRule : Natural; + + -- A subprogram proof is completed by the checker if: + -- o at LEAST one VC was proved by the checker and + -- o ZERO VCs were proved by the review file or + -- left Undischarged and + -- o the subprogram has no false VCs. + SubprogramsProvedByChecker : Natural; + + -- A subprogram proof is completed by review if: + -- o at LEAST one VC was proved in the review file and + -- o ZERO VCs were left Undischarged and + -- o the subprogram has no false VCs. + SubprogramsProvedByReview : Natural; + + -- The following fields record the number of VCs proved by + -- each strategy grouped by the sort of origin (the terminal point) + -- of the VC. + VCsTotal : VCCounter; + VCsProvedByExaminer : VCCounter; + VCsProvedBySimplifier : VCCounter; + VCsProvedByChecker : VCCounter; + VCsProvedWithUserProofRule : VCCounter; + VCsProvedByReview : VCCounter; + VCsProvedFalse : VCCounter; + VCsUndischarged : VCCounter; + + -- Record number of subprograms with DPCs + Subprograms_With_DPCs : Natural; + + -- The following fields record the number of dead paths ZombieScope + -- has found. + Number_Of_Dead_Paths : Natural; + Subprograms_With_Dead_Paths : Natural; + end record; + + TheTotals : TotalType; + + function Sum (T : in VCCounter) return Natural + is + Result : Natural := 0; + begin + for I in VCDetails.TerminalPointType loop + Result := Result + T (I); + end loop; + return Result; + end Sum; + + -- The calculation of percentages is factored out, to keep the + -- standard and XML summary output consistent. + procedure CalcuatePercentages (TheTotals : in TotalType; + PercentUndischargedStr : out EStrings.T; + PercentProvedByExaminerStr : out EStrings.T; + PercentProvedByCheckerStr : out EStrings.T; + PercentProvedByReviewStr : out EStrings.T; + PercentSimplifiedStr : out EStrings.T; + PercentWithUserRuleStr : out EStrings.T; + PercentProvedFalseStr : out EStrings.T) + --#derives PercentUndischargedStr, + --# PercentProvedByExaminerStr, + --# PercentProvedByCheckerStr, + --# PercentProvedByReviewStr, + --# PercentSimplifiedStr, + --# PercentWithUserRuleStr, + --# PercentProvedFalseStr from TheTotals; + is + subtype Percentage is Natural range 0 .. 100; + + VCsTotal : Natural; + + PercentUndischarged : Percentage; + PercentUndischargedC : Character; + PercentProvedByExaminer : Percentage; + PercentProvedByExaminerC : Character; + PercentProvedByChecker : Percentage; + PercentProvedByCheckerC : Character; + PercentProvedByReview : Percentage; + PercentProvedByReviewC : Character; + PercentSimplified : Percentage; + PercentSimplifiedC : Character; + PercentWithUserRule : Percentage; + PercentWithUserRuleC : Character; + PercentProvedFalse : Percentage; + PercentProvedFalseC : Character; + + procedure TotalAndValueToPercentage (OverallTotal : in Natural; + Value : in Natural; + Percent : out Percentage; + PercentC : out Character) + --# derives Percent, PercentC from OverallTotal, Value; + --# pre (OverallTotal/=0); + is + PercisePercentValue : Float; + RoundedPercentValue : Percentage; + begin + PercisePercentValue := (Float (Value) * 100.0) / Float (OverallTotal); + RoundedPercentValue := Percentage (PercisePercentValue); + + case RoundedPercentValue is + + -- If the rounded percentage value is zero, but the actual + -- value is non-zero, then the rounded value is forced to be 1. + -- This behaviour ensures that a zero percentage really means + -- zero. + when 0 => + if (Value /= 0) then + Percent := 1; + + -- If the actual percent is less than 0.5 then this is + -- indicated with an appropriate leading character. + if (PercisePercentValue < 0.5) then + PercentC := '<'; + else + PercentC := ' '; + end if; + else + Percent := 0; + PercentC := ' '; + end if; + + -- If the rounded percentage value is 100, but the actual value + -- is not equal to the total, then the rounded value is forced + -- to be 99. This behaviour ensures that a hundred percent + -- really means all. + when 100 => + if (Value /= OverallTotal) then + Percent := 99; + + -- If the actual percent is greater than 99.5 then this is + -- indicated with an appropriate leading character. + if (PercisePercentValue > 99.5) then + PercentC := '>'; + else + PercentC := ' '; + end if; + else + Percent := 100; + PercentC := ' '; + end if; + + -- In all other cases, accept the rounding approximation. + when 1 .. 99 => + Percent := RoundedPercentValue; + PercentC := ' '; + end case; + end TotalAndValueToPercentage; + + procedure GeneratePercentString (Percent : in Percentage; + PercentC : in Character; + PercentStr : out EStrings.T) + --# derives PercentStr from Percent, PercentC; + is + subtype StringLength is Integer range 1 .. 10; + subtype TempString is String (StringLength); + PercentPart : TempString; + DummySuccess : Boolean; + begin + --Initialise to empty string. + PercentStr := EStrings.Empty_String; + + --# accept F, 10, DummySuccess, "Error status ignored as number always fits."; + --# accept F, 33, DummySuccess, "Error status ignored as number always fits."; + + --For alingment: if percent is one digit, add two spaces. + -- : if percent is two digits, add one spaces. + case Percent is + when 0 .. 9 => + EStrings.Append_String (E_Str => PercentStr, + Str => " "); + when 10 .. 99 => + EStrings.Append_String (E_Str => PercentStr, + Str => " "); + when 100 => + null; + end case; + + --Append the: '>','<',' ' prefix. (max length "X": 1) + EStrings.Append_Char (E_Str => PercentStr, + Ch => PercentC, + Success => DummySuccess); + + --Append the: percent number. (max length "XYYY": 4) + SPARK_IO.Put_Int_To_String (PercentPart, Percent, 1, 10); + EStrings.Append_Examiner_String + (E_Str1 => PercentStr, + E_Str2 => EStrings.Trim + (EStrings.Copy_String (Str => PercentPart))); + + --Append the: symbol '%'. (max length "XYYY%": 5) + EStrings.Append_Char (E_Str => PercentStr, + Ch => '%', + Success => DummySuccess); + + end GeneratePercentString; + + begin + + VCsTotal := Sum (TheTotals.VCsTotal); + + TotalAndValueToPercentage (VCsTotal, + Sum (TheTotals.VCsUndischarged), + PercentUndischarged, + PercentUndischargedC); + GeneratePercentString (PercentUndischarged, + PercentUndischargedC, + PercentUndischargedStr); + + TotalAndValueToPercentage (VCsTotal, + Sum (TheTotals.VCsProvedByExaminer), + PercentProvedByExaminer, + PercentProvedByExaminerC); + GeneratePercentString (PercentProvedByExaminer, + PercentProvedByExaminerC, + PercentProvedByExaminerStr); + + TotalAndValueToPercentage (VCsTotal, + Sum (TheTotals.VCsProvedByChecker), + PercentProvedByChecker, + PercentProvedByCheckerC); + GeneratePercentString (PercentProvedByChecker, + PercentProvedByCheckerC, + PercentProvedByCheckerStr); + + TotalAndValueToPercentage (VCsTotal, + Sum (TheTotals.VCsProvedByReview), + PercentProvedByReview, + PercentProvedByReviewC); + GeneratePercentString (PercentProvedByReview, + PercentProvedByReviewC, + PercentProvedByReviewStr); + + TotalAndValueToPercentage (VCsTotal, + Sum (TheTotals.VCsProvedBySimplifier), + PercentSimplified, + PercentSimplifiedC); + GeneratePercentString (PercentSimplified, + PercentSimplifiedC, + PercentSimplifiedStr); + + TotalAndValueToPercentage (VCsTotal, + Sum (TheTotals.VCsProvedWithUserProofRule), + PercentWithUserRule, + PercentWithUserRuleC); + GeneratePercentString (PercentWithUserRule, + PercentWithUserRuleC, + PercentWithUserRuleStr); + + TotalAndValueToPercentage (VCsTotal, + Sum (TheTotals.VCsProvedFalse), + PercentProvedFalse, + PercentProvedFalseC); + GeneratePercentString (PercentProvedFalse, + PercentProvedFalseC, + PercentProvedFalseStr); + end CalcuatePercentages; + + -- Never returns from this subprogram. + -- Null dependency relation used to avoid propagation + -- of FatalErrors.State impacting existing clients of Total. + -- FatalErrors.State is of little interest in this context. + procedure FatalError (Error : in FatalErrors.ErrorType) + --# derives null from Error; + is + --# hide FatalError; + begin + FatalErrors.Process (Error, ELStrings.Empty_String); + end FatalError; + + function TotalsAreBalanced return Boolean + --# global in TheTotals; + is + TotalSubprogramsProved : Natural; + TotalSubprogramsAtLeastOneFalseVC : Natural; + TotalSubprogramsNoFalseAtLeastOneUndischarged : Natural; + TotalSubprograms : Natural; + begin + -- Total all of the subprogram that have been fully proved. + TotalSubprogramsProved := ((((TheTotals.SubprogramsProvedByExaminer + + TheTotals.SubprogramsProvedBySimplifier) + + TheTotals.SubprogramsProvedWithUserProofRule) + + TheTotals.SubprogramsProvedByChecker) + + TheTotals.SubprogramsProvedByReview); + + -- Total all of the subprogram that have at least one false vc. + TotalSubprogramsAtLeastOneFalseVC := TheTotals.SubprogramsWithALOFalseVC; + + -- Total all of the subprogram that have no false vcs, and at least one + -- undischarged vc. + TotalSubprogramsNoFalseAtLeastOneUndischarged := TheTotals.SubprogramsWithALOUndischargedVC; + + -- Total all of the subprograms. + TotalSubprograms := ((TotalSubprogramsProved + + TotalSubprogramsAtLeastOneFalseVC) + + TotalSubprogramsNoFalseAtLeastOneUndischarged); + + -- Return true if the total matches the recorded total number of Subprograms + -- with VCs and false otherwise. + return (TotalSubprograms = TheTotals.SubprogramsWithVCs); + end TotalsAreBalanced; + + procedure UpdateTotals (VCG : in Boolean; DPC : in Boolean) + --# global in VCHeap.State; + --# in out TheTotals; + --# derives TheTotals from *, + --# VCG, + --# DPC, + --# VCHeap.State; + is + SubProgramIsUndischarged : Boolean; + SubProgramHasVCProvedByExaminer : Boolean; + SubProgramHasVCProvedBySimplifier : Boolean; + SubProgramHasVCProvedByContradiction : Boolean; + SubProgramHasVCProvedWithUserProofRule : Boolean; + SubProgramHasVCProvedByChecker : Boolean; + SubProgramHasVCProvedByReview : Boolean; + SubProgramHasVCProvedFalse : Boolean; + Subprogram_Contains_Dead_Paths : Boolean; + MoreVCs : Boolean; + + HeapIndex : Heap.Atom; + NextIndex : Heap.Atom; + + UnusedVCName : EStrings.T; + UnusedPathStart : EStrings.T; + UnusedPathEnd : EStrings.T; + EndType : VCDetails.TerminalPointType; + + VC_State : VCDetails.VC_State_T; + DPC_State : VCDetails.DPC_State_T; + + begin + + --Always count missing SLG files. + if VCHeap.ErrorRaised (VCDetails.MissingSLGFile) then + TheTotals.SubprogramsWhereMissingSLGFile := TheTotals.SubprogramsWhereMissingSLGFile + 1; + end if; + + --Only perform detailed analysis of subprogram if it did not have an + --associated corrupt file. + if VCHeap.ErrorRaised (VCDetails.Corrupt_VC_File) then + TheTotals.Subprograms_Where_VC_Analysis_Abandoned := + TheTotals.Subprograms_Where_VC_Analysis_Abandoned + 1; + end if; + + if VCHeap.ErrorRaised (VCDetails.Corrupt_DPC_File) then + TheTotals.Subprograms_Where_DPC_Analysis_Abandoned := + TheTotals.Subprograms_Where_DPC_Analysis_Abandoned + 1; + end if; + + MoreVCs := True; + HeapIndex := VCHeap.FirstEntry; + + SubProgramIsUndischarged := False; + SubProgramHasVCProvedByExaminer := False; + SubProgramHasVCProvedBySimplifier := False; + SubProgramHasVCProvedByContradiction := False; + SubProgramHasVCProvedByChecker := False; + SubProgramHasVCProvedWithUserProofRule := False; + SubProgramHasVCProvedByReview := False; + SubProgramHasVCProvedFalse := False; + Subprogram_Contains_Dead_Paths := False; + + if VCG and (not VCHeap.ErrorRaised (VCDetails.Corrupt_VC_File)) then + TheTotals.SubprogramsWithVCs := TheTotals.SubprogramsWithVCs + 1; + end if; + + if DPC and (not VCHeap.ErrorRaised (VCDetails.Corrupt_DPC_File)) then + TheTotals.Subprograms_With_DPCs := TheTotals.Subprograms_With_DPCs + 1; + end if; + + while MoreVCs and not Heap.IsNullPointer (HeapIndex) loop + + -- Get the details for the next VC. + --# accept F, 10, UnusedPathEnd, "UnusedPathEnd unused here" & + --# F, 10, UnusedPathStart, "UnusedPathStart unused here" & + --# F, 10, UnusedVCName, "UnusedPVCName unused here" ; + VCHeap.Details (ListIndex => HeapIndex, + VCName => UnusedVCName, + PathStart => UnusedPathStart, + PathEnd => UnusedPathEnd, + EndType => EndType, + VC_State => VC_State, + DPC_State => DPC_State); + + --# end accept; + + --# accept F, 41, "Expression is stable"; + if VCG and (not VCHeap.ErrorRaised (VCDetails.Corrupt_VC_File)) then + --# end accept; + TheTotals.VCsTotal (EndType) := TheTotals.VCsTotal (EndType) + 1; + + case VC_State is + when VCDetails.VC_False => + TheTotals.VCsProvedFalse (EndType) := + TheTotals.VCsProvedFalse (EndType) + 1; + SubProgramHasVCProvedFalse := True; + SubProgramIsUndischarged := True; + when VCDetails.VC_Proved_By_Examiner => + SubProgramHasVCProvedByExaminer := True; + TheTotals.VCsProvedByExaminer (EndType) := + TheTotals.VCsProvedByExaminer (EndType) + 1; + when VCDetails.VC_Proved_By_Inference => + SubProgramHasVCProvedBySimplifier := True; + TheTotals.VCsProvedBySimplifier (EndType) := + TheTotals.VCsProvedBySimplifier (EndType) + 1; + when VCDetails.VC_Proved_By_Contradiction => + SubProgramHasVCProvedByContradiction := True; + SubProgramHasVCProvedBySimplifier := True; + TheTotals.VCsProvedBySimplifier (EndType) := + TheTotals.VCsProvedBySimplifier (EndType) + 1; + when VCDetails.VC_Proved_By_Checker => + SubProgramHasVCProvedByChecker := True; + + TheTotals.VCsProvedByChecker (EndType) := + TheTotals.VCsProvedByChecker (EndType) + 1; + when VCDetails.VC_Proved_By_Review => + SubProgramHasVCProvedByReview := True; + + TheTotals.VCsProvedByReview (EndType) := + TheTotals.VCsProvedByReview (EndType) + 1; + when VCDetails.VC_Proved_Using_User_Proof_Rules => + SubProgramHasVCProvedWithUserProofRule := True; + SubProgramHasVCProvedBySimplifier := True; + TheTotals.VCsProvedWithUserProofRule (EndType) := + TheTotals.VCsProvedWithUserProofRule (EndType) + 1; + TheTotals.VCsProvedBySimplifier (EndType) := + TheTotals.VCsProvedBySimplifier (EndType) + 1; + when VCDetails.VC_SIV_Not_Present | VCDetails.VC_Undischarged => + TheTotals.VCsUndischarged (EndType) := + TheTotals.VCsUndischarged (EndType) + 1; + SubProgramIsUndischarged := True; + when others => -- VC_Not_Present + -- No VC is present. + null; + end case; + end if; + + --# accept F, 41, "Expression is stable"; + if DPC and (not VCHeap.ErrorRaised (VCDetails.Corrupt_DPC_File)) then + --# end accept; + if DPC_State = VCDetails.DPC_Dead then + -- Update the total number of subprograms containing + -- dead paths. + if not Subprogram_Contains_Dead_Paths then + TheTotals.Subprograms_With_Dead_Paths := + TheTotals.Subprograms_With_Dead_Paths + 1; + end if; + Subprogram_Contains_Dead_Paths := True; + -- Update the total number of dead paths found. + TheTotals.Number_Of_Dead_Paths := + TheTotals.Number_Of_Dead_Paths + 1; + end if; + end if; + + VCHeap.Next (AfterThis => HeapIndex, + Success => MoreVCs, + NextOne => NextIndex); + + HeapIndex := NextIndex; + + end loop; + + --# assert True; + + -- Update the At Least One Counts + if SubProgramIsUndischarged then + if SubProgramHasVCProvedFalse then + TheTotals.SubprogramsWithALOFalseVC := + TheTotals.SubprogramsWithALOFalseVC + 1; + else + TheTotals.SubprogramsWithALOUndischargedVC := + TheTotals.SubprogramsWithALOUndischargedVC + 1; + end if; + end if; + + --# assert True; + + + if SubProgramHasVCProvedByExaminer then + TheTotals.SubprogramsWithALOExaminerVC := + TheTotals.SubprogramsWithALOExaminerVC + 1; + end if; + + --# assert True; + + if SubProgramHasVCProvedBySimplifier then + TheTotals.SubprogramsWithALOSimplifierVC := + TheTotals.SubprogramsWithALOSimplifierVC + 1; + end if; + + --# assert True; + + if SubProgramHasVCProvedByContradiction then + TheTotals.SubprogramsWithALOContradictionVC := + TheTotals.SubprogramsWithALOContradictionVC + 1; + end if; + + --# assert True; + + if SubProgramHasVCProvedWithUserProofRule then + TheTotals.SubprogramsWithALOUserRuleVC := + TheTotals.SubprogramsWithALOUserRuleVC + 1; + end if; + + --# assert True; + + if SubProgramHasVCProvedByChecker then + TheTotals.SubprogramsWithALOCheckerVC := + TheTotals.SubprogramsWithALOCheckerVC + 1; + end if; + + --# assert True; + + if SubProgramHasVCProvedByReview then + TheTotals.SubprogramsWithALOReviewVC := + TheTotals.SubprogramsWithALOReviewVC + 1; + end if; + + --# assert True; + + -- Update the proof strategy use hierarchy (See declaration of TotalType) + -- Examiner -> Simplifier -> User Rules -> Checker -> Review + if not SubProgramIsUndischarged then + if SubProgramHasVCProvedByReview then + TheTotals.SubprogramsProvedByReview := + TheTotals.SubprogramsProvedByReview + 1; + + elsif SubProgramHasVCProvedByChecker then + TheTotals.SubprogramsProvedByChecker := + TheTotals.SubprogramsProvedByChecker + 1; + + elsif SubProgramHasVCProvedWithUserProofRule then + TheTotals.SubprogramsProvedWithUserProofRule := + TheTotals.SubprogramsProvedWithUserProofRule + 1; + + elsif SubProgramHasVCProvedBySimplifier then + TheTotals.SubprogramsProvedBySimplifier := + TheTotals.SubprogramsProvedBySimplifier + 1; + + elsif SubProgramHasVCProvedByExaminer then + TheTotals.SubprogramsProvedByExaminer := + TheTotals.SubprogramsProvedByExaminer + 1; + end if; + end if; + + --# assert True; + + --# accept F, 33, UnusedPathEnd, "UnusedPathEnd unused here" & + --# F, 33, UnusedPathStart, "UnusedPathStart unused here" & + --# F, 33, UnusedVCName, "UnusedPVCName unused here"; + end UpdateTotals; + + procedure RulesUsedForFile (ReportFile : in SPARK_IO.File_Type; + RuleFileName : in EStrings.T; + RulesFile : in out SPARK_IO.File_Type) + --# global in out SPARK_IO.File_Sys; + --# derives RulesFile from * & + --# SPARK_IO.File_Sys from *, + --# ReportFile, + --# RuleFileName, + --# RulesFile; + is separate; + + procedure Output (ReportFile : in SPARK_IO.File_Type; + TempFile : in out SPARK_IO.File_Type; + TempFalseFile : in out SPARK_IO.File_Type; + TempContraFile : in out SPARK_IO.File_Type; + TempUserFile : in out SPARK_IO.File_Type; + TempRluErrorFile : in out SPARK_IO.File_Type; + TempRluUsedFile : in out SPARK_IO.File_Type; + TempRulesUsedFile : in out SPARK_IO.File_Type; + TempPRVerrFile : in out SPARK_IO.File_Type; + TempWarnErrorFile : in out SPARK_IO.File_Type; + TempSDPErrorFile : in out SPARK_IO.File_Type; + TempDPCErrorFile : in out SPARK_IO.File_Type) + --# global in CommandLine.Data; + --# in TheTotals; + --# in out SPARK_IO.File_Sys; + --# derives SPARK_IO.File_Sys from *, + --# CommandLine.Data, + --# ReportFile, + --# TempContraFile, + --# TempDPCErrorFile, + --# TempFalseFile, + --# TempFile, + --# TempPRVerrFile, + --# TempRluErrorFile, + --# TempRluUsedFile, + --# TempRulesUsedFile, + --# TempSDPErrorFile, + --# TempUserFile, + --# TempWarnErrorFile, + --# TheTotals & + --# TempContraFile, + --# TempDPCErrorFile, + --# TempFalseFile, + --# TempFile, + --# TempPRVerrFile, + --# TempRluErrorFile, + --# TempRluUsedFile, + --# TempSDPErrorFile, + --# TempUserFile, + --# TempWarnErrorFile from * & + --# TempRulesUsedFile from *, + --# TempRluUsedFile; + is + PercentUndischargedStr : EStrings.T; + PercentProvedByExaminerStr : EStrings.T; + PercentProvedByCheckerStr : EStrings.T; + PercentProvedByReviewStr : EStrings.T; + PercentSimplifiedStr : EStrings.T; + PercentWithUserRuleStr : EStrings.T; + PercentProvedFalseStr : EStrings.T; + + TotalSubprogramsProved : Natural; + + TempStoreInt : Integer; + TempStoreString : EStrings.T; + TempStoreBool : Boolean; + TempStatus : SPARK_IO.File_Status; + + + begin + SPARK_IO.Put_Line (ReportFile, Banner.MajorSeparatorLine, 0); + SPARK_IO.Put_Line (ReportFile, "Summary:", 0); + SPARK_IO.New_Line (ReportFile, 1); + + --# accept F, 10, TempStatus, "TempStatus not used here" & + --# F, 10, TempStoreBool, "TempStoreBool not used here"; + + -- print out the names of files containing warnings or errors + SPARK_IO.Reset (TempWarnErrorFile, SPARK_IO.In_File, TempStatus); + if not SPARK_IO.End_Of_File (TempWarnErrorFile) then + SPARK_IO.Put_Line (ReportFile, "***WARNING: The following files, or their absence, raised warnings or errors:", 0); + SPARK_IO.New_Line (ReportFile, 1); + while not SPARK_IO.End_Of_File (TempWarnErrorFile) loop + SPARK_IO.Get_Integer (TempWarnErrorFile, TempStoreInt, 4, TempStoreBool); + SPARK_IO.Put_Integer (ReportFile, TempStoreInt, 4, 10); + SPARK_IO.Put_String (ReportFile, " ", 0); + EStrings.Get_Line (File => TempWarnErrorFile, + E_Str => TempStoreString); + EStrings.Put_String (File => ReportFile, + E_Str => TempStoreString); + SPARK_IO.New_Line (ReportFile, 1); + end loop; + SPARK_IO.New_Line (ReportFile, 1); + end if; + + --# assert True; + + -- print out the names of any user rule files containing syntax errors + SPARK_IO.Reset (TempRluErrorFile, SPARK_IO.In_File, TempStatus); + if not SPARK_IO.End_Of_File (TempRluErrorFile) then + SPARK_IO.Put_Line (ReportFile, "***WARNING: The following user defined rule files contain syntax errors:", 0); + SPARK_IO.New_Line (ReportFile, 1); + while not SPARK_IO.End_Of_File (TempRluErrorFile) loop + -- Note no number output here (not possible to know earlier) + EStrings.Get_Line (File => TempRluErrorFile, + E_Str => TempStoreString); + -- Switching back and forth between Append and Input modes + -- causes empty lines to be created + if EStrings.Get_Length (E_Str => TempStoreString) /= 0 then + SPARK_IO.Put_String (ReportFile, " ", 0); + EStrings.Put_String (File => ReportFile, + E_Str => TempStoreString); + SPARK_IO.New_Line (ReportFile, 1); + end if; + end loop; + SPARK_IO.New_Line (ReportFile, 1); + end if; + + --# assert True; + + -- print out any used user-defined rule files + SPARK_IO.Reset (TempRluUsedFile, SPARK_IO.In_File, TempStatus); + if not SPARK_IO.End_Of_File (TempRluUsedFile) then + SPARK_IO.Put_Line (ReportFile, "The following user-defined rule files have been used:", 0); + SPARK_IO.New_Line (ReportFile, 1); + while not SPARK_IO.End_Of_File (TempRluUsedFile) loop + -- Note no number output here (difficult to calculate earlier) + EStrings.Get_Line (File => TempRluUsedFile, + E_Str => TempStoreString); + -- Switching back and forth between Append and Input modes + -- causes empty lines to be created + if EStrings.Get_Length (E_Str => TempStoreString) /= 0 then + SPARK_IO.Put_String (ReportFile, " ", 0); + EStrings.Put_String (File => ReportFile, + E_Str => TempStoreString); + SPARK_IO.New_Line (ReportFile, 1); + RulesUsedForFile (ReportFile => ReportFile, + RuleFileName => TempStoreString, + RulesFile => TempRulesUsedFile); + end if; + end loop; + SPARK_IO.New_Line (ReportFile, 1); + end if; + + --# assert True; + + -- print out the file names and numbers of any false VC + SPARK_IO.Reset (TempFalseFile, SPARK_IO.In_File, TempStatus); + if not SPARK_IO.End_Of_File (TempFalseFile) then + SPARK_IO.Put_Line (ReportFile, "The following subprograms have VCs proved false:", 0); + SPARK_IO.New_Line (ReportFile, 1); + while not SPARK_IO.End_Of_File (TempFalseFile) loop + SPARK_IO.Get_Integer (TempFalseFile, TempStoreInt, 4, TempStoreBool); + SPARK_IO.Put_Integer (ReportFile, TempStoreInt, 4, 10); + SPARK_IO.Put_String (ReportFile, " ", 0); + EStrings.Get_Line (File => TempFalseFile, + E_Str => TempStoreString); + EStrings.Put_String (File => ReportFile, + E_Str => TempStoreString); + SPARK_IO.New_Line (ReportFile, 1); + end loop; + SPARK_IO.New_Line (ReportFile, 1); + end if; + + --# assert True; + + -- print out the file names and numbers of any undischarged VC (excluding those proved false) + SPARK_IO.Reset (TempFile, SPARK_IO.In_File, TempStatus); + if not SPARK_IO.End_Of_File (TempFile) then + SPARK_IO.Put_Line (ReportFile, "The following subprograms have undischarged VCs (excluding those proved false):", 0); + SPARK_IO.New_Line (ReportFile, 1); + while not SPARK_IO.End_Of_File (TempFile) loop + SPARK_IO.Get_Integer (TempFile, TempStoreInt, 4, TempStoreBool); + SPARK_IO.Put_Integer (ReportFile, TempStoreInt, 4, 10); + SPARK_IO.Put_String (ReportFile, " ", 0); + EStrings.Get_Line (File => TempFile, + E_Str => TempStoreString); + EStrings.Put_String (File => ReportFile, + E_Str => TempStoreString); + SPARK_IO.New_Line (ReportFile, 1); + end loop; + SPARK_IO.New_Line (ReportFile, 1); + end if; + + --# assert True; + + -- print out the file names and numbers of any VC proved by contradiction + SPARK_IO.Reset (TempContraFile, SPARK_IO.In_File, TempStatus); + if not SPARK_IO.End_Of_File (TempContraFile) then + SPARK_IO.Put_Line (ReportFile, "The following subprograms have VCs proved by contradiction:", 0); + SPARK_IO.New_Line (ReportFile, 1); + while not SPARK_IO.End_Of_File (TempContraFile) loop + SPARK_IO.Get_Integer (TempContraFile, TempStoreInt, 4, TempStoreBool); + SPARK_IO.Put_Integer (ReportFile, TempStoreInt, 4, 10); + SPARK_IO.Put_String (ReportFile, " ", 0); + EStrings.Get_Line (File => TempContraFile, + E_Str => TempStoreString); + EStrings.Put_String (File => ReportFile, + E_Str => TempStoreString); + SPARK_IO.New_Line (ReportFile, 1); + end loop; + SPARK_IO.New_Line (ReportFile, 1); + end if; + + --# assert True; + + -- print out the file names and numbers of any VC proved by a user-defined proof rule + SPARK_IO.Reset (TempUserFile, SPARK_IO.In_File, TempStatus); + if not SPARK_IO.End_Of_File (TempUserFile) then + SPARK_IO.Put_Line (ReportFile, "The following subprograms have VCs proved using a user-defined proof rule:", 0); + SPARK_IO.New_Line (ReportFile, 1); + while not SPARK_IO.End_Of_File (TempUserFile) loop + SPARK_IO.Get_Integer (TempUserFile, TempStoreInt, 4, TempStoreBool); + SPARK_IO.Put_Integer (ReportFile, TempStoreInt, 4, 10); + SPARK_IO.Put_String (ReportFile, " ", 0); + EStrings.Get_Line (File => TempUserFile, + E_Str => TempStoreString); + EStrings.Put_String (File => ReportFile, + E_Str => TempStoreString); + SPARK_IO.New_Line (ReportFile, 1); + end loop; + SPARK_IO.New_Line (ReportFile, 1); + end if; + + --# assert True; + + -- print out the file names and numbers of any files with review errors + SPARK_IO.Reset (TempPRVerrFile, SPARK_IO.In_File, TempStatus); + if not SPARK_IO.End_Of_File (TempPRVerrFile) then + SPARK_IO.Put_Line (ReportFile, "***WARNING: The PRV file(s) associated with the following subprograms may be out of date", 0); + SPARK_IO.Put_Line (ReportFile, "The following subprograms have review files containing VCs already proved elsewhere:", 0); + SPARK_IO.New_Line (ReportFile, 1); + while not SPARK_IO.End_Of_File (TempPRVerrFile) loop + SPARK_IO.Get_Integer (TempPRVerrFile, TempStoreInt, 4, TempStoreBool); + SPARK_IO.Put_Integer (ReportFile, TempStoreInt, 4, 10); + SPARK_IO.Put_String (ReportFile, " ", 0); + EStrings.Get_Line (File => TempPRVerrFile, + E_Str => TempStoreString); + EStrings.Put_String (File => ReportFile, + E_Str => TempStoreString); + SPARK_IO.New_Line (ReportFile, 1); + end loop; + SPARK_IO.New_Line (ReportFile, 1); + end if; + + -- print out the names of any missing SDP files + SPARK_IO.Reset (TempSDPErrorFile, SPARK_IO.In_File, TempStatus); + if not SPARK_IO.End_Of_File (TempSDPErrorFile) then + SPARK_IO.Put_Line (ReportFile, "***WARNING: The following DPC files have not been ZombieScoped:", 0); + SPARK_IO.New_Line (ReportFile, 1); + while not SPARK_IO.End_Of_File (TempSDPErrorFile) loop + EStrings.Get_Line (File => TempSDPErrorFile, + E_Str => TempStoreString); + -- Switching back and forth between Append and Input modes + -- causes empty lines to be created + if EStrings.Get_Length (E_Str => TempStoreString) /= 0 then + SPARK_IO.Put_String (ReportFile, " ", 0); + EStrings.Put_String (File => ReportFile, + E_Str => TempStoreString); + SPARK_IO.New_Line (ReportFile, 1); + end if; + end loop; + SPARK_IO.New_Line (ReportFile, 1); + end if; + + -- print out the names of any missing DPC files + SPARK_IO.Reset (TempDPCErrorFile, SPARK_IO.In_File, TempStatus); + if not SPARK_IO.End_Of_File (TempDPCErrorFile) then + SPARK_IO.Put_Line (ReportFile, "***WARNING: The following DPC files are missing:", 0); + SPARK_IO.New_Line (ReportFile, 1); + while not SPARK_IO.End_Of_File (TempDPCErrorFile) loop + EStrings.Get_Line (File => TempDPCErrorFile, + E_Str => TempStoreString); + -- Switching back and forth between Append and Input modes + -- causes empty lines to be created + if EStrings.Get_Length (E_Str => TempStoreString) /= 0 then + SPARK_IO.Put_String (ReportFile, " ", 0); + EStrings.Put_String (File => ReportFile, + E_Str => TempStoreString); + SPARK_IO.New_Line (ReportFile, 1); + end if; + end loop; + SPARK_IO.New_Line (ReportFile, 1); + end if; + --# end accept; + + --# assert True; + + -- Print a summary of the number of subprograms conatining at + -- least one instance of the following: + SPARK_IO.Put_Line + (ReportFile, + "Proof strategies used by subprograms", 0); + SPARK_IO.Put_Line + (ReportFile, + "-------------------------------------------------------------------------", 0); + SPARK_IO.Put_String + (ReportFile, + "Total subprograms with at least one VC proved by examiner: ", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.SubprogramsWithALOExaminerVC, 4, 10); + SPARK_IO.New_Line (ReportFile, 1); + + SPARK_IO.Put_String + (ReportFile, + "Total subprograms with at least one VC proved by simplifier: ", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.SubprogramsWithALOSimplifierVC, 4, 10); + SPARK_IO.New_Line (ReportFile, 1); + + SPARK_IO.Put_String + (ReportFile, + "Total subprograms with at least one VC proved by contradiction: ", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.SubprogramsWithALOContradictionVC, 4, 10); + SPARK_IO.New_Line (ReportFile, 1); + + SPARK_IO.Put_String + (ReportFile, + "Total subprograms with at least one VC proved with user proof rule: ", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.SubprogramsWithALOUserRuleVC, 4, 10); + SPARK_IO.New_Line (ReportFile, 1); + + SPARK_IO.Put_String + (ReportFile, + "Total subprograms with at least one VC proved using checker: ", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.SubprogramsWithALOCheckerVC, 4, 10); + SPARK_IO.New_Line (ReportFile, 1); + + SPARK_IO.Put_String + (ReportFile, + "Total subprograms with at least one VC discharged by review: ", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.SubprogramsWithALOReviewVC, 4, 10); + SPARK_IO.New_Line (ReportFile, 1); + + --# assert True; + + -- Print out hierarchy of proof strategy use (see declaration of TotalType) + -- Examiner -> Simplifier -> User Rules -> Checker -> Review + SPARK_IO.New_Line (ReportFile, 1); + SPARK_IO.Put_Line + (ReportFile, + "Maximum extent of strategies used for fully proved subprograms:", 0); + SPARK_IO.Put_Line + (ReportFile, + "-------------------------------------------------------------------------", 0); + SPARK_IO.Put_String + (ReportFile, + "Total subprograms with proof completed by examiner: ", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.SubprogramsProvedByExaminer, 4, 10); + SPARK_IO.New_Line (ReportFile, 1); + + SPARK_IO.Put_String + (ReportFile, + "Total subprograms with proof completed by simplifier: ", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.SubprogramsProvedBySimplifier, 4, 10); + SPARK_IO.New_Line (ReportFile, 1); + + SPARK_IO.Put_String + (ReportFile, + "Total subprograms with proof completed with user defined rules: ", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.SubprogramsProvedWithUserProofRule, 4, 10); + SPARK_IO.New_Line (ReportFile, 1); + + SPARK_IO.Put_String + (ReportFile, + "Total subprograms with proof completed by checker: ", 0); + SPARK_IO.Put_Integer (ReportFile, TheTotals.SubprogramsProvedByChecker, 4, 10); + SPARK_IO.New_Line (ReportFile, 1); + + SPARK_IO.Put_String + (ReportFile, + "Total subprograms with VCs discharged by review: ", 0); + SPARK_IO.Put_Integer (ReportFile, TheTotals.SubprogramsProvedByReview, 4, 10); + SPARK_IO.New_Line (ReportFile, 1); + + TotalSubprogramsProved := (((( + TheTotals.SubprogramsProvedByExaminer + + TheTotals.SubprogramsProvedBySimplifier) + + TheTotals.SubprogramsProvedWithUserProofRule) + + TheTotals.SubprogramsProvedByChecker) + + TheTotals.SubprogramsProvedByReview); + + --# assert True; + + SPARK_IO.New_Line (ReportFile, 1); + SPARK_IO.Put_Line + (ReportFile, + "Overall subprogram summary:", 0); + SPARK_IO.Put_Line + (ReportFile, + "-------------------------------------------------------------------------", 0); + SPARK_IO.Put_String + (ReportFile, + "Total subprograms fully proved: ", 0); + SPARK_IO.Put_Integer + (ReportFile, TotalSubprogramsProved, 4, 10); + SPARK_IO.New_Line (ReportFile, 1); + + SPARK_IO.Put_String + (ReportFile, + "Total subprograms with at least one undischarged VC: ", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.SubprogramsWithALOUndischargedVC, 4, 10); + + if TheTotals.SubprogramsWithALOUndischargedVC > 0 then + SPARK_IO.Put_String (ReportFile, " <<<", 0); + end if; + SPARK_IO.New_Line (ReportFile, 1); + + SPARK_IO.Put_String + (ReportFile, + "Total subprograms with at least one false VC: ", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.SubprogramsWithALOFalseVC, 4, 10); + + if TheTotals.SubprogramsWithALOFalseVC > 0 then + SPARK_IO.Put_String (ReportFile, " <<<", 0); + end if; + SPARK_IO.New_Line (ReportFile, 1); + + SPARK_IO.Put_String + (ReportFile, + " -----", 0); + + SPARK_IO.New_Line (ReportFile, 1); + SPARK_IO.Put_String + (ReportFile, + "Total subprograms for which VCs have been generated: ", 0); + SPARK_IO.Put_Integer (ReportFile, TheTotals.SubprogramsWithVCs, 4, 10); + SPARK_IO.New_Line (ReportFile, 2); + + -- Only report errors if there are some. + if (TheTotals.Subprograms_Where_VC_Analysis_Abandoned > 0) or + (TheTotals.Subprograms_Where_DPC_Analysis_Abandoned > 0) or + (TheTotals.SubprogramsWhereMissingSLGFile > 0) then + SPARK_IO.Put_Line + (ReportFile, + "WARNING: Overall error summary:", 0); + SPARK_IO.Put_Line + (ReportFile, + "-------------------------------------------------------------------------", 0); + SPARK_IO.Put_String + (ReportFile, + "Total simplified subprograms with missing slg file: ", 0); + SPARK_IO.Put_Integer (ReportFile, TheTotals.SubprogramsWhereMissingSLGFile, 7, 10); + SPARK_IO.New_Line (ReportFile, 1); + SPARK_IO.Put_String + (ReportFile, + "Total subprograms where VC analysis was abandoned due to errors: ", 0); + SPARK_IO.Put_Integer (ReportFile, TheTotals.Subprograms_Where_VC_Analysis_Abandoned, 4, 10); + SPARK_IO.New_Line (ReportFile, 1); + SPARK_IO.Put_String + (ReportFile, + "Total subprograms where DPC analysis was abandoned due to errors: ", 0); + SPARK_IO.Put_Integer (ReportFile, TheTotals.Subprograms_Where_DPC_Analysis_Abandoned, 3, 10); + SPARK_IO.New_Line (ReportFile, 2); + else + -- One blank line between each table in this group, but double blank line + -- after the last table. + SPARK_IO.New_Line (ReportFile, 1); + end if; + + -- The sum of the subprograms fully proved, + -- the subprograms with at least undischarged VC and + -- the subprograms with at least 1 false VC must equal + -- the number of subprograms for which VCs have been generated. + + SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1); + + --# assert TotalSubprogramsProved + + --# TheTotals.SubprogramsWithALOUndischargedVC + + --# TheTotals.SubprogramsWithALOFalseVC + --# = TheTotals.SubprogramsWithVCs; + + -- Check the totals are balanced. + if not TotalsAreBalanced then + FatalError (FatalErrors.SubprogramTotalsInconsistent); + end if; + + --# assert True; + + SPARK_IO.Put_Line + (ReportFile, + "ZombieScope Summary:", 0); + SPARK_IO.Put_Line + (ReportFile, + "-------------------------------------------------------------------------", 0); + SPARK_IO.Put_String + (ReportFile, + "Total subprograms for which DPCs have been generated:", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.Subprograms_With_DPCs, 20, 10); + SPARK_IO.New_Line (ReportFile, 1); + SPARK_IO.Put_String + (ReportFile, + "Total number subprograms with dead paths found:", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.Subprograms_With_Dead_Paths, 26, 10); + SPARK_IO.New_Line (ReportFile, 1); + SPARK_IO.Put_String + (ReportFile, + "Total number of dead paths found:", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.Number_Of_Dead_Paths, 40, 10); + SPARK_IO.New_Line (ReportFile, 3); + + -- Issue warning message if some DPC files have not been analysed. + + --# assert True; + + SPARK_IO.Put_Line + (ReportFile, + "VC summary:", 0); + SPARK_IO.Put_Line + (ReportFile, + "-------------------------------------------------------------------------", 0); + SPARK_IO.Put_Line + (ReportFile, + "Note: U/R denotes where the Simplifier has proved VCs using one or more " & + "user-", 0); + SPARK_IO.Put_Line + (ReportFile, "defined proof rules.", 0); + + SPARK_IO.New_Line (ReportFile, 1); + + SPARK_IO.Put_String + (ReportFile, + "Total VCs by type: ", 0); + + SPARK_IO.New_Line (ReportFile, 1); + + SPARK_IO.Put_Line + (ReportFile, + " -----------Proved By Or Using------------", 0); + SPARK_IO.Put_String + (ReportFile, + " Total Examiner Simp(U/R) Checker Review False Undiscgd", 0); + + SPARK_IO.New_Line (ReportFile, 1); + + SPARK_IO.Put_String + (ReportFile, "Assert or Post: ", 0); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsTotal (VCDetails.Assert_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedByExaminer (VCDetails.Assert_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedBySimplifier (VCDetails.Assert_Point), 7, 10); + + if TheTotals.VCsProvedWithUserProofRule (VCDetails.Assert_Point) > 0 then + SPARK_IO.Put_String (ReportFile, "(", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedWithUserProofRule (VCDetails.Assert_Point), 4, 10); + SPARK_IO.Put_String (ReportFile, ")", 0); + else + SPARK_IO.Put_String (ReportFile, " ", 0); + end if; + + --# assert True; + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedByChecker (VCDetails.Assert_Point), 9, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedByReview (VCDetails.Assert_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedFalse (VCDetails.Assert_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsUndischarged (VCDetails.Assert_Point), 8, 10); + + SPARK_IO.New_Line (ReportFile, 1); + + SPARK_IO.Put_String + (ReportFile, "Precondition check:", 0); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsTotal (VCDetails.Precondition_Check_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedByExaminer (VCDetails.Precondition_Check_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedBySimplifier (VCDetails.Precondition_Check_Point), 7, 10); + + if TheTotals.VCsProvedWithUserProofRule (VCDetails.Precondition_Check_Point) > 0 then + SPARK_IO.Put_String (ReportFile, "(", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedWithUserProofRule (VCDetails.Precondition_Check_Point), 4, 10); + SPARK_IO.Put_String (ReportFile, ")", 0); + else + SPARK_IO.Put_String (ReportFile, " ", 0); + end if; + + --# assert True; + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedByChecker (VCDetails.Precondition_Check_Point), 9, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedByReview (VCDetails.Precondition_Check_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedFalse (VCDetails.Precondition_Check_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsUndischarged (VCDetails.Precondition_Check_Point), 8, 10); + + SPARK_IO.New_Line (ReportFile, 1); + + SPARK_IO.Put_String + (ReportFile, "Check statement: ", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsTotal (VCDetails.Check_Statement_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedByExaminer (VCDetails.Check_Statement_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedBySimplifier (VCDetails.Check_Statement_Point), 7, 10); + + if TheTotals.VCsProvedWithUserProofRule (VCDetails.Check_Statement_Point) > 0 then + SPARK_IO.Put_String (ReportFile, "(", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedWithUserProofRule (VCDetails.Check_Statement_Point), 4, 10); + SPARK_IO.Put_String (ReportFile, ")", 0); + else + SPARK_IO.Put_String (ReportFile, " ", 0); + end if; + + --# assert True; + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedByChecker (VCDetails.Check_Statement_Point), 9, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedByReview (VCDetails.Check_Statement_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedFalse (VCDetails.Check_Statement_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsUndischarged (VCDetails.Check_Statement_Point), 8, 10); + + SPARK_IO.New_Line (ReportFile, 1); + + SPARK_IO.Put_String + (ReportFile, "Runtime check: ", 0); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsTotal (VCDetails.Runtime_Check_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedByExaminer (VCDetails.Runtime_Check_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedBySimplifier (VCDetails.Runtime_Check_Point), 7, 10); + + if TheTotals.VCsProvedWithUserProofRule (VCDetails.Runtime_Check_Point) > 0 then + SPARK_IO.Put_String (ReportFile, "(", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedWithUserProofRule (VCDetails.Runtime_Check_Point), 4, 10); + SPARK_IO.Put_String (ReportFile, ")", 0); + else + SPARK_IO.Put_String (ReportFile, " ", 0); + end if; + + --# assert True; + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedByChecker (VCDetails.Runtime_Check_Point), 9, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedByReview (VCDetails.Runtime_Check_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedFalse (VCDetails.Runtime_Check_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsUndischarged (VCDetails.Runtime_Check_Point), 8, 10); + + SPARK_IO.New_Line (ReportFile, 1); + + + SPARK_IO.Put_String + (ReportFile, "Refinement VCs: ", 0); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsTotal (VCDetails.Refinement_VC_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedByExaminer (VCDetails.Refinement_VC_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedBySimplifier (VCDetails.Refinement_VC_Point), 7, 10); + + if TheTotals.VCsProvedWithUserProofRule (VCDetails.Refinement_VC_Point) > 0 then + SPARK_IO.Put_String (ReportFile, "(", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedWithUserProofRule (VCDetails.Refinement_VC_Point), 4, 10); + SPARK_IO.Put_String (ReportFile, ")", 0); + else + SPARK_IO.Put_String (ReportFile, " ", 0); + end if; + + --# assert True; + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedByChecker (VCDetails.Refinement_VC_Point), 9, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedByReview (VCDetails.Refinement_VC_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedFalse (VCDetails.Refinement_VC_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsUndischarged (VCDetails.Refinement_VC_Point), 8, 10); + + SPARK_IO.New_Line (ReportFile, 1); + + SPARK_IO.Put_String + (ReportFile, "Inheritance VCs: ", 0); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsTotal (VCDetails.Inheritance_VC_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedByExaminer (VCDetails.Inheritance_VC_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedBySimplifier (VCDetails.Inheritance_VC_Point), 7, 10); + + if TheTotals.VCsProvedWithUserProofRule (VCDetails.Inheritance_VC_Point) > 0 then + SPARK_IO.Put_String (ReportFile, "(", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedWithUserProofRule (VCDetails.Inheritance_VC_Point), 4, 10); + SPARK_IO.Put_String (ReportFile, ")", 0); + else + SPARK_IO.Put_String (ReportFile, " ", 0); + end if; + + --# assert True; + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedByChecker (VCDetails.Undetermined_Point), 9, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedFalse (VCDetails.Inheritance_VC_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedByReview (VCDetails.Inheritance_VC_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsUndischarged (VCDetails.Inheritance_VC_Point), 8, 10); + + SPARK_IO.New_Line (ReportFile, 1); + + -- Assuming a well-structured set of VCG, SIV and PLG files, + -- the number of Undetermined_Point VCs should always be + -- zero. + -- + -- A corrupt VCG file might lead to an Undetermined_Point + -- VC, so we only output the total if it's non-zero... + + if TheTotals.VCsTotal (VCDetails.Undetermined_Point) > 0 then + SPARK_IO.Put_String + (ReportFile, "Undetermined: ", 0); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsTotal (VCDetails.Undetermined_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedByExaminer (VCDetails.Undetermined_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedBySimplifier (VCDetails.Undetermined_Point), 7, 10); + + if TheTotals.VCsProvedWithUserProofRule (VCDetails.Undetermined_Point) > 0 then + SPARK_IO.Put_String (ReportFile, "(", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedWithUserProofRule (VCDetails.Undetermined_Point), 4, 10); + SPARK_IO.Put_String (ReportFile, ")", 0); + else + SPARK_IO.Put_String (ReportFile, " ", 0); + end if; + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedByChecker (VCDetails.Undetermined_Point), 9, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedByReview (VCDetails.Undetermined_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsProvedFalse (VCDetails.Undetermined_Point), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, TheTotals.VCsUndischarged (VCDetails.Undetermined_Point), 8, 10); + + SPARK_IO.New_Line (ReportFile, 1); + end if; + + --# assert True; + + SPARK_IO.Put_String + (ReportFile, Banner.MajorSeparatorLine, 0); + + SPARK_IO.New_Line (ReportFile, 1); + + SPARK_IO.Put_String + (ReportFile, "Totals: ", 0); + + SPARK_IO.Put_Integer + (ReportFile, Sum (TheTotals.VCsTotal), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, Sum (TheTotals.VCsProvedByExaminer), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, Sum (TheTotals.VCsProvedBySimplifier), 7, 10); + + if Sum (TheTotals.VCsProvedWithUserProofRule) > 0 then + SPARK_IO.Put_String (ReportFile, "(", 0); + SPARK_IO.Put_Integer + (ReportFile, Sum (TheTotals.VCsProvedWithUserProofRule), 4, 10); + SPARK_IO.Put_String (ReportFile, ")", 0); + else + SPARK_IO.Put_String (ReportFile, " ", 0); + end if; + + --# assert True; + + SPARK_IO.Put_Integer + (ReportFile, Sum (TheTotals.VCsProvedByChecker), 9, 10); + + SPARK_IO.Put_Integer + (ReportFile, Sum (TheTotals.VCsProvedByReview), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, Sum (TheTotals.VCsProvedFalse), 7, 10); + + SPARK_IO.Put_Integer + (ReportFile, Sum (TheTotals.VCsUndischarged), 8, 10); + + if Sum (TheTotals.VCsUndischarged) > 0 then + SPARK_IO.Put_String (ReportFile, " <<<", 0); + end if; + + --# assert True; + + SPARK_IO.New_Line (ReportFile, 1); + + if CommandLine.Data.OutputPercentUndischarged and then + Sum (TheTotals.VCsTotal) /= 0 then + + CalcuatePercentages (TheTotals, + PercentUndischargedStr, + PercentProvedByExaminerStr, + PercentProvedByCheckerStr, + PercentProvedByReviewStr, + PercentSimplifiedStr, + PercentWithUserRuleStr, + PercentProvedFalseStr); + + SPARK_IO.Put_String (ReportFile, "% Totals: ", 0); + EStrings.Put_String (File => ReportFile, + E_Str => PercentProvedByExaminerStr); + SPARK_IO.Put_String (ReportFile, " ", 0); + EStrings.Put_String (File => ReportFile, + E_Str => PercentSimplifiedStr); + + if Sum (TheTotals.VCsProvedWithUserProofRule) > 0 then + SPARK_IO.Put_String (ReportFile, "(", 0); -- 1 char + EStrings.Put_String (File => ReportFile, + E_Str => PercentWithUserRuleStr); -- 5 char + SPARK_IO.Put_String (ReportFile, ")", 0); -- 1 char + else + SPARK_IO.Put_String (ReportFile, " ", 0); -- 1+5+1 = 7 char + end if; + + SPARK_IO.Put_String (ReportFile, " ", 0); + EStrings.Put_String (File => ReportFile, + E_Str => PercentProvedByCheckerStr); + SPARK_IO.Put_String (ReportFile, " ", 0); + EStrings.Put_String (File => ReportFile, + E_Str => PercentProvedByReviewStr); + SPARK_IO.Put_String (ReportFile, " ", 0); + EStrings.Put_String (File => ReportFile, + E_Str => PercentProvedFalseStr); + SPARK_IO.Put_String (ReportFile, " ", 0); + EStrings.Put_String (File => ReportFile, + E_Str => PercentUndischargedStr); + + -- Only suppress the 'look out' tag if everything has been proved, and + -- there are no false VCs. + if not ((EStrings.Eq1_String (E_Str => PercentUndischargedStr, + Str => " 0%") and then + EStrings.Eq1_String (E_Str => PercentProvedFalseStr, + Str => " 0%"))) then + SPARK_IO.Put_String (ReportFile, " <<<", 0); + end if; + SPARK_IO.New_Line (ReportFile, 1); + end if; + + --# assert True; + + -- Only report errors if there are some. + if TheTotals.Subprograms_Where_VC_Analysis_Abandoned > 0 then + SPARK_IO.Put_String + (ReportFile, "!!! ERRORS IN SIV FILES !!!", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.Subprograms_Where_VC_Analysis_Abandoned, 8, 10); + SPARK_IO.New_Line (ReportFile, 1); + end if; + + if TheTotals.Subprograms_Where_DPC_Analysis_Abandoned > 0 then + SPARK_IO.Put_String + (ReportFile, "!!! ERRORS IN DPC FILES !!!", 0); + SPARK_IO.Put_Integer + (ReportFile, TheTotals.Subprograms_Where_DPC_Analysis_Abandoned, 8, 10); + SPARK_IO.New_Line (ReportFile, 1); + end if; + + --# assert True; + + --# accept F, 33, TempStatus, "TempStatus not used here" & + --# F, 33, TempStoreBool, "TempStoreBool not used here" & + --# F, 601, TempRulesUsedFile, SPARK_IO.File_Sys, "False coupling through SPARK_IO" & + --# F, 601, TempRulesUsedFile, ReportFile, "False coupling through SPARK_IO" & + --# F, 601, TempRulesUsedFile, TempRluErrorFile, "False coupling through SPARK_IO" & + --# F, 601, TempRulesUsedFile, TempWarnErrorFile, "False coupling through SPARK_IO"; + end Output; + + + procedure XMLOutput (ReportFile : in SPARK_IO.File_Type) + --# global in TheTotals; + --# in out SPARK_IO.File_Sys; + --# in out XMLSummary.State; + --# derives SPARK_IO.File_Sys from *, + --# ReportFile, + --# TheTotals, + --# XMLSummary.State & + --# XMLSummary.State from *, + --# TheTotals; + is + PercentUndischargedStr : EStrings.T; + PercentProvedByExaminerStr : EStrings.T; + PercentProvedByCheckerStr : EStrings.T; + PercentProvedByReviewStr : EStrings.T; + PercentSimplifiedStr : EStrings.T; + PercentWithUserRuleStr : EStrings.T; + PercentProvedFalseStr : EStrings.T; + begin + + -- Check the totals are balanced. + if not TotalsAreBalanced then + FatalError (FatalErrors.SubprogramTotalsInconsistent); + end if; + + XMLSummary.StartSummary (ReportFile); + + XMLSummary.StartSubprogramSummary (TheTotals.SubprogramsWithVCs, + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITExaminer, + TheTotals.SubprogramsProvedByExaminer, + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITSimplifier, + TheTotals.SubprogramsProvedBySimplifier, + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITChecker, + TheTotals.SubprogramsProvedByChecker, + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITReview, + TheTotals.SubprogramsProvedByReview, + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITFalse, + TheTotals.SubprogramsWithALOFalseVC, + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITUndischarged, + TheTotals.SubprogramsWithALOUndischargedVC, + ReportFile); + + XMLSummary.EndSubprogramSummary (ReportFile); + + --# assert True; + + -- In XML always report number of errors, even if they are zero. + -- (It seems better for parsing not to hide XML entries.) + -- This is deliberately not nested inside the subprograms tag above, as + -- this is implicitly describing only well-formed subprograms. + XMLSummary.StartSubprogramsInErrorSummary (TheTotals.Subprograms_Where_VC_Analysis_Abandoned, + ReportFile); + ---- Nothing inside this tag just now. + XMLSummary.EndSubprogramsInErrorSummary (ReportFile); + + --# assert True; + + XMLSummary.StartVCSummary (ReportFile); + + XMLSummary.StartSummarySection (XMLSummary.SSAssert_Post, + TheTotals.VCsTotal (VCDetails.Assert_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITExaminer, + TheTotals.VCsProvedByExaminer (VCDetails.Assert_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITSimplifier, + TheTotals.VCsProvedBySimplifier (VCDetails.Assert_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITChecker, + TheTotals.VCsProvedByChecker (VCDetails.Assert_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITReview, + TheTotals.VCsProvedByReview (VCDetails.Assert_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITFalse, + TheTotals.VCsProvedFalse (VCDetails.Assert_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITUndischarged, + TheTotals.VCsUndischarged (VCDetails.Assert_Point), + ReportFile); + + XMLSummary.EndSummarySection (ReportFile); + + --# assert True; + + XMLSummary.StartSummarySection (XMLSummary.SSPrecondition, + TheTotals.VCsTotal (VCDetails.Precondition_Check_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITExaminer, + TheTotals.VCsProvedByExaminer (VCDetails.Precondition_Check_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITSimplifier, + TheTotals.VCsProvedBySimplifier (VCDetails.Precondition_Check_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITChecker, + TheTotals.VCsProvedByChecker (VCDetails.Precondition_Check_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITReview, + TheTotals.VCsProvedByReview (VCDetails.Precondition_Check_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITFalse, + TheTotals.VCsProvedFalse (VCDetails.Precondition_Check_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITUndischarged, + TheTotals.VCsUndischarged (VCDetails.Precondition_Check_Point), + ReportFile); + + XMLSummary.EndSummarySection (ReportFile); + + --# assert True; + + XMLSummary.StartSummarySection (XMLSummary.SSCheck, + TheTotals.VCsTotal (VCDetails.Check_Statement_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITExaminer, + TheTotals.VCsProvedByExaminer (VCDetails.Check_Statement_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITSimplifier, + TheTotals.VCsProvedBySimplifier (VCDetails.Check_Statement_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITChecker, + TheTotals.VCsProvedByChecker (VCDetails.Check_Statement_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITReview, + TheTotals.VCsProvedByReview (VCDetails.Check_Statement_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITFalse, + TheTotals.VCsProvedFalse (VCDetails.Check_Statement_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITUndischarged, + TheTotals.VCsUndischarged (VCDetails.Check_Statement_Point), + ReportFile); + + XMLSummary.EndSummarySection (ReportFile); + + --# assert True; + + XMLSummary.StartSummarySection (XMLSummary.SSRuntime, + TheTotals.VCsTotal (VCDetails.Runtime_Check_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITExaminer, + TheTotals.VCsProvedByExaminer (VCDetails.Runtime_Check_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITSimplifier, + TheTotals.VCsProvedBySimplifier (VCDetails.Runtime_Check_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITChecker, + TheTotals.VCsProvedByChecker (VCDetails.Runtime_Check_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITReview, + TheTotals.VCsProvedByReview (VCDetails.Runtime_Check_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITFalse, + TheTotals.VCsProvedFalse (VCDetails.Runtime_Check_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITUndischarged, + TheTotals.VCsUndischarged (VCDetails.Runtime_Check_Point), + ReportFile); + + XMLSummary.EndSummarySection (ReportFile); + + --# assert True; + + + XMLSummary.StartSummarySection (XMLSummary.SSRefinement, + TheTotals.VCsTotal (VCDetails.Refinement_VC_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITExaminer, + TheTotals.VCsProvedByExaminer (VCDetails.Refinement_VC_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITSimplifier, + TheTotals.VCsProvedBySimplifier (VCDetails.Refinement_VC_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITChecker, + TheTotals.VCsProvedByChecker (VCDetails.Refinement_VC_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITReview, + TheTotals.VCsProvedByReview (VCDetails.Refinement_VC_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITFalse, + TheTotals.VCsProvedFalse (VCDetails.Refinement_VC_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITUndischarged, + TheTotals.VCsUndischarged (VCDetails.Refinement_VC_Point), + ReportFile); + + XMLSummary.EndSummarySection (ReportFile); + + + --# assert True; + + XMLSummary.StartSummarySection (XMLSummary.SSInheritance, + TheTotals.VCsTotal (VCDetails.Inheritance_VC_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITExaminer, + TheTotals.VCsProvedByExaminer (VCDetails.Inheritance_VC_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITSimplifier, + TheTotals.VCsProvedBySimplifier (VCDetails.Inheritance_VC_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITChecker, + TheTotals.VCsProvedByChecker (VCDetails.Inheritance_VC_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITReview, + TheTotals.VCsProvedByReview (VCDetails.Inheritance_VC_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITFalse, + TheTotals.VCsProvedFalse (VCDetails.Inheritance_VC_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITUndischarged, + TheTotals.VCsUndischarged (VCDetails.Inheritance_VC_Point), + ReportFile); + + XMLSummary.EndSummarySection (ReportFile); + + + --# assert True; + + XMLSummary.StartSummarySection (XMLSummary.SSUndetermined, + TheTotals.VCsTotal (VCDetails.Undetermined_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITExaminer, + TheTotals.VCsProvedByExaminer (VCDetails.Undetermined_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITSimplifier, + TheTotals.VCsProvedBySimplifier (VCDetails.Undetermined_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITChecker, + TheTotals.VCsProvedByChecker (VCDetails.Undetermined_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITReview, + TheTotals.VCsProvedByReview (VCDetails.Undetermined_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITFalse, + TheTotals.VCsProvedFalse (VCDetails.Undetermined_Point), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITUndischarged, + TheTotals.VCsUndischarged (VCDetails.Undetermined_Point), + ReportFile); + + XMLSummary.EndSummarySection (ReportFile); + + + --# assert True; + + XMLSummary.StartSummarySection (XMLSummary.SSTotals, + Sum (TheTotals.VCsTotal), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITExaminer, + Sum (TheTotals.VCsProvedByExaminer), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITSimplifier, + Sum (TheTotals.VCsProvedBySimplifier), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITChecker, + Sum (TheTotals.VCsProvedByChecker), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITReview, + Sum (TheTotals.VCsProvedByReview), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITFalse, + Sum (TheTotals.VCsProvedFalse), + ReportFile); + + XMLSummary.SummaryItemInt (XMLSummary.ITUndischarged, + Sum (TheTotals.VCsUndischarged), + ReportFile); + + XMLSummary.EndSummarySection (ReportFile); + + --# assert True; + + if Sum (TheTotals.VCsTotal) /= 0 then + + CalcuatePercentages (TheTotals, + PercentUndischargedStr, + PercentProvedByExaminerStr, + PercentProvedByCheckerStr, + PercentProvedByReviewStr, + PercentSimplifiedStr, + PercentWithUserRuleStr, + PercentProvedFalseStr); + + XMLSummary.StartSummarySection (XMLSummary.SSPercentages, + Sum (TheTotals.VCsTotal), + ReportFile); + + XMLSummary.SummaryItemStr (XMLSummary.ITExaminer, + EStrings.Trim (PercentProvedByExaminerStr), + ReportFile); + + XMLSummary.SummaryItemStr (XMLSummary.ITSimplifier, + EStrings.Trim (PercentSimplifiedStr), + ReportFile); + + XMLSummary.SummaryItemStr (XMLSummary.ITSimplifierUserRule, + EStrings.Trim (PercentWithUserRuleStr), + ReportFile); + + XMLSummary.SummaryItemStr (XMLSummary.ITChecker, + EStrings.Trim (PercentProvedByCheckerStr), + ReportFile); + + XMLSummary.SummaryItemStr (XMLSummary.ITReview, + EStrings.Trim (PercentProvedByReviewStr), + ReportFile); + + XMLSummary.SummaryItemStr (XMLSummary.ITFalse, + EStrings.Trim (PercentProvedFalseStr), + ReportFile); + + XMLSummary.SummaryItemStr (XMLSummary.ITUndischarged, + EStrings.Trim (PercentUndischargedStr), + ReportFile); + + XMLSummary.EndSummarySection (ReportFile); + + end if; + + XMLSummary.EndVCSummary (ReportFile); + + XMLSummary.EndSummary (ReportFile); + + end XMLOutput; + +begin + TheTotals := TotalType'(SubprogramsWithVCs => 0, + SubprogramsWhereMissingSLGFile => 0, + Subprograms_Where_VC_Analysis_Abandoned => 0, + Subprograms_Where_DPC_Analysis_Abandoned => 0, + SubprogramsWithALOUndischargedVC => 0, + SubprogramsWithALOExaminerVC => 0, + SubprogramsWithALOSimplifierVC => 0, + SubprogramsWithALOContradictionVC => 0, + SubprogramsWithALOUserRuleVC => 0, + SubprogramsWithALOCheckerVC => 0, + SubprogramsWithALOReviewVC => 0, + SubprogramsWithALOFalseVC => 0, + SubprogramsProvedByExaminer => 0, + SubprogramsProvedBySimplifier => 0, + SubprogramsProvedByChecker => 0, + SubprogramsProvedWithUserProofRule => 0, + SubprogramsProvedByReview => 0, + VCsTotal => NullVCCounter, + VCsProvedByExaminer => NullVCCounter, + VCsProvedBySimplifier => NullVCCounter, + VCsProvedByChecker => NullVCCounter, + VCsProvedWithUserProofRule => NullVCCounter, + VCsProvedByReview => NullVCCounter, + VCsProvedFalse => NullVCCounter, + VCsUndischarged => NullVCCounter, + Subprograms_With_DPCs => 0, + Subprograms_With_Dead_Paths => 0, + Number_Of_Dead_Paths => 0); +end Total; diff --git a/pogs/total.ads b/pogs/total.ads index 7fe0daa..c64ea1c 100644 --- a/pogs/total.ads +++ b/pogs/total.ads @@ -31,6 +31,7 @@ with SPARK_IO; --# EStrings, --# FatalErrors, --# Heap, +--# RuleListADT, --# SPARK_IO, --# VCDetails, --# VCHeap, @@ -55,6 +56,7 @@ is TempUserFile : in out SPARK_IO.File_Type; TempRluErrorFile : in out SPARK_IO.File_Type; TempRluUsedFile : in out SPARK_IO.File_Type; + TempRulesUsedFile : in out SPARK_IO.File_Type; TempPRVerrFile : in out SPARK_IO.File_Type; TempWarnErrorFile : in out SPARK_IO.File_Type; TempSDPErrorFile : in out SPARK_IO.File_Type; @@ -72,6 +74,8 @@ is --# TempSDPErrorFile, --# TempUserFile, --# TempWarnErrorFile from * & + --# TempRulesUsedFile from *, + --# TempRluUsedFile & --# SPARK_IO.File_Sys from *, --# CommandLine.Data, --# ReportFile, @@ -83,6 +87,7 @@ is --# TempPRVerrFile, --# TempRluErrorFile, --# TempRluUsedFile, + --# TempRulesUsedFile, --# TempSDPErrorFile, --# TempUserFile, --# TempWarnErrorFile; diff --git a/pogs/vcs-analysesimplogfile.adb b/pogs/vcs-analysesimplogfile.adb index 09b24d6..f1a07b9 100644 --- a/pogs/vcs-analysesimplogfile.adb +++ b/pogs/vcs-analysesimplogfile.adb @@ -38,6 +38,7 @@ procedure AnalyseSimpLogFile FileName : in ELStrings.T; RuleFilesErrors : in out SPARK_IO.File_Type; RuleFilesUsed : in out SPARK_IO.File_Type; + RulesUsed : in SPARK_IO.File_Type; SLGErrorInFile : out Boolean) is RuleLine : ELStrings.T; @@ -168,6 +169,9 @@ begin -- AnalyseSimpLogFile ELStrings.Put_Line (File => RuleFilesUsed, E_Str => RuleFileWithPath); end if; + -- And add the rulefile to the Rules used file + ELStrings.Put_Line (File => RulesUsed, + E_Str => RuleFileWithPath); -- Output to the report if not EncounteredARuleFile then @@ -203,6 +207,10 @@ begin -- AnalyseSimpLogFile EStrings.Put_Line (File => ReportFile, E_Str => OutputLine); + -- Add the rule to the Rules used file. + EStrings.Put_Line (File => RulesUsed, + E_Str => Rule); + EncounteredAVC := False; OutputLine := EStrings.Copy_String (Str => " "); SLGParserVCStatus := SLG_Parser.Success; @@ -247,6 +255,10 @@ begin -- AnalyseSimpLogFile end loop; + -- Empty string terminates the rules for this file in this log. + EStrings.Put_Line (File => RulesUsed, + E_Str => EStrings.Empty_String); + -- Must have found a rule if not EncounteredARule or SLGParserRuleStatus = SLG_Parser.Unexpected_Text then @@ -276,5 +288,6 @@ begin -- AnalyseSimpLogFile --# accept Flow, 33, Success, "Expect Success unused" & --# Flow, 601, RuleFilesUsed, ReportFile, "False coupling through SPARK_IO" & - --# Flow, 601, RuleFilesUsed, RuleFilesErrors, "False coupling through SPARK_IO"; + --# Flow, 601, RuleFilesUsed, RuleFilesErrors, "False coupling through SPARK_IO" & + --# Flow, 601, RuleFilesUsed, RulesUsed, "False coupling through SPARK_IO"; end AnalyseSimpLogFile; diff --git a/pogs/vcs.adb b/pogs/vcs.adb index 09596ae..8ea1b7d 100644 --- a/pogs/vcs.adb +++ b/pogs/vcs.adb @@ -678,6 +678,7 @@ is FileName : in ELStrings.T; RuleFilesErrors : in out SPARK_IO.File_Type; RuleFilesUsed : in out SPARK_IO.File_Type; + RulesUsed : in SPARK_IO.File_Type; SLGErrorInFile : out Boolean) --# global in CommandLine.Data; --# in out FatalErrors.State; @@ -689,6 +690,7 @@ is --# ReportFile, --# RuleFilesErrors, --# RuleFilesUsed, + --# RulesUsed, --# SPARK_IO.File_sys & --# RuleFilesErrors, --# RuleFilesUsed from *, @@ -700,6 +702,7 @@ is --# ReportFile, --# RuleFilesErrors, --# RuleFilesUsed, + --# RulesUsed, --# SPARK_IO.File_sys; -- precondition to entering this procedure is that the SLG file exists -- and XML output is not selected. @@ -717,6 +720,7 @@ is TempUserFile : in SPARK_IO.File_Type; TempRluErrorFile : in out SPARK_IO.File_Type; TempRluUsedFile : in out SPARK_IO.File_Type; + TempRulesUsedFile : in SPARK_IO.File_Type; TempPRVerrFile : in SPARK_IO.File_Type; TempWarnErrorFile : in SPARK_IO.File_Type; Temp_SDP_Error_File : in SPARK_IO.File_Type; @@ -941,6 +945,7 @@ is SimplifierLogFileName, --in TempRluErrorFile, --in out TempRluUsedFile, --in out + TempRulesUsedFile, --in SLGFileContainedError); -- out if SLGFileContainedError then @@ -1149,10 +1154,13 @@ is --# accept Flow, 601, XMLSummary.State, TempRluErrorFile, "False coupling through SPARK_IO" & --# Flow, 601, XMLSummary.State, TempRluUsedFile, "False coupling through SPARK_IO" & + --# Flow, 601, XMLSummary.State, TempRulesUsedFile, "False coupling through SPARK_IO" & --# Flow, 601, VCHeap.State, TempRluErrorFile, "False coupling through SPARK_IO" & --# Flow, 601, VCHeap.State, TempRluUsedFile, "False coupling through SPARK_IO" & + --# Flow, 601, VCHeap.State, TempRulesUsedFile, "False coupling through SPARK_IO" & --# Flow, 601, Total.State, TempRluErrorFile, "False coupling through SPARK_IO" & --# Flow, 601, Total.State, TempRluUsedFile, "False coupling through SPARK_IO" & + --# Flow, 601, Total.State, TempRulesUsedFile, "False coupling through SPARK_IO" & --# Flow, 601, TempRluErrorFile, CommandLine.Data, "False coupling through SPARK_IO" & --# Flow, 601, TempRluUsedFile, CommandLine.Data, "False coupling through SPARK_IO" & --# Flow, 601, TempRluErrorFile, ReportFile, "False coupling through SPARK_IO" & diff --git a/pogs/vcs.ads b/pogs/vcs.ads index 2b0c7cb..8c12740 100644 --- a/pogs/vcs.ads +++ b/pogs/vcs.ads @@ -58,6 +58,7 @@ is TempUserFile : in SPARK_IO.File_Type; TempRluErrorFile : in out SPARK_IO.File_Type; TempRluUsedFile : in out SPARK_IO.File_Type; + TempRulesUsedFile : in SPARK_IO.File_Type; TempPRVerrFile : in SPARK_IO.File_Type; TempWarnErrorFile : in SPARK_IO.File_Type; Temp_SDP_Error_File : in SPARK_IO.File_Type; @@ -99,6 +100,7 @@ is --# SPARK_IO.File_sys, --# TempRluErrorFile, --# TempRluUsedFile, + --# TempRulesUsedFile, --# VCHeap.I_State, --# VCHeap.State & --# SPARK_IO.File_sys from *, @@ -113,6 +115,7 @@ is --# TempPRVerrFile, --# TempRluErrorFile, --# TempRluUsedFile, + --# TempRulesUsedFile, --# TempUserFile, --# TempWarnErrorFile, --# Temp_DPC_Error_File, -- 1.7.0.2.msysgit.0 From 33c8f4221e5f0c322a1b90fb6e8164665d13cf43 Mon Sep 17 00:00:00 2001 From: Phil Thornley Date: Fri, 13 Aug 2010 16:51:48 +0100 Subject: [PATCH 2/2] Commit of new files. New files added for printing the rules lists. --- pogs/rulelistadt.adb | 222 ++++++++++++++++++++++++++++++++ pogs/rulelistadt.ads | 96 ++++++++++++++ pogs/total-rulesusedforfile.adb | 269 +++++++++++++++++++++++++++++++++++++++ 3 files changed, 587 insertions(+), 0 deletions(-) create mode 100644 pogs/rulelistadt.adb create mode 100644 pogs/rulelistadt.ads create mode 100644 pogs/total-rulesusedforfile.adb diff --git a/pogs/rulelistadt.adb b/pogs/rulelistadt.adb new file mode 100644 index 0000000..07b3b49 --- /dev/null +++ b/pogs/rulelistadt.adb @@ -0,0 +1,222 @@ +-------------------------------------------------------------------------------- +-- (C) Phil Thornley +-------------------------------------------------------------------------------- +-- +-- This modification to the SPARK toolset is free software; you can redistribute +-- it and/or modify it under terms of the GNU General Public License as +-- published by the Free Software Foundation; either version 3, or (at your +-- option) any later version. This modification to the SPARK toolset is +-- distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; +-- without even the implied warranty of MERCHANTABILITY or FITNESS FOR A +-- PARTICULAR PURPOSE. See the GNU General Public License for more details. +-- You should have received a copy of the GNU General Public License distributed +-- with the SPARK toolset; see file COPYING3. If not, go to +-- http://www.gnu.org/licenses for a complete copy of the license. +-- +--============================================================================== + + +-- ****** This package is not implemented in SPARK ****** -- + + +-------------------------------------------------------------------------------- +--Synopsis: -- +-- -- +--Package providing a data structure to store a set of rule names and to -- +--recover sequences for columns in row order. -- +-- -- +-------------------------------------------------------------------------------- + +package body RuleListADT is + + use type EStrings.Order_Types; + use type StringLists.Cursor; + + --------------------------------------------------------------------------- + -- Internal Operations + --------------------------------------------------------------------------- + + --------------------------------------------------------------------------- + -- Returns the numeric value of the rule number. + --------------------------------------------------------------------------- + function RuleNumber (Name : EStrings.T; + Posn : EStrings.Positions) return Natural + is + RuleNo : Natural := 0; + Pos : Natural; + Pos0 : constant := Character'Pos('0'); + begin + Pos := Posn; + while EStrings.Get_Element (Name, Pos) /= ')' loop + RuleNo := + RuleNo * 10 + + (Character'Pos (EStrings.Get_Element (Name, Pos)) - Pos0); + Pos := Pos + 1; + end loop; + return RuleNo; + end RuleNumber; + + --------------------------------------------------------------------------- + -- Compares two rulenames to determine whether they are equal and, if not, + -- which should be listed first. Rules with the same rule family name are + -- ordered by rule number. + -- The implementation is a modification of the function Lex_Order in the + -- package EStrings. + --------------------------------------------------------------------------- + function RuleOrder (FirstName, SecondName : EStrings.T) + return EStrings.Order_Types + is + Pos : EStrings.Positions := 1; + Finished : Boolean := False; + OrderResult : EStrings.Order_Types; + + RankOfNextCharInFirst : Integer; + RankOfNextCharInSecond : Integer; + + FirstRuleNumber : Natural; + SecondRuleNumber : Natural; + begin + while not Finished loop + -- if the remainder of only one of the strings is empty then + -- that is the first in order + -- if the remainder of both is empty then neither is first + if Pos > EStrings.Get_Length (FirstName) + and Pos <= EStrings.Get_Length (SecondName) + then + OrderResult := EStrings.First_One_First; + Finished := True; + elsif Pos > EStrings.Get_Length (SecondName) + and Pos <= EStrings.Get_Length (FirstName) + then + OrderResult := EStrings.Second_One_First; + Finished := True; + elsif Pos > EStrings.Get_Length (FirstName) + and Pos > EStrings.Get_Length (SecondName) + then + OrderResult := EStrings.Neither_First; + Finished := True; + else + -- decide using the current Character in the string + RankOfNextCharInFirst := + Character'Pos (EStrings.Get_Element (FirstName, Pos)); + RankOfNextCharInSecond := + Character'Pos (EStrings.Get_Element (SecondName, Pos)); + + if RankOfNextCharInFirst < RankOfNextCharInSecond then + OrderResult := EStrings.First_One_First; + Finished := True; + elsif RankOfNextCharInSecond < RankOfNextCharInFirst then + OrderResult := EStrings.Second_One_First; + Finished := True; + else + if Pos < EStrings.Positions'Last then + Pos := Pos + 1; + else + OrderResult := EStrings.Neither_First; + Finished := True; + end if; + end if; + + if EStrings.Get_Element (FirstName, Pos) = '(' then + FirstRuleNumber := RuleNumber (FirstName, Pos + 1); + SecondRuleNumber := RuleNumber (SecondName, Pos + 1); + if FirstRuleNumber < SecondRuleNumber then + OrderResult := EStrings.First_One_First; + Finished := True; + elsif SecondRuleNumber < FirstRuleNumber then + OrderResult := EStrings.Second_One_First; + Finished := True; + end if; + end if; + end if; + end loop; + + return OrderResult; + end RuleOrder; + + --------------------------------------------------------------------------- + -- Provided Operations + --------------------------------------------------------------------------- + + --------------------------------------------------------------------------- + procedure Initialize (RuleList : out T) + is + begin + RuleList := T'(Rules => StringLists.Empty_List, + ColumnRules => Cursors'(others => StringLists.No_Element)); + end Initialize; + + --------------------------------------------------------------------------- + procedure AddRule (RuleList : in out T; + Rule : in EStrings.T) + is + Current : StringLists.Cursor; + Compare : EStrings.Order_Types; + begin + Current := StringLists.First (RuleList.Rules); + if Current = StringLists.No_Element + or else + RuleOrder + (FirstName => Rule, + SecondName => + StringLists.Element (Current)) = EStrings.First_One_First + then + StringLists.Prepend (RuleList.Rules, + Rule); + else + while Current /= StringLists.No_Element loop + Compare := + RuleOrder (FirstName => Rule, + SecondName => StringLists.Element (Current)); + exit when Compare /= EStrings.Second_One_First; + StringLists.Next (Current); + end loop; + if Current = StringLists.No_Element then + StringLists.Append (RuleList.Rules, + Rule); + elsif Compare = EStrings.First_One_First then + StringLists.Insert (RuleList.Rules, + Current, + Rule); + end if; + end if; + end AddRule; + + --------------------------------------------------------------------------- + function GetRuleCount (RuleList : T) return Natural + is + begin + return Integer (StringLists.Length (RuleList.Rules)); + end GetRuleCount; + + --------------------------------------------------------------------------- + procedure SetColumns (RuleList : in out T; + Columns : in ColumnIDs; + FullRows : in Positive; + ExtraRow : in Natural) + is + begin + RuleList.ColumnRules (1) := StringLists.First (RuleList.Rules); + for I in ColumnIDs range 2 .. Columns loop + RuleList.ColumnRules (I) := RuleList.ColumnRules (I - 1); + for R in Integer range 1 .. FullRows loop + StringLists.Next (RuleList.ColumnRules (I)); + end loop; + if I - 1 <= ExtraRow then + StringLists.Next (RuleList.ColumnRules (I)); + end if; + end loop; + end SetColumns; + + --------------------------------------------------------------------------- + procedure GetNextRule (RuleList : in out T; + Column : in ColumnIDs; + Rule : out EStrings.T) + is + begin + Rule := StringLists.Element (RuleList.ColumnRules (Column)); + StringLists.Next (RuleList.ColumnRules (Column)); + end GetNextRule; + --------------------------------------------------------------------------- + +end RuleListADT; diff --git a/pogs/rulelistadt.ads b/pogs/rulelistadt.ads new file mode 100644 index 0000000..6f351f2 --- /dev/null +++ b/pogs/rulelistadt.ads @@ -0,0 +1,96 @@ +-------------------------------------------------------------------------------- +-- (C) Phil Thornley +-------------------------------------------------------------------------------- +-- +-- This modification to the SPARK toolset is free software; you can redistribute +-- it and/or modify it under terms of the GNU General Public License as +-- published by the Free Software Foundation; either version 3, or (at your +-- option) any later version. This modification to the SPARK toolset is +-- distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; +-- without even the implied warranty of MERCHANTABILITY or FITNESS FOR A +-- PARTICULAR PURPOSE. See the GNU General Public License for more details. +-- You should have received a copy of the GNU General Public License distributed +-- with the SPARK toolset; see file COPYING3. If not, go to +-- http://www.gnu.org/licenses for a complete copy of the license. +-- +--============================================================================== + + +-------------------------------------------------------------------------------- +--Synopsis: -- +-- -- +--Package providing a data structure to store a set of rule names and to -- +--recover sequences for columns in row order. -- +-- -- +-------------------------------------------------------------------------------- + +with Ada.Containers.Doubly_Linked_Lists; + +with EStrings; + +--# inherit EStrings; +package RuleListADT +is + + type T is private; + + -- Copy of constant defined in Total.RulesUsedForFile. + MaxColumns : constant := 10; + + subtype ColumnIDs is Positive range 1 .. MaxColumns; + + --------------------------------------------------------------------------- + procedure Initialize (RuleList : out T); + --# derives RuleList from ; + + --------------------------------------------------------------------------- + function GetRuleCount (RuleList : T) return Natural; + + --------------------------------------------------------------------------- + procedure AddRule (RuleList : in out T; + Rule : in EStrings.T); + --# derives RuleList from *, + --# Rule; + + --------------------------------------------------------------------------- + -- Initialize the column cursors for each column. + --------------------------------------------------------------------------- + procedure SetColumns (RuleList : in out T; + Columns : in ColumnIDs; + FullRows : in Positive; + ExtraRow : in Natural); + --# derives RuleList from *, + --# Columns, + --# ExtraRow, + --# FullRows; + + --------------------------------------------------------------------------- + -- Returns the current rule name for Column and advances the cursor + -- to the next rule. + --------------------------------------------------------------------------- + procedure GetNextRule (RuleList : in out T; + Column : in ColumnIDs; + Rule : out EStrings.T); + --# derives Rule from Column, + --# RuleList & + --# RuleList from *, + --# Column; + --------------------------------------------------------------------------- + +private + --# hide RuleListADT; + + package StringLists is new Ada.Containers.Doubly_Linked_Lists + (Element_Type => EStrings.T, + "=" => EStrings.Eq_String); + + type Cursors is array (ColumnIDs) of StringLists.Cursor; + + type T is + record + Rules : StringLists.List; + ColumnRules : Cursors; + end record; + +end RuleListADT; + diff --git a/pogs/total-rulesusedforfile.adb b/pogs/total-rulesusedforfile.adb new file mode 100644 index 0000000..e6962d9 --- /dev/null +++ b/pogs/total-rulesusedforfile.adb @@ -0,0 +1,269 @@ +-------------------------------------------------------------------------------- +-- (C) Phil Thornley +-------------------------------------------------------------------------------- +-- +-- This modification to the SPARK toolset is free software; you can redistribute +-- it and/or modify it under terms of the GNU General Public License as +-- published by the Free Software Foundation; either version 3, or (at your +-- option) any later version. This modification to the SPARK toolset is +-- distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; +-- without even the implied warranty of MERCHANTABILITY or FITNESS FOR A +-- PARTICULAR PURPOSE. See the GNU General Public License for more details. +-- You should have received a copy of the GNU General Public License distributed +-- with the SPARK toolset; see file COPYING3. If not, go to +-- http://www.gnu.org/licenses for a complete copy of the license. +-- +--============================================================================== + + +-------------------------------------------------------------------------------- +--Synopsis: -- +-- -- +--Procedure to print out the rules in the file RulesFile that have been -- +--stored for the rule file with name RuleFileName. -- +-- -- +-------------------------------------------------------------------------------- + +-------------------------------------------------------------------------------- +-- Implementation Note: +-- +-- The rule file name is stored in RulesFile (by VCS.AnalyseSimpLogFile) as an +-- ELString but the RuleFileName parameter passed in from Total is an EString. +-- In this procedure the name is read into an ELString then converted to an +-- EString for comparison with RuleFileName. +-------------------------------------------------------------------------------- + +with Ada.Numerics.Elementary_Functions; + +with RuleListADT; + +separate(Total) +procedure RulesUsedForFile (ReportFile : in SPARK_IO.File_Type; + RuleFileName : in EStrings.T; + RulesFile : in out SPARK_IO.File_Type) +is + + Indentation : constant := 8; + LineLength : constant := 80 - Indentation; + ColumnGap : constant := 3; + + -- Shortest possible rule name is 4 chars: a(1). + MinRule : constant := 4; + + -- MaxColumns is 10 with these values. + -- The specification of RuleListADT has a copy of MaxColumns which must be + -- updated for any change here. + MaxColumns : constant := (LineLength - MinRule) / (ColumnGap + MinRule) + 1; + + subtype ColumnRange is Positive range 1 .. MaxColumns; + + subtype LineCols is Integer range 1 .. 80; + subtype String80 is String(LineCols); + + BlankLine : constant String80 := String80'(others => ' '); + + subtype RuleLengths is Integer range MinRule .. EStrings.Positions'Last; + MaxRuleLength : RuleLengths; + + RuleList : RuleListADT.T; + RuleCount : Natural; + Columns : ColumnRange; + FullRows : Natural; + LastRow : Natural; + + ARuleFileName : ELStrings.T; + ShorterName : EStrings.T; + ARuleName : EStrings.T; + TempStatus : SPARK_IO.File_Status; + + --------------------------------------------------------------------------- + function IntSqRoot (X : Natural) return Natural + --# pre X >=1; + --# return R => (R >= 1 and R * R <= X); + is + --# hide IntSqRoot; + begin + return + Integer + (Float'Floor (Ada.Numerics.Elementary_Functions.Sqrt (Float (X)))); + end IntSqRoot; + + --------------------------------------------------------------------------- + procedure Layout (RuleCount : in Positive; + MaxRuleLength : in RuleLengths; + Columns : out ColumnRange; + FullRows : out Positive; + LastRow : out Natural) + --# derives Columns, + --# FullRows, + --# LastRow from MaxRuleLength, + --# RuleCount; + --# post LastRow <= ColumnRange'Last; + is + MinFullRows : Natural; + begin + if MaxRuleLength <= LineLength then + -- Up to 5 rules use a single column. + if RuleCount <= 5 then + Columns := 1; + FullRows := RuleCount; + LastRow := 0; + else + -- Layout for the maximum number of columns. + Columns := + (LineLength - MaxRuleLength) / (ColumnGap + MaxRuleLength) + 1; + --# assert RuleCount >= 6 + --# and Columns in 1 .. 10; + MinFullRows := RuleCount / Columns; + LastRow := RuleCount rem Columns; + -- Don't want more columns than rows. + if LastRow = 0 then + if MinFullRows < Columns then + --# check MinFullRows < 10; + --# check MinFullRows * Columns >= RuleCount - Columns + 1 ; + --# check MinFullRows * Columns + Columns - 1 <= 100; + --# check RuleCount <= 100; + Columns := IntSqRoot (RuleCount); + FullRows := RuleCount / Columns; + LastRow := RuleCount rem Columns; + else + FullRows := MinFullRows; + end if; + elsif MinFullRows < Columns - 1 then -- LastRow > 0 + --# check MinFullRows < 9; + --# check MinFullRows * Columns >= RuleCount - Columns + 1 ; + --# check MinFullRows * Columns + Columns - 1 <= 100; + --# check RuleCount <= 100; + Columns := IntSqRoot (RuleCount); + FullRows := RuleCount / Columns; + LastRow := RuleCount rem Columns; + elsif MinFullRows = 0 then + --# check RuleCount < Columns; + Columns := IntSqRoot (RuleCount); + FullRows := RuleCount / Columns; + LastRow := RuleCount rem Columns; + else + FullRows := MinFullRows; + end if; + end if; + else -- MaxRuleLength > LineLength + Columns := 1; + FullRows := RuleCount; + LastRow := 0; + end if; + end Layout; + + --------------------------------------------------------------------------- + procedure PrintOneLine (ReportFile : in SPARK_IO.File_Type; + RuleList : in out RuleListADT.T; + Columns : in ColumnRange) + --# global in out SPARK_IO.File_Sys; + --# in MaxRuleLength; + --# derives RuleList from *, + --# Columns & + --# SPARK_IO.File_Sys from *, + --# Columns, + --# MaxRuleLength, + --# ReportFile, + --# RuleList; + is + PrintRuleName : EStrings.T; + begin + SPARK_IO.Put_String (File => ReportFile, + Item => BlankLine, + Stop => Indentation); + for Col in ColumnRange range 1 .. Columns + --# assert Columns <= ColumnRange'Last + --# and Columns% = Columns; + loop + RuleListADT.GetNextRule (RuleList => RuleList, + Column => Col, + Rule => PrintRuleName); + EStrings.Put_String (File => ReportFile, + E_Str => PrintRuleName); + if Col < Columns and + -- Redundant check, makes run-time error proofs easy. + EStrings.Get_Length (PrintRuleName) - ColumnGap <= MaxRuleLength + then + SPARK_IO.Put_String + (File => ReportFile, + Item => BlankLine, + Stop => + (MaxRuleLength - EStrings.Get_Length(PrintRuleName)) + ColumnGap); + end if; + end loop; + SPARK_IO.New_Line (File => ReportFile, + Spacing => 1); + end PrintOneLine; + --------------------------------------------------------------------------- + +begin -- Code of RulesUsedForFile + + RuleListADT.Initialize (RuleList); + MaxRuleLength := MinRule; + + -- Add rules for this file; + --# accept F, 10, TempStatus, "Returned status is not used"; + SPARK_IO.Reset (RulesFile, SPARK_IO.In_File, TempStatus); + --# end accept; + if not SPARK_IO.End_Of_File (RulesFile) then + loop + ELStrings.Get_Line (File => RulesFile, + E_Str => ARuleFileName); + ShorterName := ELStrings.ToExaminerString (ARuleFileName); + loop + exit when SPARK_IO.End_Of_File (RulesFile); + EStrings.Get_Line (RulesFile, + ARuleName); + exit when EStrings.Eq_String (ARuleName, EStrings.Empty_String); + --# accept F, 41, "Stable test, to avoid two separate loops"; + if EStrings.Eq_String (ShorterName, RuleFileName) then + --# end accept; + -- Add to the list and keep track of the longest. + RuleListADT.AddRule (RuleList => RuleList, + Rule => ARuleName); + if EStrings.Get_Length (ARuleName) > MaxRuleLength then + MaxRuleLength := EStrings.Get_Length (ARuleName); + end if; + + end if; + end loop; + exit when SPARK_IO.End_Of_File (RulesFile); + end loop; + end if; + + RuleCount := RuleListADT.GetRuleCount (RuleList); + if RuleCount > 0 then + + Layout (RuleCount => RuleCount, + MaxRuleLength => MaxRuleLength, + Columns => Columns, + FullRows => FullRows, + LastRow => LastRow); + + RuleListADT.SetColumns (RuleList => RuleList, + Columns => Columns, + FullRows => FullRows, + ExtraRow => LastRow); + + for I in Positive range 1 .. FullRows + --# assert LastRow <= ColumnRange'Last; + loop + PrintOneLine (ReportFile, + RuleList, + Columns); + end loop; + if LastRow > 0 then + --# accept F, 10, RuleList, "Returned value is not needed."; + PrintOneLine (ReportFile, + RuleList, + LastRow); + --# end accept; + end if; + SPARK_IO.New_Line (File => ReportFile, + Spacing => 1); + + end if; + + --# accept F, 33, TempStatus, "Returned status is not used."; +end RulesUsedForFile; -- 1.7.0.2.msysgit.0