[multiple changes]
2016-05-02 Hristian Kirtchev <kirtchev@adacore.com> * lib-xref.ads, lib-xref-spark_specific.adb, get_spark_xrefs.adb, put_spark_xrefs.adb: Minor reformatting. 2016-05-02 Doug Rupp <rupp@adacore.com> * g-traceb.ads: Document traceback for ARM. 2016-05-02 Javier Miranda <miranda@adacore.com> * exp_disp.adb (Make_Tags): Do not generate the external name of interface tags adding the suffix counter since it causes problems at link time when the IP routines are inlined across units with optimization. 2016-05-02 Ed Schonberg <schonberg@adacore.com> * einfo.ads, einfo.adb (Predicates_Ignared): new flag to indicate that predicate checking is disabled for predicated subtypes in the context of an Assertion_Policy pragma. * checks.adb (Apply_Predicate_Check): Do nothing if Predicates_Ignored is true. * exp_ch3.adb (Expand_Freeze_Enumeration_Type): If Predicates_Ignores is true, the function Rep_To_Pos does raise an exception for invalid data. * exp_ch4.adb (Expand_N_Type_Conversion): IF target is a predicated type do not apply check if Predicates_Ignored is true. * exp_ch5.adb (Expand_N_Case_Statement): If Predicates_Ignored is true, sem_prag.adb: * sem_ch3.adb (Analyze_Object_Declaration): If Predicates_Ignored is true do not emit predicate check on initializing expression. From-SVN: r235730
This commit is contained in:
parent
bcb0389ef3
commit
8d4611f7b0
|
@ -1,3 +1,36 @@
|
|||
2016-05-02 Hristian Kirtchev <kirtchev@adacore.com>
|
||||
|
||||
* lib-xref.ads, lib-xref-spark_specific.adb, get_spark_xrefs.adb,
|
||||
put_spark_xrefs.adb: Minor reformatting.
|
||||
|
||||
2016-05-02 Doug Rupp <rupp@adacore.com>
|
||||
|
||||
* g-traceb.ads: Document traceback for ARM.
|
||||
|
||||
2016-05-02 Javier Miranda <miranda@adacore.com>
|
||||
|
||||
* exp_disp.adb (Make_Tags): Do not generate the
|
||||
external name of interface tags adding the suffix counter since
|
||||
it causes problems at link time when the IP routines are inlined
|
||||
across units with optimization.
|
||||
|
||||
2016-05-02 Ed Schonberg <schonberg@adacore.com>
|
||||
|
||||
* einfo.ads, einfo.adb (Predicates_Ignared): new flag to indicate
|
||||
that predicate checking is disabled for predicated subtypes in
|
||||
the context of an Assertion_Policy pragma.
|
||||
* checks.adb (Apply_Predicate_Check): Do nothing if
|
||||
Predicates_Ignored is true.
|
||||
* exp_ch3.adb (Expand_Freeze_Enumeration_Type): If
|
||||
Predicates_Ignores is true, the function Rep_To_Pos does raise
|
||||
an exception for invalid data.
|
||||
* exp_ch4.adb (Expand_N_Type_Conversion): IF target is a predicated
|
||||
type do not apply check if Predicates_Ignored is true.
|
||||
* exp_ch5.adb (Expand_N_Case_Statement): If Predicates_Ignored
|
||||
is true, sem_prag.adb:
|
||||
* sem_ch3.adb (Analyze_Object_Declaration): If Predicates_Ignored
|
||||
is true do not emit predicate check on initializing expression.
|
||||
|
||||
2016-05-02 Arnaud Charlet <charlet@adacore.com>
|
||||
|
||||
* get_spark_xrefs.adb (Get_Nat, Get_Name): Initialize variables when
|
||||
|
|
|
@ -2670,6 +2670,9 @@ package body Checks is
|
|||
if Predicate_Checks_Suppressed (Empty) then
|
||||
return;
|
||||
|
||||
elsif Predicates_Ignored (Typ) then
|
||||
return;
|
||||
|
||||
elsif Present (Predicate_Function (Typ)) then
|
||||
S := Current_Scope;
|
||||
while Present (S) and then not Is_Subprogram (S) loop
|
||||
|
|
|
@ -601,8 +601,8 @@ package body Einfo is
|
|||
-- Is_Volatile_Full_Access Flag285
|
||||
-- Is_Exception_Handler Flag286
|
||||
-- Rewritten_For_C Flag287
|
||||
-- Predicates_Ignored Flag288
|
||||
|
||||
-- (unused) Flag288
|
||||
-- (unused) Flag289
|
||||
-- (unused) Flag300
|
||||
|
||||
|
@ -2910,6 +2910,12 @@ package body Einfo is
|
|||
return Node14 (Id);
|
||||
end Postconditions_Proc;
|
||||
|
||||
function Predicates_Ignored (Id : E) return B is
|
||||
begin
|
||||
pragma Assert (Is_Type (Id));
|
||||
return Flag288 (Id);
|
||||
end Predicates_Ignored;
|
||||
|
||||
function Prival (Id : E) return E is
|
||||
begin
|
||||
pragma Assert (Is_Protected_Component (Id));
|
||||
|
@ -5971,6 +5977,12 @@ package body Einfo is
|
|||
Set_Node14 (Id, V);
|
||||
end Set_Postconditions_Proc;
|
||||
|
||||
procedure Set_Predicates_Ignored (Id : E; V : B) is
|
||||
begin
|
||||
pragma Assert (Is_Type (Id));
|
||||
Set_Flag288 (Id, V);
|
||||
end Set_Predicates_Ignored;
|
||||
|
||||
procedure Set_Direct_Primitive_Operations (Id : E; V : L) is
|
||||
begin
|
||||
pragma Assert (Is_Tagged_Type (Id));
|
||||
|
@ -9130,6 +9142,7 @@ package body Einfo is
|
|||
W ("Reverse_Bit_Order", Flag164 (Id));
|
||||
W ("Reverse_Storage_Order", Flag93 (Id));
|
||||
W ("Rewritten_For_C", Flag287 (Id));
|
||||
W ("Predicates_Ignored", Flag288 (Id));
|
||||
W ("Sec_Stack_Needed_For_Return", Flag167 (Id));
|
||||
W ("Size_Depends_On_Discriminant", Flag177 (Id));
|
||||
W ("Size_Known_At_Compile_Time", Flag92 (Id));
|
||||
|
|
|
@ -3767,6 +3767,11 @@ package Einfo is
|
|||
-- is the special version created for membership tests, where if one of
|
||||
-- these raise expressions is executed, the result is to return False.
|
||||
|
||||
-- Predicates_Ignored (Flag288)
|
||||
-- Defined on all types. Indicates whether the subtype declaration is in
|
||||
-- a context where Assertion_Policy is Ignore, in which case no checks
|
||||
-- (static or dynamic) must be generated for objects of the type.
|
||||
|
||||
-- Primitive_Operations (synthesized)
|
||||
-- Defined in concurrent types, tagged record types and subtypes, tagged
|
||||
-- private types and tagged incomplete types. For concurrent types whose
|
||||
|
@ -7137,6 +7142,7 @@ package Einfo is
|
|||
function Partial_View_Has_Unknown_Discr (Id : E) return B;
|
||||
function Pending_Access_Types (Id : E) return L;
|
||||
function Postconditions_Proc (Id : E) return E;
|
||||
function Predicates_Ignored (Id : E) return B;
|
||||
function Prival (Id : E) return E;
|
||||
function Prival_Link (Id : E) return E;
|
||||
function Private_Dependents (Id : E) return L;
|
||||
|
@ -7489,6 +7495,7 @@ package Einfo is
|
|||
procedure Set_Depends_On_Private (Id : E; V : B := True);
|
||||
procedure Set_Derived_Type_Link (Id : E; V : E);
|
||||
procedure Set_Digits_Value (Id : E; V : U);
|
||||
procedure Set_Predicates_Ignored (Id : E; V : B);
|
||||
procedure Set_Direct_Primitive_Operations (Id : E; V : L);
|
||||
procedure Set_Directly_Designated_Type (Id : E; V : E);
|
||||
procedure Set_Disable_Controlled (Id : E; V : B := True);
|
||||
|
@ -8637,6 +8644,7 @@ package Einfo is
|
|||
pragma Inline (Partial_View_Has_Unknown_Discr);
|
||||
pragma Inline (Pending_Access_Types);
|
||||
pragma Inline (Postconditions_Proc);
|
||||
pragma Inline (Predicates_Ignored);
|
||||
pragma Inline (Prival);
|
||||
pragma Inline (Prival_Link);
|
||||
pragma Inline (Private_Dependents);
|
||||
|
@ -9100,6 +9108,7 @@ package Einfo is
|
|||
pragma Inline (Set_Partial_View_Has_Unknown_Discr);
|
||||
pragma Inline (Set_Pending_Access_Types);
|
||||
pragma Inline (Set_Postconditions_Proc);
|
||||
pragma Inline (Set_Predicates_Ignored);
|
||||
pragma Inline (Set_Prival);
|
||||
pragma Inline (Set_Prival_Link);
|
||||
pragma Inline (Set_Private_Dependents);
|
||||
|
|
|
@ -5034,9 +5034,13 @@ package body Exp_Ch3 is
|
|||
end loop;
|
||||
end if;
|
||||
|
||||
-- In normal mode, add the others clause with the test
|
||||
-- In normal mode, add the others clause with the test.
|
||||
-- If Predicates_Ignored is True, validity checks do not apply to
|
||||
-- the subtype.
|
||||
|
||||
if not No_Exception_Handlers_Set then
|
||||
if not No_Exception_Handlers_Set
|
||||
and then not Predicates_Ignored (Typ)
|
||||
then
|
||||
Append_To (Lst,
|
||||
Make_Case_Statement_Alternative (Loc,
|
||||
Discrete_Choices => New_List (Make_Others_Choice (Loc)),
|
||||
|
|
|
@ -11387,6 +11387,7 @@ package body Exp_Ch4 is
|
|||
-- internal conversions for the purpose of checking predicates.
|
||||
|
||||
if Present (Predicate_Function (Target_Type))
|
||||
and then not Predicates_Ignored (Target_Type)
|
||||
and then Target_Type /= Operand_Type
|
||||
and then Comes_From_Source (N)
|
||||
then
|
||||
|
|
|
@ -2573,10 +2573,11 @@ package body Exp_Ch5 is
|
|||
-- does not obey the predicate, the value is marked non-static, and
|
||||
-- there can be no corresponding static alternative. In that case we
|
||||
-- replace the case statement with an exception, regardless of whether
|
||||
-- assertions are enabled or not.
|
||||
-- assertions are enabled or not, unless predicates are ignored.
|
||||
|
||||
if Compile_Time_Known_Value (Expr)
|
||||
and then Has_Predicates (Etype (Expr))
|
||||
and then not Predicates_Ignored (Etype (Expr))
|
||||
and then not Is_OK_Static_Expression (Expr)
|
||||
then
|
||||
Rewrite (N,
|
||||
|
@ -2659,7 +2660,9 @@ package body Exp_Ch5 is
|
|||
-- comes from source -- no need to validity check internally
|
||||
-- generated case statements).
|
||||
|
||||
if Validity_Check_Default then
|
||||
if Validity_Check_Default
|
||||
and then not Predicates_Ignored (Etype (Expr))
|
||||
then
|
||||
Ensure_Valid (Expr);
|
||||
end if;
|
||||
|
||||
|
@ -2788,11 +2791,33 @@ package body Exp_Ch5 is
|
|||
|
||||
if not Others_Present then
|
||||
Others_Node := Make_Others_Choice (Sloc (Last_Alt));
|
||||
|
||||
-- If Predicates_Ignored is true the value does not satisfy the
|
||||
-- predicate, and there is no Others choice, Constraint_Error
|
||||
-- must be raised (4.5.7 (21/3)).
|
||||
|
||||
if Predicates_Ignored (Etype (Expr)) then
|
||||
declare
|
||||
Except : constant Node_Id :=
|
||||
Make_Raise_Constraint_Error (Loc,
|
||||
Reason => CE_Invalid_Data);
|
||||
New_Alt : constant Node_Id :=
|
||||
Make_Case_Statement_Alternative (Loc,
|
||||
Discrete_Choices => New_List (Make_Others_Choice (Loc)),
|
||||
Statements => New_List (Except));
|
||||
begin
|
||||
Append (New_Alt, Alternatives (N));
|
||||
Analyze_And_Resolve (Except);
|
||||
end;
|
||||
|
||||
else
|
||||
Set_Others_Discrete_Choices
|
||||
(Others_Node, Discrete_Choices (Last_Alt));
|
||||
Set_Discrete_Choices (Last_Alt, New_List (Others_Node));
|
||||
end if;
|
||||
|
||||
end if;
|
||||
|
||||
-- Deal with possible declarations of controlled objects, and also
|
||||
-- with rewriting choice sequences for static predicate references.
|
||||
|
||||
|
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- B o d y --
|
||||
-- --
|
||||
-- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1992-2016, 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- --
|
||||
|
@ -6751,8 +6751,7 @@ package body Exp_Disp is
|
|||
if Building_Static_DT (Typ) then
|
||||
Iface_DT :=
|
||||
Make_Defining_Identifier (Loc,
|
||||
Chars => New_External_Name
|
||||
(Typ_Name, 'T', Suffix_Index => -1));
|
||||
Chars => New_External_Name (Typ_Name, 'T'));
|
||||
Import_DT
|
||||
(Tag_Typ => Related_Type (Node (AI_Tag_Comp)),
|
||||
DT => Iface_DT,
|
||||
|
|
|
@ -65,6 +65,8 @@
|
|||
-- LynxOS 178 elf PowerPC
|
||||
-- Solaris x86
|
||||
-- Solaris sparc
|
||||
-- VxWorks ARM
|
||||
-- VxWorks7 ARM
|
||||
-- VxWorks PowerPC
|
||||
-- VxWorks x86
|
||||
-- Windows XP
|
||||
|
|
|
@ -114,8 +114,8 @@ procedure Get_SPARK_Xrefs is
|
|||
-------------
|
||||
|
||||
function Get_Nat return Nat is
|
||||
Val : Nat := 0;
|
||||
C : Character := Nextc;
|
||||
Val : Nat := 0;
|
||||
|
||||
begin
|
||||
if C not in '0' .. '9' then
|
||||
|
|
|
@ -509,9 +509,9 @@ package Lib.Xref is
|
|||
E_Void => ' ',
|
||||
|
||||
-- The following entities are not ones to which we gather the cross-
|
||||
-- references, since it does not make sense to do so (e.g. references to
|
||||
-- a package are to the spec, not the body) Indeed the occurrence of the
|
||||
-- body entity is considered to be a reference to the spec entity.
|
||||
-- references, since it does not make sense to do so (e.g. references
|
||||
-- to a package are to the spec, not the body). Indeed the occurrence of
|
||||
-- the body entity is considered to be a reference to the spec entity.
|
||||
|
||||
E_Package_Body => ' ',
|
||||
E_Protected_Body => ' ',
|
||||
|
|
|
@ -104,6 +104,7 @@ begin
|
|||
|
||||
begin
|
||||
-- Write only non-empty tables
|
||||
|
||||
if S.From_Xref <= S.To_Xref then
|
||||
|
||||
Write_Info_Initiate ('F');
|
||||
|
|
|
@ -3814,14 +3814,15 @@ package body Sem_Ch3 is
|
|||
-- do this in the analyzer and not the expander because the analyzer
|
||||
-- does some substantial rewriting in some cases.
|
||||
|
||||
-- We need a predicate check if the type has predicates, and if either
|
||||
-- there is an initializing expression, or for default initialization
|
||||
-- when we have at least one case of an explicit default initial value
|
||||
-- and then this is not an internal declaration whose initialization
|
||||
-- comes later (as for an aggregate expansion).
|
||||
-- We need a predicate check if the type has predicates that are not
|
||||
-- ignored, and if either there is an initializing expression, or for
|
||||
-- default initialization when we have at least one case of an explicit
|
||||
-- default initial value and then this is not an internal declaration
|
||||
-- whose initialization comes later (as for an aggregate expansion).
|
||||
|
||||
if not Suppress_Assignment_Checks (N)
|
||||
and then Present (Predicate_Function (T))
|
||||
and then not Predicates_Ignored (T)
|
||||
and then not No_Initialization (N)
|
||||
and then
|
||||
(Present (E)
|
||||
|
|
|
@ -18744,8 +18744,15 @@ package body Sem_Prag is
|
|||
-- the rep item chain, for processing when the type is frozen.
|
||||
-- This is accomplished by a call to Rep_Item_Too_Late. We also
|
||||
-- mark the type as having predicates.
|
||||
-- If the current policy is Ignore mark the subtype accordingly.
|
||||
-- In the case of predicates we consider them enabled unless an
|
||||
-- Ignore is specified, to preserve existing warnings.
|
||||
|
||||
Set_Has_Predicates (Typ);
|
||||
Set_Predicates_Ignored (Typ,
|
||||
Present (Check_Policy_List)
|
||||
and then
|
||||
Policy_In_Effect (Name_Assertion_Policy) = Name_Ignore);
|
||||
Discard := Rep_Item_Too_Late (Typ, N, FOnly => True);
|
||||
end Predicate;
|
||||
|
||||
|
@ -28563,6 +28570,7 @@ package body Sem_Prag is
|
|||
-- RM defined
|
||||
|
||||
Name_Assert |
|
||||
Name_Assertion_Policy |
|
||||
Name_Static_Predicate |
|
||||
Name_Dynamic_Predicate |
|
||||
Name_Pre |
|
||||
|
|
Loading…
Reference in New Issue