[multiple changes]

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.

From-SVN: r217841
This commit is contained in:
Arnaud Charlet 2014-11-20 12:28:12 +01:00
parent 39f0fa29d0
commit 697b781a68
13 changed files with 368 additions and 84 deletions

View File

@ -1,3 +1,24 @@
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.

View File

@ -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);

View File

@ -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;

View File

@ -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;

View File

@ -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
------------------
-- Remove_Items --
------------------
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_Precondition,
Name_Refined_Global,
Name_Refined_Depends,
Name_Refined_Post,
Name_Test_Case,
Name_Unmodified,
Name_Unreferenced)
then
Remove (Item);
end if;
Item := Next_Item;
end loop;
end Remove_Items;
-- Start of processing for Remove_Aspects_And_Pragmas
begin
Decl := First (Declarations (Bod));
while Present (Decl) loop
Nxt := Next (Decl);
if Nkind (Decl) = N_Pragma
and then Nam_In (Pragma_Name (Decl), Name_Contract_Cases,
Name_Precondition,
Name_Postcondition,
Name_Unreferenced,
Name_Unmodified)
then
Remove (Decl);
end if;
Decl := Nxt;
end loop;
end Remove_Pragmas;
Remove_Items (Aspect_Specifications (Body_Decl));
Remove_Items (Declarations (Body_Decl));
end Remove_Aspects_And_Pragmas;
end Inline;

View File

@ -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;

View File

@ -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 --
------------------

View File

@ -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

View File

@ -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);

View File

@ -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;

View File

@ -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.

View File

@ -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));
-- The pragma appears with an argument
if Present (Arg) then
Expr := Get_Pragma_Arg (Arg);
if Present (Arg1) then
Expr := Get_Pragma_Arg (Arg1);
-- When the associated subprogram is an expression function, the
-- argument of the pragma may not have been analyzed.
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;

View File

@ -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 --