+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
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
-- Is_Volatile_Full_Access Flag285
-- Is_Exception_Handler Flag286
-- Rewritten_For_C Flag287
+ -- Predicates_Ignored Flag288
- -- (unused) Flag288
-- (unused) Flag289
-- (unused) Flag300
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));
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));
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));
-- 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
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;
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);
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);
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);
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)),
-- 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
-- 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,
-- 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;
if not Others_Present then
Others_Node := Make_Others_Choice (Sloc (Last_Alt));
- Set_Others_Discrete_Choices
- (Others_Node, Discrete_Choices (Last_Alt));
- Set_Discrete_Choices (Last_Alt, New_List (Others_Node));
+
+ -- 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
-- --
-- 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- --
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,
-- LynxOS 178 elf PowerPC
-- Solaris x86
-- Solaris sparc
+-- VxWorks ARM
+-- VxWorks7 ARM
-- VxWorks PowerPC
-- VxWorks x86
-- Windows XP
-------------
function Get_Nat return Nat is
- Val : Nat := 0;
C : Character := Nextc;
+ Val : Nat := 0;
begin
if C not in '0' .. '9' then
Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
Spec_Entity : constant Entity_Id :=
- Unique_Entity (Srec.Scope_Entity);
+ Unique_Entity (Srec.Scope_Entity);
Spec_Scope : constant Scope_Index :=
- Entity_Hash_Table.Get (Spec_Entity);
+ Entity_Hash_Table.Get (Spec_Entity);
begin
-- Generic spec may be missing in which case Spec_Scope is zero
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 => ' ',
begin
-- Write only non-empty tables
+
if S.From_Xref <= S.To_Xref then
Write_Info_Initiate ('F');
Output_One_Xref : declare
R : SPARK_Xref_Record renames
- SPARK_Xref_Table.Table (X);
+ SPARK_Xref_Table.Table (X);
begin
if R.Entity_Line /= Entity_Line
-- 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)
-- 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;
-- RM defined
Name_Assert |
+ Name_Assertion_Policy |
Name_Static_Predicate |
Name_Dynamic_Predicate |
Name_Pre |
projects / gcc.git / commitdiff