+2014-08-04 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * a-cfhama.adb, a-cfhase.adb, a-cforma.adb, a-cforse.adb Add
+ SPARK_Mode in the body.
+ * sem_ch7.adb (Analyze_Package_Body_Helper): Restore the original
+ way to verify the consistency of SPARK_Mode between a spec and
+ a body.
+ * sem_ch12.adb (Analyze_Package_Instantiation): Remove the call
+ to Set_Ignore_Pragma_SPARK_Mode. Set flag Ignore_Pragma_SPARK_Mode
+ manually.
+ (Analyze_Subprogram_Instantiation): Remove the call to
+ Set_Ignore_Pragma_SPARK_Mode. Set flag Ignore_Pragma_SPARK_Mode
+ manually.
+ * sem_prag.adb (Analyze_Pragma): Remove local variable
+ Inst_Id. SPARK_Mode can no longer be applied to a package or
+ subprogram instantiation.
+ * sem_util.adb, sem_util.ads (Set_Ignore_Pragma_SPARK_Mode):
+ Removed.
+
2014-08-04 Robert Dewar <dewar@adacore.com>
* sem_prag.adb, osint.adb, osint.ads: Minor reformatting.
with Ada.Containers.Prime_Numbers; use Ada.Containers.Prime_Numbers;
-with System; use type System.Address;
+with System; use type System.Address;
package body Ada.Containers.Formal_Hashed_Maps is
+ pragma SPARK_Mode (Off);
-----------------------
-- Local Subprograms --
-- --
-- B o d y --
-- --
--- Copyright (C) 2010-2013, Free Software Foundation, Inc. --
+-- Copyright (C) 2010-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- --
with System; use type System.Address;
package body Ada.Containers.Formal_Hashed_Sets is
+ pragma SPARK_Mode (Off);
-----------------------
-- Local Subprograms --
-- --
-- B o d y --
-- --
--- Copyright (C) 2010-2013, Free Software Foundation, Inc. --
+-- Copyright (C) 2010-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- --
with System; use type System.Address;
package body Ada.Containers.Formal_Ordered_Maps is
+ pragma SPARK_Mode (Off);
-----------------------------
-- Node Access Subprograms --
pragma Elaborate_All
(Ada.Containers.Red_Black_Trees.Generic_Bounded_Set_Operations);
-with System; use type System.Address;
+with System; use type System.Address;
package body Ada.Containers.Formal_Ordered_Sets is
+ pragma SPARK_Mode (Off);
------------------------------
-- Access to Fields of Node --
goto Leave;
else
- -- If the instance or its context is subject to SPARK_Mode "off",
+ -- If the context of the instance is subject to SPARK_Mode "off",
-- set the global flag which signals Analyze_Pragma to ignore all
-- SPARK_Mode pragmas within the instance.
- Set_Ignore_Pragma_SPARK_Mode (N);
+ if SPARK_Mode = Off then
+ Ignore_Pragma_SPARK_Mode := True;
+ end if;
Gen_Decl := Unit_Declaration_Node (Gen_Unit);
Error_Msg_NE ("instantiation of & within itself", N, Gen_Unit);
else
- -- If the instance or its context is subject to SPARK_Mode "off",
+ -- If the context of the instance is subject to SPARK_Mode "off",
-- set the global flag which signals Analyze_Pragma to ignore all
-- SPARK_Mode pragmas within the instance.
- Set_Ignore_Pragma_SPARK_Mode (N);
+ if SPARK_Mode = Off then
+ Ignore_Pragma_SPARK_Mode := True;
+ end if;
Set_Entity (Gen_Id, Gen_Unit);
Set_Is_Instantiated (Gen_Unit);
-- Verify that the SPARK_Mode of the body agrees with that of its spec
if Present (SPARK_Pragma (Body_Id)) then
- if Present (SPARK_Pragma (Spec_Id)) then
- if Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) = Off
+ if Present (SPARK_Aux_Pragma (Spec_Id)) then
+ if Get_SPARK_Mode_From_Pragma (SPARK_Aux_Pragma (Spec_Id)) = Off
and then
Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) = On
then
Body_Id : Entity_Id;
Context : Node_Id;
- Inst_Id : Entity_Id;
Mode : Name_Id;
Mode_Id : SPARK_Mode_Type;
Spec_Id : Entity_Id;
Mode_Id := Get_SPARK_Mode_Type (Mode);
Context := Parent (N);
- -- Handle a compilation unit with configuration pragmas
-
- if Nkind (Context) = N_Compilation_Unit_Aux then
- Context := Parent (Context);
- end if;
-
-- The pragma appears in a configuration pragmas file
if No (Context) then
SPARK_Mode_Pragma := N;
SPARK_Mode := Mode_Id;
- -- The pragma applies to a compilation unit
-
- elsif Nkind (Context) = N_Compilation_Unit then
-
- -- The pragma acts as a configuration pragma
-
- -- pragma SPARK_Mode ...;
- -- package Pack is ...;
-
- if List_Containing (N) = Context_Items (Context) then
- Check_Valid_Configuration_Pragma;
- SPARK_Mode_Pragma := N;
- SPARK_Mode := Mode_Id;
-
- -- The pragma applies to a package instantiation that acts as a
- -- compilation unit.
-
- -- package Inst is new Gen ...;
- -- pragma SPARK_Mode ...;
-
- elsif Nkind (Unit (Context)) = N_Package_Instantiation then
- Inst_Id := Defining_Entity (Instance_Spec (Unit (Context)));
- Check_Library_Level_Entity (Inst_Id);
- Check_Pragma_Conformance
- (Context_Pragma => SPARK_Mode_Pragma,
- Entity_Pragma => Empty,
- Entity => Empty);
-
- Set_SPARK_Pragma (Inst_Id, N);
- Set_SPARK_Pragma_Inherited (Inst_Id, False);
-
- -- Otherwise the pragma applies to a subprogram instantiation
- -- that acts as a compilation unit.
-
- else
- Spec_Id := Defining_Entity (Unit (Context));
- Check_Library_Level_Entity (Spec_Id);
- Check_Pragma_Conformance
- (Context_Pragma => SPARK_Mode_Pragma,
- Entity_Pragma => Empty,
- Entity => Empty);
+ -- The pragma acts as a configuration pragma in a compilation unit
- Set_SPARK_Pragma (Spec_Id, N);
- Set_SPARK_Pragma_Inherited (Spec_Id, False);
+ -- pragma SPARK_Mode ...;
+ -- package Pack is ...;
- if Ekind (Spec_Id) = E_Package
- and then Present (Related_Instance (Spec_Id))
- then
- Inst_Id := Related_Instance (Spec_Id);
- Set_SPARK_Pragma (Inst_Id, N);
- Set_SPARK_Pragma_Inherited (Inst_Id, False);
- end if;
- end if;
+ elsif Nkind (Context) = N_Compilation_Unit
+ and then List_Containing (N) = Context_Items (Context)
+ then
+ Check_Valid_Configuration_Pragma;
+ SPARK_Mode_Pragma := N;
+ SPARK_Mode := Mode_Id;
-- Otherwise the placement of the pragma within the tree dictates
-- its associated construct. Inspect the declarative list where
raise Pragma_Exit;
end if;
- -- Skip internally generated code, but consider subprogram
- -- instantiations housed within their wrapper packages.
+ -- Skip internally generated code
- elsif not Comes_From_Source (Stmt)
- and then
- (Nkind (Stmt) /= N_Subprogram_Declaration
- or else No (Generic_Parent (Specification (Stmt))))
- then
+ elsif not Comes_From_Source (Stmt) then
null;
- -- The pragma is associated with a package or subprogram
- -- instantiation that does not act as a compilation unit.
-
- -- package Inst is new Gen ...;
- -- pragma SPARK_Mode ...;
-
- elsif Nkind_In (Stmt, N_Function_Instantiation,
- N_Package_Instantiation,
- N_Procedure_Instantiation)
- then
- Inst_Id := Defining_Entity (Instance_Spec (Stmt));
- Check_Library_Level_Entity (Inst_Id);
- Check_Pragma_Conformance
- (Context_Pragma => SPARK_Mode_Pragma,
- Entity_Pragma => Empty,
- Entity => Empty);
-
- Set_SPARK_Pragma (Inst_Id, N);
- Set_SPARK_Pragma_Inherited (Inst_Id, False);
- return;
-
-- The pragma applies to a [generic] subprogram declaration
-- [generic]
Prev (Stmt);
end loop;
+ -- The pragma applies to a package or a subprogram that acts as
+ -- a compilation unit.
+
+ -- procedure Proc ...;
+ -- pragma SPARK_Mode ...;
+
+ if Nkind (Context) = N_Compilation_Unit_Aux then
+ Context := Unit (Parent (Context));
+ end if;
+
-- The pragma appears within package declarations
if Nkind (Context) = N_Package_Specification then
Set_SPARK_Aux_Pragma (Body_Id, N);
Set_SPARK_Aux_Pragma_Inherited (Body_Id, False);
+ -- The pragma appeared as an aspect of a [generic] subprogram
+ -- declaration that acts as a compilation unit.
+
+ -- [generic]
+ -- procedure Proc ...;
+ -- pragma SPARK_Mode ...;
+
+ elsif Nkind_In (Context, N_Generic_Subprogram_Declaration,
+ N_Subprogram_Declaration)
+ then
+ Spec_Id := Defining_Entity (Context);
+ Check_Library_Level_Entity (Spec_Id);
+ Check_Pragma_Conformance
+ (Context_Pragma => SPARK_Pragma (Spec_Id),
+ Entity_Pragma => Empty,
+ Entity => Empty);
+
+ Set_SPARK_Pragma (Spec_Id, N);
+ Set_SPARK_Pragma_Inherited (Spec_Id, False);
+
-- The pragma appears at the top of subprogram body
-- declarations.
Set_Entity (N, Val);
end Set_Entity_With_Checks;
- ----------------------------------
- -- Set_Ignore_Pragma_SPARK_Mode --
- ----------------------------------
-
- procedure Set_Ignore_Pragma_SPARK_Mode (N : Node_Id) is
- procedure Set_SPARK_Mode (Expr : Node_Id);
- -- Set flag Ignore_Pragma_SPARK_Mode based on the argument of aspect or
- -- pragma SPARK_Mode denoted by Expr.
-
- --------------------
- -- Set_SPARK_Mode --
- --------------------
-
- procedure Set_SPARK_Mode (Expr : Node_Id) is
- begin
- -- When pragma SPARK_Mode with argument "off" applies to an instance,
- -- all SPARK_Mode pragmas within the instance are ignored.
-
- if Present (Expr)
- and then Nkind (Expr) = N_Identifier
- and then Chars (Expr) = Name_Off
- then
- Ignore_Pragma_SPARK_Mode := True;
- end if;
- end Set_SPARK_Mode;
-
- -- Local variables
-
- Aspects : constant List_Id := Aspect_Specifications (N);
- Context : constant Node_Id := Parent (N);
- Args : List_Id;
- Aspect : Node_Id;
- Decl : Node_Id;
-
- -- Start of processing for Set_Ignore_Pragma_SPARK_Mode
-
- begin
- -- When the enclosing context of the instance has SPARK_Mode "off", all
- -- SPARK_Mode pragmas within the instance are ignored. Note that there
- -- is no point in checking whether the instantiation itself carries
- -- aspect/pragma SPARK_Mode because it is either illegal ("on") or has
- -- no effect ("off").
-
- if SPARK_Mode = Off then
- Ignore_Pragma_SPARK_Mode := True;
- return;
- end if;
-
- -- Inspect the aspects of the instantiation and locate SPARK_Mode. Note
- -- that the aspect form of SPARK_Mode precedes a potentially duplicate
- -- pragma.
-
- if Present (Aspects) then
- Aspect := First (Aspects);
- while Present (Aspect) loop
- if Get_Aspect_Id (Aspect) = Aspect_SPARK_Mode then
- Set_SPARK_Mode (Expression (Aspect));
- return;
- end if;
-
- Next (Aspect);
- end loop;
- end if;
-
- -- Peek ahead of the instance and locate pragma SPARK_Mode. Even though
- -- the pragma is analyzed after the instance, its mode must be known now
- -- as it governs the legality of SPARK_Mode pragmas within the instance.
-
- Decl := Empty;
-
- -- The instance is a compilation unit, the pragma appears on the
- -- Pragmas_After list.
-
- if Present (Context)
- and then Nkind (Context) = N_Compilation_Unit
- and then Present (Aux_Decls_Node (Context))
- and then Present (Pragmas_After (Aux_Decls_Node (Context)))
- then
- Decl := First (Pragmas_After (Aux_Decls_Node (Context)));
-
- -- The instance is part of a declarative list, the pragma appears after
- -- the instance.
-
- elsif Is_List_Member (N) then
- Decl := Next (N);
- end if;
-
- -- Inspect all declarations following the instance
-
- while Present (Decl) loop
- if Nkind (Decl) = N_Pragma then
- if Get_Pragma_Id (Decl) = Pragma_SPARK_Mode then
- Args := Pragma_Argument_Associations (Decl);
-
- -- The pragma argument dictates the mode
-
- if Present (Args) then
- Set_SPARK_Mode (Get_Pragma_Arg (First (Args)));
- end if;
-
- -- Only the first SPARK_Mode following the instance is
- -- considered, any extra (illegal) pragmas are ignored.
-
- exit;
- end if;
-
- -- Skip internally generated code
-
- elsif not Comes_From_Source (Decl) then
- null;
-
- -- Otherwise a source construct exhaust the range where the pragma
- -- may appear.
-
- else
- exit;
- end if;
-
- Next (Decl);
- end loop;
- end Set_Ignore_Pragma_SPARK_Mode;
-
------------------------
-- Set_Name_Entity_Id --
------------------------
-- If restriction No_Implementation_Identifiers is set, then it checks
-- that the entity is not implementation defined.
- procedure Set_Ignore_Pragma_SPARK_Mode (N : Node_Id);
- -- Determine whether [the enclosing context of] package or subprogram N is
- -- subject to pragma SPARK_Mode with mode "off". If this is the case, set
- -- global flag Ignore_Pragma_SPARK_Mode to True.
-
procedure Set_Name_Entity_Id (Id : Name_Id; Val : Entity_Id);
pragma Inline (Set_Name_Entity_Id);
-- Sets the Entity_Id value associated with the given name, which is the
projects / thirdparty / gcc.git / commitdiff
