GNATprove2XLS

gnatprove2xls.py is a Python 3 script which converts report files produced by GNATprove to spreadsheet files compatible with MS Excel 97/2000/XP/2003 XLS files.

Rationale

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

The goal of gnatprove2xls.py is to extract this information and present it in a spreadsheet format to facilitate human analysis on GNATprove's results such as: sorting, filtering, and summarizing using the spreadsheet program's features. For example, to sort the results to find out which subprograms have the least percentage of proved checks.

Usage

gnatprove2xls.py depends on the xlwt module. You can install it using this command:

pip3 install xlwt

The follow command reads the GNATprove report file gnatprove.out and generates a spreadsheet called gnatprove.xls:

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

Output format

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

Summary Worksheet

The //Summary// worksheet contains a summary of the flow analysis and proof performed on each compilation unit. It shows the total number of flow errors/warnings, and number of checks performed for all subprograms and packages 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 by GNATprove.
• "Flow Errors" - The total number of flow errors from all subprograms and packages in the unit.
• "Flow Warnings" - The total number of flow warnings from all subprograms and packages in the unit.
• "Checks" - The total number of checks that were performed by GNATprove from all subprograms 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 and packages in the unit.

Details Worksheet

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

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 the subprogram or package. If no proof was performed then this cell is empty.
• "Proved Checks" - The total number of checks that were successfully proved by GNATprove 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 total number of checks.

Suppressed Messages Worksheet

The //Suppressed Messages// worksheet contains a list of all suppressed messages from GNATprove's report file. This is a list of all manual suppressions and justifications from the use of pragma Annotate or pragma Warnings in 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.