From: Arnaud Charlet Date: Thu, 20 Nov 2014 11:28:12 +0000 (+0100) Subject: [multiple changes] X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=697b781a68a969edaf76da0275c2decb8626a891;p=gcc.git [multiple changes] 2014-11-20 Robert Dewar * a-stream.ads, a-reatim.ads, a-calend.ads, sinfo.ads, s-crtl.ads, interfac.ads, s-taskin.ads: Minor reformatting. 2014-11-20 Hristian Kirtchev * sem_prag.adb (Analyze_Pragma): Extensions_Visible can now apply to an expression function. * sem_util.adb (Extensions_Visible_Status): Add special processing for expression functions. 2014-11-20 Hristian Kirtchev * inline.adb (Build_Body_To_Inline): Remove meaningless aspects and pragmas. (Generate_Subprogram_Body): Remove meaningless aspects and pragmas. (Remove_Aspects_And_Pragmas): New routine. (Remove_Pragmas): Removed. * namet.ads, namet.adb (Nam_In): New versions of the routine. From-SVN: r217841 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index b88ce84ee58..e43c701f2eb 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,24 @@ +2014-11-20 Robert Dewar + + * a-stream.ads, a-reatim.ads, a-calend.ads, sinfo.ads, s-crtl.ads, + interfac.ads, s-taskin.ads: Minor reformatting. + +2014-11-20 Hristian Kirtchev + + * sem_prag.adb (Analyze_Pragma): Extensions_Visible can now + apply to an expression function. + * sem_util.adb (Extensions_Visible_Status): Add special processing + for expression functions. + +2014-11-20 Hristian Kirtchev + + * inline.adb (Build_Body_To_Inline): Remove meaningless aspects + and pragmas. + (Generate_Subprogram_Body): Remove meaningless aspects and pragmas. + (Remove_Aspects_And_Pragmas): New routine. + (Remove_Pragmas): Removed. + * namet.ads, namet.adb (Nam_In): New versions of the routine. + 2014-11-20 Thomas Quinot * sem_util.adb: Minor reformatting. diff --git a/gcc/ada/a-calend.ads b/gcc/ada/a-calend.ads index 8e268b9c2b5..55efe115f5d 100644 --- a/gcc/ada/a-calend.ads +++ b/gcc/ada/a-calend.ads @@ -200,11 +200,15 @@ private type Time_Rep is new Long_Long_Integer; type Time is new Time_Rep; -- The underlying type of Time has been chosen to be a 64 bit signed - -- integer number since it allows for easier processing of sub seconds + -- integer number since it allows for easier processing of sub-seconds -- and arithmetic. We use Long_Long_Integer to allow this unit to compile -- when using custom target configuration files where the max integer is - -- 32bits. This is useful for static analysis tools such as SPARK or + -- 32 bits. This is useful for static analysis tools such as SPARK or -- CodePeer. + -- + -- Note: the reason we have two separate types here is to avoid problems + -- with overloading ambiguities in the body if we tried to use Time as an + -- internal computational type. Days_In_Month : constant array (Month_Number) of Day_Number := (31, 28, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31); diff --git a/gcc/ada/a-reatim.ads b/gcc/ada/a-reatim.ads index b020adcd077..8558d460a58 100644 --- a/gcc/ada/a-reatim.ads +++ b/gcc/ada/a-reatim.ads @@ -90,12 +90,14 @@ package Ada.Real_Time is function Minutes (M : Integer) return Time_Span; pragma Ada_05 (Minutes); - -- Seconds_Count needs 64 bits, since Time has the full range of Duration. - -- The delta of Duration is 10 ** (-9), so the maximum number of seconds is - -- 2**63/10**9 = 8*10**9 which does not quite fit in 32 bits. - - type Seconds_Count is range - Long_Long_Integer'First .. Long_Long_Integer'Last; + type Seconds_Count is new Long_Long_Integer; + -- Seconds_Count needs 64 bits, since Time has the full range of + -- Duration. The delta of Duration is 10 ** (-9), so the maximum number of + -- seconds is 2**63/10**9 = 8*10**9 which does not quite fit in 32 bits. + -- However, rather than make this explicitly 64-bits we derive from + -- Long_Long_Integer. In normal usage this will have the same effect. + -- But in the case of CodePeer with a target configuration file with a + -- maximum integer size of 32, it allows analysis of this unit. procedure Split (T : Time; SC : out Seconds_Count; TS : out Time_Span); function Time_Of (SC : Seconds_Count; TS : Time_Span) return Time; diff --git a/gcc/ada/a-stream.ads b/gcc/ada/a-stream.ads index 0977f285f6f..40e60ce2499 100644 --- a/gcc/ada/a-stream.ads +++ b/gcc/ada/a-stream.ads @@ -41,8 +41,12 @@ package Ada.Streams is type Stream_Element is mod 2 ** Standard'Storage_Unit; - type Stream_Element_Offset is range - Long_Long_Integer'First .. Long_Long_Integer'Last; + type Stream_Element_Offset is new Long_Long_Integer; + -- Stream_Element_Offset needs 64 bits to accomodate large stream files. + -- However, rather than make this explicitly 64-bits we derive from + -- Long_Long_Integer. In normal usage this will have the same effect. + -- But in the case of CodePeer with a target configuration file with a + -- maximum integer size of 32, it allows analysis of this unit. subtype Stream_Element_Count is Stream_Element_Offset range 0 .. Stream_Element_Offset'Last; diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index c900cd394f3..9e97e8305fe 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -23,6 +23,7 @@ -- -- ------------------------------------------------------------------------------ +with Aspects; use Aspects; with Atree; use Atree; with Debug; use Debug; with Einfo; use Einfo; @@ -212,11 +213,21 @@ package body Inline is -- function anyway. This is also the case if the function is defined in a -- task body or within an entry (for example, an initialization procedure). - procedure Remove_Pragmas (Bod : Node_Id); - -- A pragma Unreferenced or pragma Unmodified that mentions a formal - -- parameter has no meaning when the body is inlined and the formals - -- are rewritten. Remove it from body to inline. The analysis of the - -- non-inlined body will handle the pragma properly. + procedure Remove_Aspects_And_Pragmas (Body_Decl : Node_Id); + -- Remove all aspects and/or pragmas that have no meaning in inlined body + -- Body_Decl. The analysis of these items is performed on the non-inlined + -- body. The items currently removed are: + -- Contract_Cases + -- Global + -- Depends + -- Postcondition + -- Precondition + -- Refined_Global + -- Refined_Depends + -- Refined_Post + -- Test_Case + -- Unmodified + -- Unreferenced ------------------------------ -- Deferred Cleanup Actions -- @@ -1103,12 +1114,12 @@ package body Inline is Set_Parameter_Specifications (Specification (Original_Body), No_List); Set_Defining_Unit_Name (Specification (Original_Body), - Make_Defining_Identifier (Sloc (N), Name_uParent)); + Make_Defining_Identifier (Sloc (N), Name_uParent)); Set_Corresponding_Spec (Original_Body, Empty); - -- Remove those pragmas that have no meaining in an inlined body. + -- Remove all aspects/pragmas that have no meaining in an inlined body - Remove_Pragmas (Original_Body); + Remove_Aspects_And_Pragmas (Original_Body); Body_To_Analyze := Copy_Generic_Node (Original_Body, Empty, False); @@ -1116,8 +1127,9 @@ package body Inline is -- to be resolved. if Ekind (Spec_Id) = E_Function then - Set_Result_Definition (Specification (Body_To_Analyze), - New_Occurrence_Of (Etype (Spec_Id), Sloc (N))); + Set_Result_Definition + (Specification (Body_To_Analyze), + New_Occurrence_Of (Etype (Spec_Id), Sloc (N))); end if; if No (Declarations (N)) then @@ -1126,9 +1138,9 @@ package body Inline is Append (Body_To_Analyze, Declarations (N)); end if; - -- The body to inline is pre-analyzed. In GNATprove mode we must - -- disable full analysis as well so that light expansion does not - -- take place either, and name resolution is unaffected. + -- The body to inline is pre-analyzed. In GNATprove mode we must disable + -- full analysis as well so that light expansion does not take place + -- either, and name resolution is unaffected. Expander_Mode_Save_And_Set (False); Full_Analysis := False; @@ -1643,12 +1655,10 @@ package body Inline is Body_To_Inline := Copy_Separate_Tree (N); end if; - -- A pragma Unreferenced or pragma Unmodified that mentions a formal - -- parameter has no meaning when the body is inlined and the formals - -- are rewritten. Remove it from body to inline. The analysis of the - -- non-inlined body will handle the pragma properly. + -- Remove all aspects/pragmas that have no meaining in an inlined + -- body. - Remove_Pragmas (Body_To_Inline); + Remove_Aspects_And_Pragmas (Body_To_Inline); -- We need to capture references to the formals in order -- to substitute the actuals at the point of inlining, i.e. @@ -3947,31 +3957,63 @@ package body Inline is end loop; end Remove_Dead_Instance; - -------------------- - -- Remove_Pragmas -- - -------------------- + -------------------------------- + -- Remove_Aspects_And_Pragmas -- + -------------------------------- - procedure Remove_Pragmas (Bod : Node_Id) is - Decl : Node_Id; - Nxt : Node_Id; + procedure Remove_Aspects_And_Pragmas (Body_Decl : Node_Id) is + procedure Remove_Items (List : List_Id); + -- Remove all useless aspects/pragmas from a particular list - begin - Decl := First (Declarations (Bod)); - while Present (Decl) loop - Nxt := Next (Decl); + ------------------ + -- Remove_Items -- + ------------------ - if Nkind (Decl) = N_Pragma - and then Nam_In (Pragma_Name (Decl), Name_Contract_Cases, - Name_Precondition, + procedure Remove_Items (List : List_Id) is + Item : Node_Id; + Item_Id : Node_Id; + Next_Item : Node_Id; + + begin + -- Traverse the list looking for an aspect specification or a pragma + + Item := First (List); + while Present (Item) loop + Next_Item := Next (Item); + + if Nkind (Item) = N_Aspect_Specification then + Item_Id := Identifier (Item); + elsif Nkind (Item) = N_Pragma then + Item_Id := Pragma_Identifier (Item); + else + Item_Id := Empty; + end if; + + if Present (Item_Id) + and then Nam_In (Chars (Item_Id), Name_Contract_Cases, + Name_Global, + Name_Depends, Name_Postcondition, - Name_Unreferenced, - Name_Unmodified) - then - Remove (Decl); - end if; + Name_Precondition, + Name_Refined_Global, + Name_Refined_Depends, + Name_Refined_Post, + Name_Test_Case, + Name_Unmodified, + Name_Unreferenced) + then + Remove (Item); + end if; - Decl := Nxt; - end loop; - end Remove_Pragmas; + Item := Next_Item; + end loop; + end Remove_Items; + + -- Start of processing for Remove_Aspects_And_Pragmas + + begin + Remove_Items (Aspect_Specifications (Body_Decl)); + Remove_Items (Declarations (Body_Decl)); + end Remove_Aspects_And_Pragmas; end Inline; diff --git a/gcc/ada/interfac.ads b/gcc/ada/interfac.ads index 85ed9e956b7..6e3afffe5ee 100644 --- a/gcc/ada/interfac.ads +++ b/gcc/ada/interfac.ads @@ -51,12 +51,13 @@ package Interfaces is type Integer_32 is range -2 ** 31 .. 2 ** 31 - 1; for Integer_32'Size use 32; - type Integer_64 is range Long_Long_Integer'First .. Long_Long_Integer'Last; + type Integer_64 is new Long_Long_Integer; for Integer_64'Size use 64; -- Note: we use Long_Long_Integer'First instead of -2 ** 63 to allow this - -- unit to compile when using custom target configuration files where - -- the max integer is 32bits. This is useful for static analysis tools - -- such as SPARK or CodePeer. + -- unit to compile when using custom target configuration files where the + -- maximum integer is 32 bits. This is useful for static analysis tools + -- such as SPARK or CodePeer. In the normal case Long_Long_Integer is + -- always 64-bits so we get the desired 64-bit type. type Unsigned_8 is mod 2 ** 8; for Unsigned_8'Size use 8; diff --git a/gcc/ada/namet.adb b/gcc/ada/namet.adb index 1cebb464b8e..1a946402845 100644 --- a/gcc/ada/namet.adb +++ b/gcc/ada/namet.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2013, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- -- -- -- GNAT 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- -- @@ -1133,6 +1133,106 @@ package body Namet is T = V7; end Nam_In; + function Nam_In + (T : Name_Id; + V1 : Name_Id; + V2 : Name_Id; + V3 : Name_Id; + V4 : Name_Id; + V5 : Name_Id; + V6 : Name_Id; + V7 : Name_Id; + V8 : Name_Id) return Boolean + is + begin + return T = V1 or else + T = V2 or else + T = V3 or else + T = V4 or else + T = V5 or else + T = V6 or else + T = V7 or else + T = V8; + end Nam_In; + + function Nam_In + (T : Name_Id; + V1 : Name_Id; + V2 : Name_Id; + V3 : Name_Id; + V4 : Name_Id; + V5 : Name_Id; + V6 : Name_Id; + V7 : Name_Id; + V8 : Name_Id; + V9 : Name_Id) return Boolean + is + begin + return T = V1 or else + T = V2 or else + T = V3 or else + T = V4 or else + T = V5 or else + T = V6 or else + T = V7 or else + T = V8 or else + T = V9; + end Nam_In; + + function Nam_In + (T : Name_Id; + V1 : Name_Id; + V2 : Name_Id; + V3 : Name_Id; + V4 : Name_Id; + V5 : Name_Id; + V6 : Name_Id; + V7 : Name_Id; + V8 : Name_Id; + V9 : Name_Id; + V10 : Name_Id) return Boolean + is + begin + return T = V1 or else + T = V2 or else + T = V3 or else + T = V4 or else + T = V5 or else + T = V6 or else + T = V7 or else + T = V8 or else + T = V9 or else + T = V10; + end Nam_In; + + function Nam_In + (T : Name_Id; + V1 : Name_Id; + V2 : Name_Id; + V3 : Name_Id; + V4 : Name_Id; + V5 : Name_Id; + V6 : Name_Id; + V7 : Name_Id; + V8 : Name_Id; + V9 : Name_Id; + V10 : Name_Id; + V11 : Name_Id) return Boolean + is + begin + return T = V1 or else + T = V2 or else + T = V3 or else + T = V4 or else + T = V5 or else + T = V6 or else + T = V7 or else + T = V8 or else + T = V9 or else + T = V10 or else + T = V11; + end Nam_In; + ------------------ -- Reinitialize -- ------------------ diff --git a/gcc/ada/namet.ads b/gcc/ada/namet.ads index 431204b6a77..a7d7a481636 100644 --- a/gcc/ada/namet.ads +++ b/gcc/ada/namet.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2013, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- -- -- -- GNAT 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- -- @@ -227,6 +227,56 @@ package Namet is V6 : Name_Id; V7 : Name_Id) return Boolean; + function Nam_In + (T : Name_Id; + V1 : Name_Id; + V2 : Name_Id; + V3 : Name_Id; + V4 : Name_Id; + V5 : Name_Id; + V6 : Name_Id; + V7 : Name_Id; + V8 : Name_Id) return Boolean; + + function Nam_In + (T : Name_Id; + V1 : Name_Id; + V2 : Name_Id; + V3 : Name_Id; + V4 : Name_Id; + V5 : Name_Id; + V6 : Name_Id; + V7 : Name_Id; + V8 : Name_Id; + V9 : Name_Id) return Boolean; + + function Nam_In + (T : Name_Id; + V1 : Name_Id; + V2 : Name_Id; + V3 : Name_Id; + V4 : Name_Id; + V5 : Name_Id; + V6 : Name_Id; + V7 : Name_Id; + V8 : Name_Id; + V9 : Name_Id; + V10 : Name_Id) return Boolean; + + function Nam_In + (T : Name_Id; + V1 : Name_Id; + V2 : Name_Id; + V3 : Name_Id; + V4 : Name_Id; + V5 : Name_Id; + V6 : Name_Id; + V7 : Name_Id; + V8 : Name_Id; + V9 : Name_Id; + V10 : Name_Id; + V11 : Name_Id) return Boolean; + pragma Inline (Nam_In); -- Inline all above functions diff --git a/gcc/ada/s-crtl.ads b/gcc/ada/s-crtl.ads index 959fa4a2eb3..217b5b6e593 100644 --- a/gcc/ada/s-crtl.ads +++ b/gcc/ada/s-crtl.ads @@ -62,11 +62,12 @@ package System.CRTL is type ssize_t is range -(2 ** (Standard'Address_Size - 1)) .. +(2 ** (Standard'Address_Size - 1)) - 1; - type int64 is range Long_Long_Integer'First .. Long_Long_Integer'Last; + type int64 is new Long_Long_Integer; -- Note: we use Long_Long_Integer'First instead of -2 ** 63 to allow this - -- unit to compile when using custom target configuration files where - -- the max integer is 32bits. This is useful for static analysis tools - -- such as SPARK or CodePeer. + -- unit to compile when using custom target configuration files where the + -- maximum integer is 32 bits. This is useful for static analysis tools + -- such as SPARK or CodePeer. In the normal case, Long_Long_Integer is + -- always 64-bits so there is no difference. type Filename_Encoding is (UTF8, ASCII_8bits, Unspecified); for Filename_Encoding use (UTF8 => 0, ASCII_8bits => 1, Unspecified => 2); diff --git a/gcc/ada/s-taskin.ads b/gcc/ada/s-taskin.ads index bf198ca3e80..ffb96c34640 100644 --- a/gcc/ada/s-taskin.ads +++ b/gcc/ada/s-taskin.ads @@ -947,7 +947,12 @@ package System.Tasking is -- by Ada.Task_Attributes. type Task_Serial_Number is mod 2 ** Long_Long_Integer'Size; - -- Used to give each task a unique serial number + -- Used to give each task a unique serial number. We want 64-bits for this + -- type to get as much uniqueness as possible (2**64 is operationally + -- infinite in this context, but 2**32 perhaps could recycle). We use + -- Long_Long_Integer (which in the normal case is always 64-bits) rather + -- than 64-bits explicitly to allow codepeer to analyze this unit when + -- a target configuration file forces the maximum integer size to 32. type Ada_Task_Control_Block (Entry_Num : Task_Entry_Index) is record Common : Common_ATCB; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index c26e4f2ebff..52853199a29 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -13920,11 +13920,12 @@ package body Sem_Prag is -- pragma Extensions_Visible [ (boolean_EXPRESSION) ]; when Pragma_Extensions_Visible => Extensions_Visible : declare - Context : constant Node_Id := Parent (N); - Expr : Node_Id; - Formal : Entity_Id; - Subp : Entity_Id; - Stmt : Node_Id; + Context : constant Node_Id := Parent (N); + Expr : Node_Id; + Formal : Entity_Id; + Orig_Stmt : Node_Id; + Subp : Entity_Id; + Stmt : Node_Id; Has_OK_Formal : Boolean := False; @@ -13949,7 +13950,18 @@ package body Sem_Prag is -- Skip internally generated code elsif not Comes_From_Source (Stmt) then - null; + Orig_Stmt := Original_Node (Stmt); + + -- When pragma Ghost applies to an expression function, the + -- expression function is transformed into a subprogram. + + if Nkind (Stmt) = N_Subprogram_Declaration + and then Comes_From_Source (Orig_Stmt) + and then Nkind (Orig_Stmt) = N_Expression_Function + then + Subp := Defining_Entity (Stmt); + exit; + end if; -- The associated [generic] subprogram declaration has been -- found, stop the search. diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 981d2193062..ba2135daa70 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -5923,7 +5923,8 @@ package body Sem_Util is function Extensions_Visible_Status (Id : Entity_Id) return Extensions_Visible_Mode is - Arg1 : Node_Id; + Arg : Node_Id; + Decl : Node_Id; Expr : Node_Id; Prag : Node_Id; Subp : Entity_Id; @@ -5946,15 +5947,51 @@ package body Sem_Util is Prag := Get_Pragma (Subp, Pragma_Extensions_Visible); + -- In certain cases analysis may request the Extensions_Visible status + -- of an expression function before the pragma has been analyzed yet. + -- Inspect the declarative items after the expression function looking + -- for the pragma (if any). + + if No (Prag) and then Is_Expression_Function (Subp) then + Decl := Next (Unit_Declaration_Node (Subp)); + while Present (Decl) loop + if Nkind (Decl) = N_Pragma + and then Pragma_Name (Decl) = Name_Extensions_Visible + then + Prag := Decl; + exit; + + -- A source construct ends the region where Extensions_Visible may + -- appear, stop the traversal. An expanded expression function is + -- no longer a source construct, but it must still be recognized. + + elsif Comes_From_Source (Decl) + or else (Nkind_In (Decl, N_Subprogram_Body, + N_Subprogram_Declaration) + and then Is_Expression_Function + (Defining_Entity (Decl))) + then + exit; + end if; + + Next (Decl); + end loop; + end if; + -- Extract the value from the Boolean expression (if any) if Present (Prag) then - Arg1 := First (Pragma_Argument_Associations (Prag)); + Arg := First (Pragma_Argument_Associations (Prag)); + + if Present (Arg) then + Expr := Get_Pragma_Arg (Arg); - -- The pragma appears with an argument + -- When the associated subprogram is an expression function, the + -- argument of the pragma may not have been analyzed. - if Present (Arg1) then - Expr := Get_Pragma_Arg (Arg1); + if not Analyzed (Expr) then + Preanalyze_And_Resolve (Expr, Standard_Boolean); + end if; -- Guard against cascading errors when the argument of pragma -- Extensions_Visible is not a valid static Boolean expression. @@ -5969,19 +6006,20 @@ package body Sem_Util is return Extensions_Visible_False; end if; - -- Otherwise the pragma defaults to True + -- Otherwise the aspect or pragma defaults to True else return Extensions_Visible_True; end if; - -- Otherwise pragma Extensions_Visible is not inherited or directly - -- specified. In SPARK code, its value defaults to "False". + -- Otherwise aspect or pragma Extensions_Visible is not inherited or + -- directly specified. In SPARK code, its value defaults to "False". elsif SPARK_Mode = On then return Extensions_Visible_False; - -- In non-SPARK code, pragma Extensions_Visible defaults to "True" + -- In non-SPARK code, aspect or pragma Extensions_Visible defaults to + -- "True". else return Extensions_Visible_True; diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index f9c7052c4d3..ae7813593a1 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -562,7 +562,7 @@ package Sinfo is -- not make sense from a user point-of-view, and that cross-references that -- do not lead to data dependences for subprograms can be safely ignored. - -- GNATprove relies on the following frontend behaviors: + -- GNATprove relies on the following front end behaviors: -- 1. The first declarations in the list of visible declarations of -- a package declaration for a generic instance, up to the first @@ -579,13 +579,17 @@ package Sinfo is -- 4. Unconstrained types are not replaced by constrained types whose -- bounds are generated from an expression: Expand_Subtype_From_Expr - -- should be noop. + -- should be a no-op. - -- 5. Errors (instead of warnings) are issued on compile-time known - -- constraint errors, except in a few selected cases where it should - -- be allowed to let analysis proceed (e.g. range checks on empty - -- ranges, typically in deactivated code based on a given - -- configuration). + -- 5. Errors (instead of warnings) are issued on compile-time-known + -- constraint errors even though such cases do not correspond to + -- illegalities in the Ada RM (this is simply another case where + -- GNATprove implements a subset of the full language). + -- + -- However, there are a few exceptions to this rule for cases where + -- we want to allow the GNATprove analysis to proceed (e.g. range + -- checks on empty ranges, which typically appear in deactivated + -- code in a particular configuration). ----------------------- -- Check Flag Fields --