Skip to content

R
riscv-gcc-1
Commit df910722 by Hristian Kirtchev Committed by Arnaud Charlet
Options

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.

From-SVN: r213578
parent 4ff2b6dc
Showing with 78 additions and 223 deletions
gcc/ada/ChangeLog
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.
......
gcc/ada/a-cfhama.adb
......@@ -33,9 +33,10 @@ pragma Elaborate_All (Ada.Containers.Hash_Tables.Generic_Bounded_Keys);
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 --
......
gcc/ada/a-cfhase.adb
......@@ -6,7 +6,7 @@
-- --
-- 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- --
......@@ -36,6 +36,7 @@ with Ada.Containers.Prime_Numbers; use Ada.Containers.Prime_Numbers;
with System; use type System.Address;
package body Ada.Containers.Formal_Hashed_Sets is
pragma SPARK_Mode (Off);
-----------------------
-- Local Subprograms --
......
gcc/ada/a-cforma.adb
......@@ -6,7 +6,7 @@
-- --
-- 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- --
......@@ -35,6 +35,7 @@ pragma Elaborate_All (Ada.Containers.Red_Black_Trees.Generic_Bounded_Keys);
with System; use type System.Address;
package body Ada.Containers.Formal_Ordered_Maps is
pragma SPARK_Mode (Off);
-----------------------------
-- Node Access Subprograms --
......
gcc/ada/a-cforse.adb
......@@ -36,9 +36,10 @@ with Ada.Containers.Red_Black_Trees.Generic_Bounded_Set_Operations;
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 --
......
gcc/ada/sem_ch12.adb
......@@ -3739,11 +3739,13 @@ package body Sem_Ch12 is
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);
......@@ -4914,11 +4916,13 @@ package body Sem_Ch12 is
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);
......
gcc/ada/sem_ch7.adb
......@@ -440,8 +440,8 @@ package body Sem_Ch7 is
-- 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
......
gcc/ada/sem_prag.adb
......@@ -19226,7 +19226,6 @@ package body Sem_Prag is
Body_Id : Entity_Id;
Context : Node_Id;
Inst_Id : Entity_Id;
Mode : Name_Id;
Mode_Id : SPARK_Mode_Type;
Spec_Id : Entity_Id;
......@@ -19261,12 +19260,6 @@ package body Sem_Prag is
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
......@@ -19281,59 +19274,17 @@ package body Sem_Prag is
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
......@@ -19353,37 +19304,11 @@ package body Sem_Prag is
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]
......@@ -19416,6 +19341,16 @@ package body Sem_Prag is
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
......@@ -19502,6 +19437,26 @@ package body Sem_Prag is
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.
......
gcc/ada/sem_util.adb
......@@ -16456,128 +16456,6 @@ package body Sem_Util is
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 --
------------------------
......
gcc/ada/sem_util.ads
......@@ -1837,11 +1837,6 @@ package Sem_Util is
-- 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
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment