Repository files navigation

gnatprove2xls.py is a Python 3 script which converts report files produced byGNATprove to spreadsheet files compatible with MS Excel97/2000/XP/2003 XLS files.

The report files generated by GNATprove contains a detailed list of the flowanalysis and proof performed on each subprogram and package during its analysis.This information is presented as a textual list, which is not particularlyeasy to analyze.

The goal ofgnatprove2xls.py is to extract this information and presentit in a spreadsheet format to facilitate human analysis on GNATprove's resultssuch as: sorting, filtering, and summarizing using the spreadsheet program'sfeatures. For example, to sort the results to find out which subprograms have theleast percentage of proved checks.

gnatprove2xls.py depends on thexlwt module. You can install it usingthis command:

pip3 install xlwt

The follow command reads the GNATprove report filegnatprove.out and generatesa spreadsheet calledgnatprove.xls:

python3 gnatprove2xls.py --out=gnatprove.xls gnatprove.out

gnatprove2xls.py organizes the information into three worksheets in theoutput spreadsheet. The following subsections describe the format of theseworksheets.

The //Summary// worksheet contains a summary of the flow analysis and proofperformed on each compilation unit. It shows the total number of flowerrors/warnings, and number of checks performed for all subprograms andpackages within the unit.

The Summary worksheet defines the following columns:

• "Unit Name" - The name of the compilation unit (the unit's file name).
• "Analyzed" - The number of subprograms and packages analyzed in the unit.E.g. "8/10" means that 8 subprograms and packages out of 10 were analyzed byGNATprove.
• "Flow Errors" - The total number of flow errors from all subprograms andpackages in the unit.
• "Flow Warnings" - The total number of flow warnings from all subprograms andpackages in the unit.
• "Checks" - The total number of checks that were performed by GNATprove from allsubprograms and packages in the unit.
• "Checks Proved" - The number of checks that were successfully proved.
• "% Proved" - Shows the number of checks successfully proved as a percentage.
• "Suppressions" - The number of suppressed messages from all subprograms andpackages in the unit.

The //Details// worksheet contains a detailed list of all subprograms andpackages read by GNATprove. For each item, it shows the type of analysisperformed (e.g. flow only, or flow analysis and proof) and the number oferrors, warnings, and checks performed.This informaton can be filtered and sorted using the spreadsheet program'sfeatures.

The Details worksheet defines the following columns:

• "Name" - The name of the subprogram or package.
• "File" - The name of the file in which the subprogram or package is declared.
• "Line" - The line number at which the subprogram or package is declared.
• "Analysis" - The type of analysis that was performed by GNATprove.This can be one of: "not analyzed", "flow only", "flow + proof", or "proof only".
• "Flow Errors" - The total number of errors that occurred during flow analysis.If no flow analysis was performed then this cell is empty.
• "Flow Warnings" - The total number of warnings that occurred during flow analysis.If no flow analysis was performed then this cell is empty.
• "Checks" - The total number of checks performed by GNATprove when proving thesubprogram or package.If no proof was performed then this cell is empty.
• "Proved Checks" - The total number of checks that were successfully proved byGNATprove when proving the subprogram or package.If no proof was performed then this cell is empty.
• "% Proved" - Shows the number of proved checks as a percentage of the totalnumber of checks.

The //Suppressed Messages// worksheet contains a list of all suppressedmessages from GNATprove's report file. This is a list of all manual suppressionsand justifications from the use ofpragma Annotate orpragma Warningsin the source code.

The Suppressed Messages worksheet defines the following columns:

• "Name" - The name of the subprogram or package which contains the suppression.
• "File" - The name of the file which contains the suppression.
• "Line" - The line number of the suppression in the source file.
• "Column" - The column number of the suppression in the source file.
• "Reason" - The reason given for the suppression.