+2014-11-20 Robert Dewar <dewar@adacore.com>
+
+ * 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 <kirtchev@adacore.com>
+
+ * 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 <kirtchev@adacore.com>
+
+ * 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 <quinot@adacore.com>
* sem_util.adb: Minor reformatting.
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);
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;
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;
-- --
------------------------------------------------------------------------------
+with Aspects; use Aspects;
with Atree; use Atree;
with Debug; use Debug;
with Einfo; use Einfo;
-- 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 --
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);
-- 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
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;
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.
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;
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;
-- --
-- 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- --
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 --
------------------
-- --
-- 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- --
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
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);
-- 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;
-- 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;
-- 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.
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;
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.
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;
-- 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
-- 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 --
projects / gcc.git / commitdiff