From 39f0fa29d043e4b05c2eb43b2b811303e60dba4f Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Thu, 20 Nov 2014 12:24:51 +0100 Subject: [PATCH] [multiple changes] 2014-11-20 Thomas Quinot * sem_util.adb: Minor reformatting. 2014-11-20 Robert Dewar * sem_prag.adb (Analyze_Pragma, case Linker_Section): Detect duplicate Linker_Section. 2014-11-20 Ed Schonberg * exp_ch4.adb: Add guard for build-in-place boolean op. 2014-11-20 Yannick Moy * checks.adb (Apply_Scalar_Range_Check): In GNATprove mode, put a range check when an empty range is used, instead of an error message. * sinfo.ads Update comment on GNATprove mode. 2014-11-20 Arnaud Charlet * a-stream.ads, s-osinte-linux.ads, a-reatim.ads, a-calend.ads, s-crtl.ads, interfac.ads, s-taskin.ads: Replace uses of 2 ** 63 and 2 ** 64 by references to Long_Long_Integer instead, to allow these units to be analyzed by codepeer or spark when using a target configuration file with long_long_size set to 32. From-SVN: r217840 --- gcc/ada/ChangeLog | 28 ++++++++++++++++++++++++++++ gcc/ada/a-calend.ads | 9 ++++++--- gcc/ada/a-reatim.ads | 3 ++- gcc/ada/a-stream.ads | 3 ++- gcc/ada/checks.adb | 16 +++++++++++++++- gcc/ada/exp_ch4.adb | 1 + gcc/ada/interfac.ads | 11 ++++++++--- gcc/ada/s-crtl.ads | 6 +++++- gcc/ada/s-osinte-linux.ads | 5 +---- gcc/ada/s-taskin.ads | 2 +- gcc/ada/sem_prag.adb | 12 +++++++++++- gcc/ada/sem_util.adb | 3 ++- gcc/ada/sinfo.ads | 6 ++++++ 13 files changed, 88 insertions(+), 17 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 7169bf7feb3..b88ce84ee58 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,31 @@ +2014-11-20 Thomas Quinot + + * sem_util.adb: Minor reformatting. + +2014-11-20 Robert Dewar + + * sem_prag.adb (Analyze_Pragma, case Linker_Section): Detect + duplicate Linker_Section. + +2014-11-20 Ed Schonberg + + * exp_ch4.adb: Add guard for build-in-place boolean op. + +2014-11-20 Yannick Moy + + * checks.adb (Apply_Scalar_Range_Check): In GNATprove mode, + put a range check when an empty range is used, instead of an + error message. + * sinfo.ads Update comment on GNATprove mode. + +2014-11-20 Arnaud Charlet + + * a-stream.ads, s-osinte-linux.ads, a-reatim.ads, a-calend.ads, + s-crtl.ads, interfac.ads, s-taskin.ads: Replace uses of 2 ** 63 and + 2 ** 64 by references to Long_Long_Integer instead, to allow these + units to be analyzed by codepeer or spark when using a target + configuration file with long_long_size set to 32. + 2014-11-20 Hristian Kirtchev * sem_util.adb (Extensions_Visible_Status): Modify the logic to account diff --git a/gcc/ada/a-calend.ads b/gcc/ada/a-calend.ads index 668efb9b32a..8e268b9c2b5 100644 --- a/gcc/ada/a-calend.ads +++ b/gcc/ada/a-calend.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2012, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- -- -- -- This specification is derived from the Ada Reference Manual for use with -- -- GNAT. The copyright notice above, and the license provisions that follow -- @@ -197,11 +197,14 @@ private -- Local Declarations -- ------------------------ - type Time_Rep is range -2 ** 63 .. +2 ** 63 - 1; + 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 - -- and arithmetic. + -- 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 + -- CodePeer. 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 084c1ef0593..b020adcd077 100644 --- a/gcc/ada/a-reatim.ads +++ b/gcc/ada/a-reatim.ads @@ -94,7 +94,8 @@ package Ada.Real_Time is -- 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 -2 ** 63 .. 2 ** 63 - 1; + type Seconds_Count is range + Long_Long_Integer'First .. Long_Long_Integer'Last; 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 388b5da27db..0977f285f6f 100644 --- a/gcc/ada/a-stream.ads +++ b/gcc/ada/a-stream.ads @@ -41,7 +41,8 @@ package Ada.Streams is type Stream_Element is mod 2 ** Standard'Storage_Unit; - type Stream_Element_Offset is range -(2 ** 63) .. +(2 ** 63) - 1; + type Stream_Element_Offset is range + Long_Long_Integer'First .. Long_Long_Integer'Last; subtype Stream_Element_Count is Stream_Element_Offset range 0 .. Stream_Element_Offset'Last; diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb index 046c5177f3c..e822db30b3e 100644 --- a/gcc/ada/checks.adb +++ b/gcc/ada/checks.adb @@ -2926,7 +2926,21 @@ package body Checks is -- since all possible values will raise CE). if Lov > Hiv then - Bad_Value; + + -- In GNATprove mode, do not issue a message in that case + -- (which would be an error stopping analysis), as this + -- likely corresponds to deactivated code based on a + -- given configuration (say, dead code inside a loop over + -- the empty range). Instead, we enable the range check + -- so that GNATprove will issue a message if it cannot be + -- proved. + + if GNATprove_Mode then + Enable_Range_Check (Expr); + else + Bad_Value; + end if; + return; end if; diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb index 0cceea14c45..aff9becb8dc 100644 --- a/gcc/ada/exp_ch4.adb +++ b/gcc/ada/exp_ch4.adb @@ -2269,6 +2269,7 @@ package body Exp_Ch4 is elsif Nkind (Parent (N)) = N_Op_Not and then Nkind (N) = N_Op_And + and then Nkind (Parent (Parent (N))) = N_Assignment_Statement and then Safe_In_Place_Array_Op (Name (Parent (Parent (N))), L, R) then return; diff --git a/gcc/ada/interfac.ads b/gcc/ada/interfac.ads index 1c88a507d7d..85ed9e956b7 100644 --- a/gcc/ada/interfac.ads +++ b/gcc/ada/interfac.ads @@ -51,10 +51,14 @@ package Interfaces is type Integer_32 is range -2 ** 31 .. 2 ** 31 - 1; for Integer_32'Size use 32; - type Integer_64 is range -2 ** 63 .. 2 ** 63 - 1; + type Integer_64 is range Long_Long_Integer'First .. Long_Long_Integer'Last; 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. - type Unsigned_8 is mod 2 ** 8; + type Unsigned_8 is mod 2 ** 8; for Unsigned_8'Size use 8; type Unsigned_16 is mod 2 ** 16; @@ -63,8 +67,9 @@ package Interfaces is type Unsigned_32 is mod 2 ** 32; for Unsigned_32'Size use 32; - type Unsigned_64 is mod 2 ** 64; + type Unsigned_64 is mod 2 ** Long_Long_Integer'Size; for Unsigned_64'Size use 64; + -- See comment on Integer_64 above function Shift_Left (Value : Unsigned_8; diff --git a/gcc/ada/s-crtl.ads b/gcc/ada/s-crtl.ads index 835bbd9e3ae..959fa4a2eb3 100644 --- a/gcc/ada/s-crtl.ads +++ b/gcc/ada/s-crtl.ads @@ -62,7 +62,11 @@ package System.CRTL is type ssize_t is range -(2 ** (Standard'Address_Size - 1)) .. +(2 ** (Standard'Address_Size - 1)) - 1; - type int64 is range -(2 ** 63) .. (2 ** 63) - 1; + type int64 is range Long_Long_Integer'First .. Long_Long_Integer'Last; + -- 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. 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-osinte-linux.ads b/gcc/ada/s-osinte-linux.ads index 15a351ac1c0..d6930de9640 100644 --- a/gcc/ada/s-osinte-linux.ads +++ b/gcc/ada/s-osinte-linux.ads @@ -599,9 +599,6 @@ private type pid_t is new int; - type unsigned_long_long_t is mod 2 ** 64; - -- Local type only used to get the alignment of this type below - subtype char_array is Interfaces.C.char_array; type pthread_attr_t is record @@ -644,7 +641,7 @@ private Data : char_array (1 .. OS_Constants.PTHREAD_COND_SIZE); end record; pragma Convention (C, pthread_cond_t); - for pthread_cond_t'Alignment use unsigned_long_long_t'Alignment; + for pthread_cond_t'Alignment use Interfaces.Unsigned_64'Alignment; type pthread_key_t is new unsigned; diff --git a/gcc/ada/s-taskin.ads b/gcc/ada/s-taskin.ads index a2f63a9cce8..bf198ca3e80 100644 --- a/gcc/ada/s-taskin.ads +++ b/gcc/ada/s-taskin.ads @@ -946,7 +946,7 @@ package System.Tasking is -- converted to a task attribute if it fits, or to a pointer to a record -- by Ada.Task_Attributes. - type Task_Serial_Number is mod 2 ** 64; + type Task_Serial_Number is mod 2 ** Long_Long_Integer'Size; -- Used to give each task a unique serial number type Ada_Task_Control_Block (Entry_Num : Task_Entry_Index) is record diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 5aa9514d188..c26e4f2ebff 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -16380,6 +16380,7 @@ package body Sem_Prag is when Pragma_Linker_Section => Linker_Section : declare Arg : Node_Id; Ent : Entity_Id; + LPE : Node_Id; begin GNAT_Pragma; @@ -16398,9 +16399,18 @@ package body Sem_Prag is case Ekind (Ent) is -- Objects (constants and variables) and types. For these cases - -- all we need to do is to set the Linker_Section_pragma field. + -- all we need to do is to set the Linker_Section_pragma field, + -- checking that we do not have a duplicate. when E_Constant | E_Variable | Type_Kind => + LPE := Linker_Section_Pragma (Ent); + + if Present (LPE) then + Error_Msg_Sloc := Sloc (LPE); + Error_Msg_NE + ("Linker_Section already specified for &#", Arg1, Ent); + end if; + Set_Linker_Section_Pragma (Ent, N); -- Subprograms diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index b2f40e6f1fd..981d2193062 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -6457,7 +6457,8 @@ package body Sem_Util is -- be a static subtype, since otherwise it would have -- been diagnosed as illegal. - elsif Is_Entity_Name (Choice) and then Is_Type (Entity (Choice)) + elsif Is_Entity_Name (Choice) + and then Is_Type (Entity (Choice)) then exit Search when Is_In_Range (Expr, Etype (Choice), Assume_Valid => False); diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index 7a3bc6ff016..f9c7052c4d3 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -581,6 +581,12 @@ package Sinfo is -- bounds are generated from an expression: Expand_Subtype_From_Expr -- should be noop. + -- 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). + ----------------------- -- Check Flag Fields -- ----------------------- -- 2.30.2