blob: c4483974984ba4636fc9adb1a2b5818650696bbe [file] [log] [blame]
------------------------------------------------------------------------------
-- C O D E P E E R / S P A R K --
-- --
-- Copyright (C) 2015-2022, AdaCore --
-- --
-- This is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. This software is distributed in the hope that it will be useful, --
-- but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHAN- --
-- TABILITY 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 this software; see file --
-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy --
-- of the license. --
-- --
------------------------------------------------------------------------------
pragma Ada_2012;
with Ada.Containers; use Ada.Containers;
with Ada.Strings.Unbounded; use Ada.Strings.Unbounded;
package SA_Messages is
-- This package can be used for reading/writing a file containing a
-- sequence of static anaysis results. Each element can describe a runtime
-- check whose outcome has been statically determined, or it might be a
-- warning or diagnostic message. It is expected that typically CodePeer
-- will do the writing and SPARK will do the reading; this will allow SPARK
-- to get the benefit of CodePeer's analysis.
--
-- Each item is represented as a pair consisting of a message and an
-- associated source location. Source locations may refer to a location
-- within the expansion of an instance of a generic; this is represented
-- by combining the corresponding location within the generic with the
-- location of the instance (repeated if the instance itself occurs within
-- a generic). In addition, the type Iteration_Id is intended for use in
-- distinguishing messages which refer to a specific iteration of a loop
-- (this case can arise, for example, if CodePeer chooses to unroll a
-- for-loop). This data structure is only general enough to support the
-- kinds of unrolling that are currently planned for CodePeer. For
-- example, an Iteration_Id can only identify an iteration of the nearest
-- enclosing loop of the associated File/Line/Column source location.
-- This is not a problem because CodePeer doesn't unroll loops which
-- contain other loops.
type Message_Kind is (
-- Check kinds
Array_Index_Check,
Divide_By_Zero_Check,
Tag_Check,
Discriminant_Check,
Range_Check,
Overflow_Check,
Assertion_Check,
-- Warning kinds
Suspicious_Range_Precondition_Warning,
Suspicious_First_Precondition_Warning,
Suspicious_Input_Warning,
Suspicious_Constant_Operation_Warning,
Unread_In_Out_Parameter_Warning,
Unassigned_In_Out_Parameter_Warning,
Non_Analyzed_Call_Warning,
Procedure_Does_Not_Return_Warning,
Check_Fails_On_Every_Call_Warning,
Unknown_Call_Warning,
Dead_Store_Warning,
Dead_Outparam_Store_Warning,
Potentially_Dead_Store_Warning,
Same_Value_Dead_Store_Warning,
Dead_Block_Warning,
Infinite_Loop_Warning,
Dead_Edge_Warning,
Plain_Dead_Edge_Warning,
True_Dead_Edge_Warning,
False_Dead_Edge_Warning,
True_Condition_Dead_Edge_Warning,
False_Condition_Dead_Edge_Warning,
Unrepeatable_While_Loop_Warning,
Dead_Block_Continuation_Warning,
Local_Lock_Of_Global_Object_Warning,
Analyzed_Module_Warning,
Non_Analyzed_Module_Warning,
Non_Analyzed_Procedure_Warning,
Incompletely_Analyzed_Procedure_Warning);
-- Assertion_Check includes checks for user-defined PPCs (both specific
-- and class-wide), Assert pragma checks, subtype predicate checks,
-- type invariant checks (specific and class-wide), and checks for
-- implementation-defined assertions such as Assert_And_Cut, Assume,
-- Contract_Cases, Default_Initial_Condition, Initial_Condition,
-- Loop_Invariant, Loop_Variant, Refined_Post, and Subprogram_Variant.
--
-- It might be nice to distinguish these different kinds of assertions
-- as is done in SPARK's VC_Kind enumeration type, but any distinction
-- which isn't already present in CP's BE_Message_Subkind enumeration type
-- would require more work on the CP side.
--
-- The warning kinds are pretty much a copy of the set of
-- Be_Message_Subkind values for which CP's Is_Warning predicate returns
-- True; see descriptive comment for each in CP's message_kinds.ads .
subtype Check_Kind is Message_Kind
range Array_Index_Check .. Assertion_Check;
subtype Warning_Kind is Message_Kind
range Message_Kind'Succ (Check_Kind'Last) .. Message_Kind'Last;
-- Possible outcomes of the static analysis of a runtime check
--
-- Not_Statically_Known_With_Low_Severity could be used instead of of
-- Not_Statically_Known if there is some reason to believe that (although
-- the tool couldn't prove it) the check is likely to always pass (in CP
-- terms, if the corresponding CP message has severity Low as opposed to
-- Medium). It's not clear yet whether SPARK will care about this
-- distinction.
type SA_Check_Result is
(Statically_Known_Success,
Not_Statically_Known_With_Low_Severity,
Not_Statically_Known,
Statically_Known_Failure);
type SA_Message (Kind : Message_Kind := Message_Kind'Last) is record
case Kind is
when Check_Kind =>
Check_Result : SA_Check_Result;
when Warning_Kind =>
null;
end case;
end record;
type Source_Location_Or_Null (<>) is private;
Null_Location : constant Source_Location_Or_Null;
subtype Source_Location is Source_Location_Or_Null with
Dynamic_Predicate => Source_Location /= Null_Location;
type Line_Number is new Positive;
type Column_Number is new Positive;
function File_Name (Location : Source_Location) return String;
function File_Name (Location : Source_Location) return Unbounded_String;
function Line (Location : Source_Location) return Line_Number;
function Column (Location : Source_Location) return Column_Number;
type Iteration_Kind is (None, Initial, Subsequent, Numbered);
-- None is for the usual no-unrolling case.
-- Initial and Subsequent are for use in the case where only the first
-- iteration of a loop (or some part thereof, such as the termination
-- test of a while-loop) is unrolled.
-- Numbered is for use in the case where a for-loop with a statically
-- known number of iterations is fully unrolled.
subtype Iteration_Number is Integer range 1 .. 255;
subtype Iteration_Total is Integer range 2 .. 255;
type Iteration_Id (Kind : Iteration_Kind := None) is record
case Kind is
when Numbered =>
Number : Iteration_Number;
Of_Total : Iteration_Total;
when others =>
null;
end case;
end record;
function Iteration (Location : Source_Location) return Iteration_Id;
function Enclosing_Instance
(Location : Source_Location) return Source_Location_Or_Null;
-- For a source location occurring within the expansion of an instance of a
-- generic unit, the Line, Column, and File_Name selectors will indicate a
-- location within the generic; the Enclosing_Instance selector yields the
-- location of the declaration of the instance.
function Make
(File_Name : String;
Line : Line_Number;
Column : Column_Number;
Iteration : Iteration_Id;
Enclosing_Instance : Source_Location_Or_Null) return Source_Location;
-- Constructor
type Message_And_Location (<>) is private;
function Location (Item : Message_And_Location) return Source_Location;
function Message (Item : Message_And_Location) return SA_Message;
function Make_Msg_Loc
(Msg : SA_Message;
Loc : Source_Location) return Message_And_Location;
-- Selectors
function "<" (Left, Right : Message_And_Location) return Boolean;
function Hash (Key : Message_And_Location) return Hash_Type;
-- Actuals for container instances
File_Extension : constant String; -- ".json" (but could change in future)
-- Clients may wish to use File_Extension in constructing
-- File_Name parameters for calls to Open.
package Writing is
function Is_Open return Boolean;
procedure Open (File_Name : String) with
Precondition => not Is_Open,
Postcondition => Is_Open;
-- Behaves like Text_IO.Create with respect to error cases
procedure Write (Message : SA_Message; Location : Source_Location);
procedure Close with
Precondition => Is_Open,
Postcondition => not Is_Open;
-- Behaves like Text_IO.Close with respect to error cases
end Writing;
package Reading is
function Is_Open return Boolean;
procedure Open (File_Name : String; Full_Path : Boolean := True) with
Precondition => not Is_Open,
Postcondition => Is_Open;
-- Behaves like Text_IO.Open with respect to error cases
function Done return Boolean with
Precondition => Is_Open;
function Get return Message_And_Location with
Precondition => not Done;
procedure Close with
Precondition => Is_Open,
Postcondition => not Is_Open;
-- Behaves like Text_IO.Close with respect to error cases
end Reading;
private
type Simple_Source_Location is record
File_Name : Unbounded_String := Null_Unbounded_String;
Line : Line_Number := Line_Number'Last;
Column : Column_Number := Column_Number'Last;
Iteration : Iteration_Id := (Kind => None);
end record;
type Source_Locations is
array (Natural range <>) of Simple_Source_Location;
type Source_Location_Or_Null (Count : Natural) is record
Locations : Source_Locations (1 .. Count);
end record;
Null_Location : constant Source_Location_Or_Null :=
(Count => 0, Locations => (others => <>));
type Message_And_Location (Count : Positive) is record
Message : SA_Message;
Location : Source_Location (Count => Count);
end record;
File_Extension : constant String := ".json";
end SA_Messages;