Adacovex.Parsers.GNATprove

Parse a gnatprove.out file, extracting VC counts per check type. Reads the GNATprove summary table and populates the Proof_Summary record with proved/unproved VC counts per category. @param File_Path Path to gnatprove.out. @param Summary Output proof summary record. @param Success True if file was parsed successfully.

Note: All items in this package are public.

Functions

function Determine_SPARK_Level (Summary : Adacovex.Types.Proof_Summary) return Adacovex.Types.SPARK_Level [Post] [Global] [SPARK]

Parameter	Description
Summary	Proof summary with VC counts per category.

Returns: Derived SPARK_Level (Stone through Platinum).

function Find_Prove_Output (Target_Dir : Standard.String) return Standard.String [Pre]

Parameter	Description
Target_Dir	Root directory to inspect.

Returns: Path to a discovered gnatprove.out, or “”.

Procedures

procedure Parse_Prove_From_Project (Target_Dir : Standard.String; Summary : Adacovex.Types.Proof_Summary; Success : Standard.Boolean) [Pre]

Parameter	Description
Success	True if gnatprove.out was found and parsed.
Summary	Output proof summary record.
Target_Dir	Project root directory.

procedure Parse_Prove_JSON (File_Path : Standard.String; Summary : Adacovex.Types.Proof_Summary; Success : Standard.Boolean) [Pre]

Parameter	Description
File_Path	Path to GNATprove JSON results file.
Success	True if JSON was parsed successfully.
Summary	Output proof summary record.

procedure Parse_Prove_Out (File_Path : Standard.String; Summary : Adacovex.Types.Proof_Summary; Success : Standard.Boolean) [Pre]

Parameter	Description
File_Path	Path to gnatprove.out.
Success	True if file was parsed successfully.
Summary	Output proof summary record.