* 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.
git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@217840
138bc75d-0d04-0410-961f-
82ee72b054a4
+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
-- --
-- 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 --
-- 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);
-- 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;
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;
-- 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;
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;
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;
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;
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);
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
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;
-- 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
when Pragma_Linker_Section => Linker_Section : declare
Arg : Node_Id;
Ent : Entity_Id;
+ LPE : Node_Id;
begin
GNAT_Pragma;
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
-- 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);
-- 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 --
-----------------------
projects / platform / upstream / linaro-gcc.git / commitdiff