+2017-04-25 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * einfo.adb Flag301 is now known as Ignore_SPARK_Mode_Pragmas.
+ (Ignore_SPARK_Mode_Pragmas): New routine.
+ (Set_Ignore_SPARK_Mode_Pragmas): New routine.
+ (Write_Entity_Flags): Add an entry for Ignore_SPARK_Mode_Pragmas.
+ * einfo.ads Add new attribute Ignore_SPARK_Mode_Pragmas and update
+ related entities.
+ (Ignore_SPARK_Mode_Pragmas): New routine
+ along with pragma Inline.
+ (Set_Ignore_SPARK_Mode_Pragmas): New routine along with pragma Inline.
+ * opt.ads Rename flag Ignore_Pragma_SPARK_Mode to
+ Ignore_SPARK_Mode_Pragmas_In_Instance.
+ * sem_ch6.adb (Analyze_Subprogram_Body_Helper):
+ Save and restore the value of global flag
+ Ignore_SPARK_Mode_Pragmas_In_Instance. Set or reinstate the value
+ of global flag Ignore_SPARK_Mode_Pragmas_In_Instance when either
+ the corresponding spec or the body must ignore all SPARK_Mode
+ pragmas found within.
+ (Analyze_Subprogram_Declaration): Mark
+ the spec when it needs to ignore all SPARK_Mode pragmas found
+ within to allow the body to infer this property in case it is
+ instantiated or inlined later.
+ * sem_ch7.adb (Analyze_Package_Body_Helper): Save and restore the
+ value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set
+ the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance
+ when the corresponding spec also ignored all SPARK_Mode pragmas
+ found within.
+ (Analyze_Package_Declaration): Mark the spec when
+ it needs to ignore all SPARK_Mode pragmas found within to allow
+ the body to infer this property in case it is instantiated or
+ inlined later.
+ * sem_ch12.adb (Analyze_Formal_Package_Declaration):
+ Save and restore the value of flag
+ Ignore_SPARK_Mode_Pragmas_In_Instance. Mark the
+ formal spec when it needs to ignore all SPARK_Mode
+ pragmas found within to allow the body to infer this
+ property in case it is instantiated or inlined later.
+ (Analyze_Package_Instantiation): Save and restore the value
+ of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Mark
+ the instance spec when it needs to ignore all SPARK_Mode
+ pragmas found within to allow the body to infer this
+ property in case it is instantiated or inlined later.
+ (Analyze_Subprogram_Instantiation): Save and restore the value
+ of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Mark the
+ instance spec and anonymous package when they need to ignore
+ all SPARK_Mode pragmas found within to allow the body to infer
+ this property in case it is instantiated or inlined later.
+ (Instantiate_Package_Body): Save and restore the value of global
+ flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set the value of
+ global flag Ignore_SPARK_Mode_Pragmas_In_Instance when the
+ corresponding instance spec also ignored all SPARK_Mode pragmas
+ found within.
+ (Instantiate_Subprogram_Body): Save and restore the
+ value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance. Set
+ the value of global flag Ignore_SPARK_Mode_Pragmas_In_Instance
+ when the corresponding instance spec also ignored all SPARK_Mode
+ pragmas found within.
+ * sem_prag.adb (Analyze_Pragma): Update the reference to
+ Ignore_Pragma_SPARK_Mode.
+ * sem_util.adb (SPARK_Mode_Is_Off): A construct which ignored
+ all SPARK_Mode pragmas defined within yields mode "off".
+
+2017-04-25 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * bindgen.adb, exp_dbug.adb, errout.adb, fname.adb: Minor reformatting.
+
+2017-04-25 Bob Duff <duff@adacore.com>
+
+ * exp_atag.adb (Build_CW_Membership): Add "Suppress =>
+ All_Checks" to avoid generating unnecessary checks.
+ * exp_ch4.adb (Expand_N_In, Make_Tag_Check): Add "Suppress =>
+ All_Checks".
+ * sem.ads: Fix comment.
+ * expander.ads: Fix comment.
+ * exp_atag.ads: Fix comment: "Index = 0" should be
+ "Index >= 0".
+
+2017-04-25 Gary Dismukes <dismukes@adacore.com>
+
+ * s-taprop-linux.adb: Minor editorial fixes.
+
2017-04-25 Eric Botcazou <ebotcazou@adacore.com>
* sem_util.adb (New_Copy_Tree): Put back the declarations of the
-- where we increment the elaboration entity if one exists.
-- Likewise for lone specs with an elaboration entity defined
- -- despite No_Elaboration_Code, e.g. when requested to
- -- preserve control flow.
+ -- despite No_Elaboration_Code, e.g. when requested to preserve
+ -- control flow.
if (U.Utype = Is_Body or else U.Utype = Is_Spec_Only)
and then Units.Table (Unum_Spec).Set_Elab_Entity
-- Body_Needed_For_Inlining Flag299
-- Has_Private_Extension Flag300
- -- (unused) Flag301
+ -- Ignore_SPARK_Mode_Pragmas Flag301
-- (unused) Flag302
-- (unused) Flag303
-- (unused) Flag304
return Node4 (Id);
end Homonym;
+ function Ignore_SPARK_Mode_Pragmas (Id : E) return B is
+ begin
+ pragma Assert
+ (Ekind_In (Id, E_Protected_Body, -- concurrent variants
+ E_Protected_Type,
+ E_Task_Body,
+ E_Task_Type)
+ or else
+ Ekind_In (Id, E_Entry, -- overloadable variants
+ E_Entry_Family,
+ E_Function,
+ E_Generic_Function,
+ E_Generic_Procedure,
+ E_Operator,
+ E_Procedure,
+ E_Subprogram_Body)
+ or else
+ Ekind_In (Id, E_Generic_Package, -- package variants
+ E_Package,
+ E_Package_Body));
+ return Flag301 (Id);
+ end Ignore_SPARK_Mode_Pragmas;
+
function Import_Pragma (Id : E) return E is
begin
pragma Assert (Is_Subprogram (Id));
Set_Elist24 (Id, V);
end Set_Incomplete_Actuals;
+ procedure Set_Ignore_SPARK_Mode_Pragmas (Id : E; V : B := True) is
+ begin
+ pragma Assert
+ (Ekind_In (Id, E_Protected_Body, -- concurrent variants
+ E_Protected_Type,
+ E_Task_Body,
+ E_Task_Type)
+ or else
+ Ekind_In (Id, E_Entry, -- overloadable variants
+ E_Entry_Family,
+ E_Function,
+ E_Generic_Function,
+ E_Generic_Procedure,
+ E_Operator,
+ E_Procedure,
+ E_Subprogram_Body)
+ or else
+ Ekind_In (Id, E_Generic_Package, -- package variants
+ E_Package,
+ E_Package_Body));
+ Set_Flag301 (Id, V);
+ end Set_Ignore_SPARK_Mode_Pragmas;
+
procedure Set_Import_Pragma (Id : E; V : E) is
begin
pragma Assert (Is_Subprogram (Id));
W ("Has_Visible_Refinement", Flag263 (Id));
W ("Has_Volatile_Components", Flag87 (Id));
W ("Has_Xref_Entry", Flag182 (Id));
+ W ("Ignore_SPARK_Mode_Pragmas", Flag301 (Id));
W ("In_Package_Body", Flag48 (Id));
W ("In_Private_Part", Flag45 (Id));
W ("In_Use", Flag8 (Id));
-- scopes. Homonyms in the same scope are overloaded. Used for name
-- resolution and for the generation of debugging information.
+-- Ignore_SPARK_Mode_Pragmas (Flag301)
+-- Present in concurrent type, entry, operator, [generic] package,
+-- package body, [generic] subprogram, and subprogram body entities.
+-- Set when the entity appears in an instance subject to SPARK_Mode
+-- "off" and indicates that all SPARK_Mode pragmas found within must
+-- be ignored.
+
-- Implementation_Base_Type (synthesized)
-- Applies to all entities. For types, similar to Base_Type, but never
-- returns a private type when applied to a non-private type. Instead in
-- Extra_Formals (Node28)
-- Contract (Node34)
-- SPARK_Pragma (Node40) (protected kind)
- -- Needs_No_Actuals (Flag22)
- -- Uses_Sec_Stack (Flag95)
-- Default_Expressions_Processed (Flag108)
-- Entry_Accepted (Flag152)
- -- Sec_Stack_Needed_For_Return (Flag167)
-- Has_Expanded_Contract (Flag240)
- -- SPARK_Pragma_Inherited (Flag265) (protected kind)
+ -- Ignore_SPARK_Mode_Pragmas (Flag301)
-- Is_Entry_Wrapper (Flag297)
+ -- Needs_No_Actuals (Flag22)
+ -- Sec_Stack_Needed_For_Return (Flag167)
+ -- SPARK_Pragma_Inherited (Flag265) (protected kind)
+ -- Uses_Sec_Stack (Flag95)
-- Address_Clause (synth)
-- Entry_Index_Type (synth)
-- First_Formal (synth)
-- Has_Nested_Subprogram (Flag282)
-- Has_Out_Or_In_Out_Parameter (Flag110)
-- Has_Recursive_Call (Flag143)
+ -- Ignore_SPARK_Mode_Pragmas (Flag301)
-- Is_Abstract_Subprogram (Flag19) (non-generic case only)
-- Is_Called (Flag102) (non-generic case only)
-- Is_Constructor (Flag76)
-- SPARK_Pragma (Node40)
-- Default_Expressions_Processed (Flag108)
-- Has_Nested_Subprogram (Flag282)
+ -- Ignore_SPARK_Mode_Pragmas (Flag301)
-- Is_Intrinsic_Subprogram (Flag64)
-- Is_Machine_Code_Subprogram (Flag137)
-- Is_Primitive (Flag218)
-- Has_Forward_Instantiation (Flag175)
-- Has_Master_Entity (Flag21)
-- Has_RACW (Flag214) (non-generic case only)
+ -- Ignore_SPARK_Mode_Pragmas (Flag301)
-- In_Package_Body (Flag48)
-- In_Use (Flag8)
-- Is_Instantiated (Flag126)
-- SPARK_Aux_Pragma (Node41)
-- Contains_Ignored_Ghost_Code (Flag279)
-- Delay_Subprogram_Descriptors (Flag50)
+ -- Ignore_SPARK_Mode_Pragmas (Flag301)
-- SPARK_Aux_Pragma_Inherited (Flag266)
-- SPARK_Pragma_Inherited (Flag265)
-- Scope_Depth (synth)
-- Has_Master_Entity (Flag21)
-- Has_Nested_Block_With_Handler (Flag101)
-- Has_Nested_Subprogram (Flag282)
+ -- Ignore_SPARK_Mode_Pragmas (Flag301)
-- Is_Abstract_Subprogram (Flag19) (non-generic case only)
-- Is_Asynchronous (Flag81)
-- Is_Called (Flag102) (non-generic case only)
-- E_Protected_Body
-- SPARK_Pragma (Node40)
+ -- Ignore_SPARK_Mode_Pragmas (Flag301)
-- SPARK_Pragma_Inherited (Flag265)
-- (any others??? First/Last Entity, Scope_Depth???)
-- Entry_Max_Queue_Lengths_Array (Node35)
-- SPARK_Pragma (Node40)
-- SPARK_Aux_Pragma (Node41)
+ -- Ignore_SPARK_Mode_Pragmas (Flag301)
-- Sec_Stack_Needed_For_Return (Flag167) ???
-- SPARK_Aux_Pragma_Inherited (Flag266)
-- SPARK_Pragma_Inherited (Flag265)
-- E_Task_Body
-- Contract (Node34)
-- SPARK_Pragma (Node40)
+ -- Ignore_SPARK_Mode_Pragmas (Flag301)
-- SPARK_Pragma_Inherited (Flag265)
-- (any others??? First/Last Entity, Scope_Depth???)
-- Delay_Cleanups (Flag114)
-- Has_Master_Entity (Flag21)
-- Has_Storage_Size_Clause (Flag23) (base type only)
+ -- Ignore_SPARK_Mode_Pragmas (Flag301)
-- Sec_Stack_Needed_For_Return (Flag167) ???
-- SPARK_Aux_Pragma_Inherited (Flag266)
-- SPARK_Pragma_Inherited (Flag265)
function Has_Xref_Entry (Id : E) return B;
function Hiding_Loop_Variable (Id : E) return E;
function Homonym (Id : E) return E;
+ function Ignore_SPARK_Mode_Pragmas (Id : E) return B;
function Import_Pragma (Id : E) return E;
function Incomplete_Actuals (Id : E) return L;
function In_Package_Body (Id : E) return B;
procedure Set_Has_Xref_Entry (Id : E; V : B := True);
procedure Set_Hiding_Loop_Variable (Id : E; V : E);
procedure Set_Homonym (Id : E; V : E);
+ procedure Set_Ignore_SPARK_Mode_Pragmas (Id : E; V : B := True);
procedure Set_Import_Pragma (Id : E; V : E);
procedure Set_Incomplete_Actuals (Id : E; V : L);
procedure Set_In_Package_Body (Id : E; V : B := True);
pragma Inline (Has_Xref_Entry);
pragma Inline (Hiding_Loop_Variable);
pragma Inline (Homonym);
+ pragma Inline (Ignore_SPARK_Mode_Pragmas);
pragma Inline (Import_Pragma);
pragma Inline (Incomplete_Actuals);
pragma Inline (In_Package_Body);
pragma Inline (Set_Has_Xref_Entry);
pragma Inline (Set_Hiding_Loop_Variable);
pragma Inline (Set_Homonym);
+ pragma Inline (Set_Ignore_SPARK_Mode_Pragmas);
pragma Inline (Set_Import_Pragma);
pragma Inline (Set_Incomplete_Actuals);
pragma Inline (Set_In_Package_Body);
Error_Msg_Internal
("info: in inlined body #",
Actual_Error_Loc, Flag_Location, Msg_Cont_Status);
+
elsif Is_Warning_Msg or Is_Style_Msg then
Error_Msg_Internal
(Warn_Insertion & "in inlined body #",
Actual_Error_Loc, Flag_Location, Msg_Cont_Status);
+
else
Error_Msg_Internal
("error in inlined body #",
Error_Msg_Internal
("info: in instantiation #",
Actual_Error_Loc, Flag_Location, Msg_Cont_Status);
+
elsif Is_Warning_Msg or else Is_Style_Msg then
Error_Msg_Internal
(Warn_Insertion & "in instantiation #",
Actual_Error_Loc, Flag_Location, Msg_Cont_Status);
+
else
Error_Msg_Internal
("instantiation error #",
-- --
-- S p e c --
-- --
--- Copyright (C) 2006-2014, Free Software Foundation, Inc. --
+-- Copyright (C) 2006-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- --
-- Typ_TSD : constant Type_Specific_Data_Ptr
-- := Build_TSD (Address!(Typ_Tag));
-- Index : constant Integer := Obj_TSD.Idepth - Typ_TSD.Idepth
- -- Index > 0 and then Obj_TSD.Tags_Table (Index) = Typ'Tag
+ -- Index >= 0 and then Obj_TSD.Tags_Table (Index) = Typ'Tag
Insert_Action (Related_Nod,
Make_Object_Declaration (Loc,
Constant_Present => True,
Object_Definition => New_Occurrence_Of
(RTE (RE_Type_Specific_Data_Ptr), Loc),
- Expression => Build_TSD (Loc, New_Occurrence_Of (Tag_Addr, Loc))));
+ Expression => Build_TSD (Loc, New_Occurrence_Of (Tag_Addr, Loc))),
+ Suppress => All_Checks);
Insert_Action (Related_Nod,
Make_Object_Declaration (Loc,
(RTE (RE_Type_Specific_Data_Ptr), Loc),
Expression => Build_TSD (Loc,
Unchecked_Convert_To (RTE (RE_Address),
- Typ_Tag_Node))));
+ Typ_Tag_Node))),
+ Suppress => All_Checks);
Insert_Action (Related_Nod,
Make_Object_Declaration (Loc,
Prefix => New_Occurrence_Of (Typ_TSD, Loc),
Selector_Name =>
New_Occurrence_Of
- (RTE_Record_Component (RE_Idepth), Loc)))));
+ (RTE_Record_Component (RE_Idepth), Loc)))),
+ Suppress => All_Checks);
New_Node :=
Make_And_Then (Loc,
-- --
-- S p e c --
-- --
--- Copyright (C) 2006-2011, Free Software Foundation, Inc. --
+-- Copyright (C) 2006-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- --
-- computed in constant time by the formula:
--
-- Index := TSD (Obj'Tag).Idepth - TSD (Typ'Tag).Idepth;
- -- Index > 0 and then TSD (Obj'Tag).Tags_Table (Index) = Typ'Tag
+ -- Index >= 0 and then TSD (Obj'Tag).Tags_Table (Index) = Typ'Tag
--
-- Related_Nod is the node where the implicit declaration of variable Index
-- is inserted. Obj_Tag_Node is relocated.
if Tagged_Type_Expansion then
Tagged_Membership (N, SCIL_Node, New_N);
Rewrite (N, New_N);
- Analyze_And_Resolve (N, Restyp);
+ Analyze_And_Resolve
+ (N, Restyp, Suppress => All_Checks);
-- Update decoration of relocated node referenced by the
-- SCIL node.
Insert_Action (N,
Make_Raise_Constraint_Error (Loc,
Condition => Cond,
- Reason => CE_Tag_Check_Failed));
+ Reason => CE_Tag_Check_Failed),
+ Suppress => All_Checks);
end Make_Tag_Check;
-- Start of processing for Tagged_Conversion
begin
Enable :=
- Enable or else (Ekind (T) in Array_Kind
- and then Present (Packed_Array_Impl_Type (T)));
+ Enable
+ or else
+ (Ekind (T) in Array_Kind
+ and then Present (Packed_Array_Impl_Type (T)));
end Enable_If_Packed_Array;
----------------------
elsif Nkind (N) = N_Identifier
and then Scope_Contains (Scope (Entity (N)), Ent)
and then (Ekind (Entity (N)) = E_Constant
- or else Ekind (Entity (N)) = E_In_Parameter)
+ or else Ekind (Entity (N)) = E_In_Parameter)
then
Prepend_String_To_Buffer (Get_Name_String (Chars (Entity (N))));
-- Scope_Contains --
--------------------
- function Scope_Contains (Sc : Node_Id; Ent : Entity_Id) return Boolean
- is
+ function Scope_Contains (Sc : Node_Id; Ent : Entity_Id) return Boolean is
Cur : Node_Id := Scope (Ent);
+
begin
while Present (Cur) loop
if Cur = Sc then
return True;
end if;
+
Cur := Scope (Cur);
end loop;
+
return False;
end Scope_Contains;
-- Start of processing for Debug_Renaming_Declaration
begin
- if not Comes_From_Source (N)
- and then not Needs_Debug_Info (Ent)
- then
+ if not Comes_From_Source (N) and then not Needs_Debug_Info (Ent) then
return Empty;
end if;
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2013, 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- --
-- always the case).
-- In both these cases, Replace or Rewrite must be used to achieve the
--- of the node, since the Expander routine is only passed the Node_Id
--- of the node to be expanded, and the resulting expanded Node_Id must
--- be the same (the parameter to Expand is mode in, not mode in-out).
+-- expansion of the node, since the Expander routine is only passed the
+-- Node_Id of the node to be expanded, and the resulting expanded Node_Id
+-- must be the same (the parameter to Expand is mode in, not mode in-out).
-- For nodes other than subexpressions, it is not necessary to preserve the
-- original tree in the Expand routines, unlike the case for modifications
function Has_Internal_Extension (Fname : String) return Boolean;
pragma Inline (Has_Internal_Extension);
- -- True if the extension is appropriate for an internal/predefined
- -- unit. That means ".ads" or ".adb" for source files, and ".ali" for
- -- ALI files.
+ -- True if the extension is appropriate for an internal/predefined unit.
+ -- That means ".ads" or ".adb" for source files, and ".ali" for ALI files.
function Has_Prefix (X, Prefix : String) return Boolean;
pragma Inline (Has_Prefix);
-- True if Prefix is at the beginning of X. For example,
- -- Has_Prefix("a-filename.ads", Prefix => "a-") is True.
+ -- Has_Prefix ("a-filename.ads", Prefix => "a-") is True.
----------------------------
-- Has_Internal_Extension --
subtype Str8 is String (1 .. 8);
Renaming_Names : constant array (1 .. 8) of Str8 :=
- ("calendar", -- Calendar
- "machcode", -- Machine_Code
- "unchconv", -- Unchecked_Conversion
- "unchdeal", -- Unchecked_Deallocation
- "directio", -- Direct_IO
- "ioexcept", -- IO_Exceptions
- "sequenio", -- Sequential_IO
- "text_io."); -- Text_IO
+ ("calendar", -- Calendar
+ "machcode", -- Machine_Code
+ "unchconv", -- Unchecked_Conversion
+ "unchdeal", -- Unchecked_Deallocation
+ "directio", -- Direct_IO
+ "ioexcept", -- IO_Exceptions
+ "sequenio", -- Sequential_IO
+ "text_io."); -- Text_IO
-- Note: the implementation is optimized to perform uniform comparisons
-- on string slices whose length is known at compile time and at most 8
-- default value appropriate to the system (in Osint.Initialize), and then
-- reset if a command line switch is used to change the setting.
- Ignore_Pragma_SPARK_Mode : Boolean := False;
- -- GNAT
- -- Set True to ignore the semantics and effects of pragma SPARK_Mode when
- -- the pragma appears inside an instance whose enclosing context is subject
- -- to SPARK_Mode "off".
-
Ignore_Rep_Clauses : Boolean := False;
-- GNAT
-- Set True to ignore all representation clauses. Useful when compiling
-- code from foreign compilers for checking or ASIS purposes. Can be
-- set True by use of -gnatI.
+ Ignore_SPARK_Mode_Pragmas_In_Instance : Boolean := False;
+ -- GNAT
+ -- Set True to ignore the semantics and effects of pragma SPARK_Mode when
+ -- the pragma appears inside an instance whose enclosing context is subject
+ -- to SPARK_Mode "off". This property applies to nested instances.
+
Ignore_Style_Checks_Pragmas : Boolean := False;
-- GNAT
-- Set True to ignore all Style_Checks pragmas. Can be set True by use
end if;
end loop;
- -- Cover the odd situtation if someone decides to change
- -- Parameters.Max_Task_Image_Length to less than 16 characters
+ -- Cover the odd situation where someone decides to change
+ -- Parameters.Max_Task_Image_Length to less than 16 characters.
if Len > Parameters.Max_Task_Image_Length then
Len := Parameters.Max_Task_Image_Length;
------------------
-- For certain kind of expressions, such as aggregates, we need to defer
--- expansion of the aggregate and its inner expressions after the whole
+-- expansion of the aggregate and its inner expressions until after the whole
-- set of expressions appearing inside the aggregate have been analyzed.
-- Consider, for instance the following example:
--
-- repeatedly (for instance in the above aggregate "new Thing (Function_Call)"
-- needs to be called 100 times.)
--- The reason why this mechanism does not work is that the expanded code for
--- the children is typically inserted above the parent and thus when the
--- father gets expanded no re-evaluation takes place. For instance in the case
--- of aggregates if "new Thing (Function_Call)" is expanded before of the
--- aggregate the expanded code will be placed outside of the aggregate and
--- when expanding the aggregate the loop from 1 to 100 will not surround the
+-- The reason this mechanism does not work is that the expanded code for the
+-- children is typically inserted above the parent and thus when the father
+-- gets expanded no re-evaluation takes place. For instance in the case of
+-- aggregates if "new Thing (Function_Call)" is expanded before the aggregate
+-- the expanded code will be placed outside of the aggregate and when
+-- expanding the aggregate the loop from 1 to 100 will not surround the
-- expanded code for "new Thing (Function_Call)".
--- To remedy this situation we introduce a new flag which signals whether we
--- want a full analysis (i.e. expansion is enabled) or a pre-analysis which
--- performs Analysis and Resolution but no expansion.
+-- To remedy this situation we introduce a flag that signals whether we want a
+-- full analysis (i.e. expansion is enabled) or a pre-analysis which performs
+-- Analysis and Resolution but no expansion.
-- After the complete pre-analysis of an expression has been carried out we
-- can transform the expression and then carry out the full three stage
-- Local variables
- Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
- -- Save flag Ignore_Pragma_SPARK_Mode for restore on exit
+ Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
+ -- Save flag Ignore_SPARK_Mode_Pragmas_In_Instance for restore on exit
Associations : Boolean := True;
New_N : Node_Id;
-- all SPARK_Mode pragmas within the generic_package_name.
if SPARK_Mode /= On then
- Ignore_Pragma_SPARK_Mode := True;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := True;
+
+ -- Mark the formal spec in case the body is instantiated at a later
+ -- pass. This preserves the original context in effect for the body.
+
+ Set_Ignore_SPARK_Mode_Pragmas (Formal);
end if;
Analyze (Specification (N));
Analyze_Aspect_Specifications (N, Pack_Id);
end if;
- Ignore_Pragma_SPARK_Mode := Save_IPSM;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
end Analyze_Formal_Package_Declaration;
---------------------------------
Inline_Now : Boolean := False;
Has_Inline_Always : Boolean := False;
- Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
- -- Save flag Ignore_Pragma_SPARK_Mode for restore on exit
+ Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
+ -- Save flag Ignore_SPARK_Mode_Pragmas_In_Instance for restore on exit
Save_SM : constant SPARK_Mode_Type := SPARK_Mode;
Save_SMP : constant Node_Id := SPARK_Mode_Pragma;
-- the instance.
if SPARK_Mode /= On then
- Ignore_Pragma_SPARK_Mode := True;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := True;
+
+ -- Mark the instance spec in case the body is instantiated at a
+ -- later pass. This preserves the original context in effect for
+ -- the body.
+
+ Set_Ignore_SPARK_Mode_Pragmas (Act_Decl_Id);
end if;
Gen_Decl := Unit_Declaration_Node (Gen_Unit);
Set_Defining_Identifier (N, Act_Decl_Id);
end if;
- Ignore_Pragma_SPARK_Mode := Save_IPSM;
- SPARK_Mode := Save_SM;
- SPARK_Mode_Pragma := Save_SMP;
- Style_Check := Save_Style_Check;
-
-- Check that if N is an instantiation of System.Dim_Float_IO or
-- System.Dim_Integer_IO, the formal type has a dimension system.
Analyze_Aspect_Specifications (N, Act_Decl_Id);
end if;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
+ SPARK_Mode := Save_SM;
+ SPARK_Mode_Pragma := Save_SMP;
+ Style_Check := Save_Style_Check;
+
if Mode_Set then
Restore_Ghost_Mode (Mode);
end if;
Restore_Env;
end if;
- Ignore_Pragma_SPARK_Mode := Save_IPSM;
- SPARK_Mode := Save_SM;
- SPARK_Mode_Pragma := Save_SMP;
- Style_Check := Save_Style_Check;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
+ SPARK_Mode := Save_SM;
+ SPARK_Mode_Pragma := Save_SMP;
+ Style_Check := Save_Style_Check;
if Mode_Set then
Restore_Ghost_Mode (Mode);
-- Local variables
- Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
- -- Save flag Ignore_Pragma_SPARK_Mode for restore on exit
+ Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
+ -- Save flag Ignore_SPARK_Mode_Pragmas_In_Instance for restore on exit
Save_SM : constant SPARK_Mode_Type := SPARK_Mode;
Save_SMP : constant Node_Id := SPARK_Mode_Pragma;
Error_Msg_NE ("instantiation of & within itself", N, Gen_Unit);
else
- -- If the context of the instance is subject to SPARK_Mode "off" or
- -- the annotation is altogether missing, set the global flag which
- -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
- -- the instance.
-
- if SPARK_Mode /= On then
- Ignore_Pragma_SPARK_Mode := True;
- end if;
-
Set_Entity (Gen_Id, Gen_Unit);
Set_Is_Instantiated (Gen_Unit);
Set_Has_Pragma_Inline_Always
(Anon_Id, Has_Pragma_Inline_Always (Gen_Unit));
+ -- If the context of the instance is subject to SPARK_Mode "off" or
+ -- the annotation is altogether missing, set the global flag which
+ -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
+ -- the instance.
+
+ if SPARK_Mode /= On then
+ Ignore_SPARK_Mode_Pragmas_In_Instance := True;
+
+ -- Mark both the instance spec and the anonymous package in case
+ -- the body is instantiated at a later pass. This preserves the
+ -- original context in effect for the body.
+
+ Set_Ignore_SPARK_Mode_Pragmas (Act_Decl_Id);
+ Set_Ignore_SPARK_Mode_Pragmas (Anon_Id);
+ end if;
+
if not Is_Intrinsic_Subprogram (Gen_Unit) then
Check_Elab_Instantiation (N);
end if;
Env_Installed := False;
Generic_Renamings.Set_Last (0);
Generic_Renamings_HTable.Reset;
-
- Ignore_Pragma_SPARK_Mode := Save_IPSM;
- SPARK_Mode := Save_SM;
- SPARK_Mode_Pragma := Save_SMP;
end if;
<<Leave>>
Analyze_Aspect_Specifications (N, Act_Decl_Id);
end if;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
+ SPARK_Mode := Save_SM;
+ SPARK_Mode_Pragma := Save_SMP;
+
if Mode_Set then
Restore_Ghost_Mode (Mode);
end if;
Restore_Env;
end if;
- Ignore_Pragma_SPARK_Mode := Save_IPSM;
- SPARK_Mode := Save_SM;
- SPARK_Mode_Pragma := Save_SMP;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
+ SPARK_Mode := Save_SM;
+ SPARK_Mode_Pragma := Save_SMP;
if Mode_Set then
Restore_Ghost_Mode (Mode);
Gen_Decl : constant Node_Id := Unit_Declaration_Node (Gen_Unit);
Loc : constant Source_Ptr := Sloc (Inst_Node);
- Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
+ Save_ISMP : constant Boolean :=
+ Ignore_SPARK_Mode_Pragmas_In_Instance;
Save_Style_Check : constant Boolean := Style_Check;
procedure Check_Initialized_Types;
Save_Env (Gen_Unit, Act_Decl_Id);
Style_Check := False;
- -- If the context of the instance is subject to SPARK_Mode "off" or
- -- the annotation is altogether missing, set the global flag which
- -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
- -- the instance.
+ -- If the context of the instance is subject to SPARK_Mode "off", the
+ -- annotation is missing, or the body is instantiated at a later pass
+ -- and its spec ignored SPARK_Mode pragma, set the global flag which
+ -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within the
+ -- instance.
- if SPARK_Mode /= On then
- Ignore_Pragma_SPARK_Mode := True;
+ if SPARK_Mode /= On
+ or else Ignore_SPARK_Mode_Pragmas (Act_Decl_Id)
+ then
+ Ignore_SPARK_Mode_Pragmas_In_Instance := True;
end if;
Current_Sem_Unit := Body_Info.Current_Sem_Unit;
end if;
Restore_Env;
- Ignore_Pragma_SPARK_Mode := Save_IPSM;
- Style_Check := Save_Style_Check;
-- If we have no body, and the unit requires a body, then complain. This
-- complaint is suppressed if we have detected other errors (since a
-- was already detected, since this can cause blowups.
else
- return;
+ goto Leave;
end if;
-- Case of package that does not need a body
Expander_Mode_Restore;
<<Leave>>
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
+ Style_Check := Save_Style_Check;
+
Restore_Ghost_Mode (Mode);
end Instantiate_Package_Body;
Pack_Id : constant Entity_Id :=
Defining_Unit_Name (Parent (Act_Decl));
- Saved_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
- Saved_Style_Check : constant Boolean := Style_Check;
+ Saved_ISMP : constant Boolean :=
+ Ignore_SPARK_Mode_Pragmas_In_Instance;
+ Saved_Style_Check : constant Boolean := Style_Check;
Saved_Warnings : constant Warning_Record := Save_Warnings;
Act_Body : Node_Id;
Save_Env (Gen_Unit, Act_Decl_Id);
Style_Check := False;
- -- If the context of the instance is subject to SPARK_Mode "off" or
- -- the annotation is altogether missing, set the global flag which
- -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
- -- the instance.
+ -- If the context of the instance is subject to SPARK_Mode "off", the
+ -- annotation is missing, or the body is instantiated at a later pass
+ -- and its spec ignored SPARK_Mode pragma, set the global flag which
+ -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within the
+ -- instance.
- if SPARK_Mode /= On then
- Ignore_Pragma_SPARK_Mode := True;
+ if SPARK_Mode /= On
+ or else Ignore_SPARK_Mode_Pragmas (Act_Decl_Id)
+ then
+ Ignore_SPARK_Mode_Pragmas_In_Instance := True;
end if;
Current_Sem_Unit := Body_Info.Current_Sem_Unit;
end if;
Restore_Env;
- Ignore_Pragma_SPARK_Mode := Saved_IPSM;
- Style_Check := Saved_Style_Check;
Restore_Warnings (Saved_Warnings);
-- Body not found. Error was emitted already. If there were no previous
Expander_Mode_Restore;
<<Leave>>
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
+ Style_Check := Saved_Style_Check;
+
Restore_Ghost_Mode (Mode);
end Instantiate_Subprogram_Body;
Analyzed_Formal : Node_Id;
Actual_Decls : List_Id) return List_Id
is
- Gen_T : constant Entity_Id := Defining_Identifier (Formal);
A_Gen_T : constant Entity_Id :=
Defining_Identifier (Analyzed_Formal);
- Ancestor : Entity_Id := Empty;
Def : constant Node_Id := Formal_Type_Definition (Formal);
+ Gen_T : constant Entity_Id := Defining_Identifier (Formal);
Act_T : Entity_Id;
+ Ancestor : Entity_Id := Empty;
Decl_Node : Node_Id;
Decl_Nodes : List_Id;
Loc : Source_Ptr;
-- Local variables
- Mode : Ghost_Mode_Type;
- Mode_Set : Boolean := False;
+ Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
+ Mode : Ghost_Mode_Type;
+ Mode_Set : Boolean := False;
-- Start of processing for Analyze_Subprogram_Body_Helper
else
Enter_Name (Body_Id);
- return;
+ goto Leave;
end if;
-- Non-generic case, find the subprogram declaration, if one was seen,
-- analysis.
elsif Prev_Id = Body_Id and then Has_Completion (Body_Id) then
- return;
+ goto Leave;
else
Body_Id := Analyze_Subprogram_Specification (Body_Spec);
Set_SPARK_Pragma_Inherited (Body_Id);
end if;
+ -- A subprogram body may be instantiated or inlined at a later pass.
+ -- Restore the state of Ignore_SPARK_Mode_Pragmas_In_Instance when it
+ -- applied to the initial declaration of the body.
+
+ if Present (Spec_Id) then
+ if Ignore_SPARK_Mode_Pragmas (Spec_Id) then
+ Ignore_SPARK_Mode_Pragmas_In_Instance := True;
+ end if;
+
+ else
+ -- Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in
+ -- case the body is instantiated or inlined later and out of context.
+ -- The body uses this attribute to restore the value of the global
+ -- flag.
+
+ if Ignore_SPARK_Mode_Pragmas_In_Instance then
+ Set_Ignore_SPARK_Mode_Pragmas (Body_Id);
+
+ elsif Ignore_SPARK_Mode_Pragmas (Body_Id) then
+ Ignore_SPARK_Mode_Pragmas_In_Instance := True;
+ end if;
+ end if;
+
-- If this is the proper body of a stub, we must verify that the stub
-- conforms to the body, and to the previous spec if one was present.
-- We know already that the body conforms to that spec. This test is
Protected_Body_Subprogram (Spec_Id);
Prot_Ext_Formal : Entity_Id := Extra_Formals (Spec_Id);
Impl_Ext_Formal : Entity_Id := Extra_Formals (Impl_Subp);
+
begin
while Present (Prot_Ext_Formal) loop
pragma Assert (Present (Impl_Ext_Formal));
end if;
<<Leave>>
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
+
if Mode_Set then
Restore_Ghost_Mode (Mode);
end if;
Set_SPARK_Pragma_Inherited (Designator);
end if;
+ -- Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in case
+ -- the body of this subprogram is instantiated or inlined later and out
+ -- of context. The body uses this attribute to restore the value of the
+ -- global flag.
+
+ if Ignore_SPARK_Mode_Pragmas_In_Instance then
+ Set_Ignore_SPARK_Mode_Pragmas (Designator);
+ end if;
+
if Debug_Flag_C then
Write_Str ("==> subprogram spec ");
Write_Name (Chars (Designator));
-- Local variables
+ Save_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance;
+
Body_Id : Entity_Id;
HSS : Node_Id;
Last_Spec_Entity : Entity_Id;
Set_SPARK_Aux_Pragma (Body_Id, SPARK_Mode_Pragma);
Set_SPARK_Pragma_Inherited (Body_Id);
Set_SPARK_Aux_Pragma_Inherited (Body_Id);
+
+ -- A package body may be instantiated or inlined at a later pass.
+ -- Restore the state of Ignore_SPARK_Mode_Pragmas_In_Instance when
+ -- it applied to the package spec.
+
+ if Ignore_SPARK_Mode_Pragmas (Spec_Id) then
+ Ignore_SPARK_Mode_Pragmas_In_Instance := True;
+ end if;
end if;
Set_Categorization_From_Pragmas (N);
end if;
end if;
+ Ignore_SPARK_Mode_Pragmas_In_Instance := Save_ISMP;
+
Restore_Ghost_Mode (Mode);
end Analyze_Package_Body_Helper;
Set_SPARK_Aux_Pragma (Id, SPARK_Mode_Pragma);
Set_SPARK_Pragma_Inherited (Id);
Set_SPARK_Aux_Pragma_Inherited (Id);
+
+ -- Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in
+ -- case the body of this package is instantiated or inlined later and
+ -- out of context. The body uses this attribute to restore the value
+ -- of the global flag.
+
+ if Ignore_SPARK_Mode_Pragmas_In_Instance then
+ Set_Ignore_SPARK_Mode_Pragmas (Id);
+ end if;
end if;
-- Analyze aspect specifications immediately, since we need to recognize
-- enclosing context has SPARK_Mode set to "off", the pragma has
-- no semantic effect.
- if Ignore_Pragma_SPARK_Mode then
+ if Ignore_SPARK_Mode_Pragmas_In_Instance then
Rewrite (N, Make_Null_Statement (Loc));
Analyze (N);
return;
-----------------------
function SPARK_Mode_Is_Off (N : Node_Id) return Boolean is
- Prag : constant Node_Id := SPARK_Pragma (Defining_Entity (N));
+ Id : constant Entity_Id := Defining_Entity (N);
+ Prag : constant Node_Id := SPARK_Pragma (Id);
begin
- return
- Present (Prag) and then Get_SPARK_Mode_From_Annotation (Prag) = Off;
+ -- Default the mode to "off" when the context is an instance and all
+ -- SPARK_Mode pragmas found within are to be ignored.
+
+ if Ignore_SPARK_Mode_Pragmas (Id) then
+ return True;
+
+ else
+ return
+ Present (Prag)
+ and then Get_SPARK_Mode_From_Annotation (Prag) = Off;
+ end if;
end SPARK_Mode_Is_Off;
-- Start of processing for Check_State_Refinements
projects / gcc.git / commitdiff