[multiple changes]

2014-11-20  Thomas Quinot  <quinot@adacore.com>

	* sem_util.adb: Minor reformatting.

2014-11-20  Robert Dewar  <dewar@adacore.com>

	* sem_prag.adb (Analyze_Pragma, case Linker_Section): Detect
	duplicate Linker_Section.

2014-11-20  Ed Schonberg  <schonberg@adacore.com>

	* exp_ch4.adb: Add guard for build-in-place boolean op.

2014-11-20  Yannick Moy  <moy@adacore.com>

	* 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  <charlet@adacore.com>

	* 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

13 files changed, 88 insertions, 17 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 7169bf7..b88ce84 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,31 @@
+2014-11-20  Thomas Quinot  <quinot@adacore.com>
+
+	* sem_util.adb: Minor reformatting.
+
+2014-11-20  Robert Dewar  <dewar@adacore.com>
+
+	* sem_prag.adb (Analyze_Pragma, case Linker_Section): Detect
+	duplicate Linker_Section.
+
+2014-11-20  Ed Schonberg  <schonberg@adacore.com>
+
+	* exp_ch4.adb: Add guard for build-in-place boolean op.
+
+2014-11-20  Yannick Moy  <moy@adacore.com>
+
+	* 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  <charlet@adacore.com>
+
+	* 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  <kirtchev@adacore.com>
 
 	* 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 668efb9..8e268b9 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 084c1ef..b020adc 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 388b5da..0977f28 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 046c517..e822db3 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 0cceea1..aff9bec 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 1c88a50..85ed9e9 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 835bbd9..959fa4a 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 15a351a..d6930de 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 a2f63a9..bf198ca 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 5aa9514..c26e4f2 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 b2f40e6..981d219 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 7a3bc6f..f9c7052 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 --
    -----------------------