+2013-07-05 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * aspects.adb: Add an entry for SPARK_Mode in table Canonical_Aspect.
+ * aspects.ads: Add an entry for SPARK_Mode in tables Aspect_Id,
+ Aspect_Argument, Aspect_Names.
+ * atree.adb (Node32): New routine.
+ (Set_Node32): New routine.
+ * atree.ads (Node32): New routine.
+ (Set_Node32): New routine.
+ * einfo.adb: Node32 is now used as SPARK_Mode_Pragmas.
+ (Set_SPARK_Mode_Pragmas): New routine.
+ (SPARK_Mode_Pragmas): New routine.
+ (Write_Field32_Name): Add and entry for SPARK_Modes.
+ * einfo.ads: Add attribute SPARK_Mode_Pragmas along with usage
+ in various entities.
+ (Set_SPARK_Mode_Pragmas): New routine and
+ pragma Inline.
+ (SPARK_Mode_Pragmas): New routine and pragma Inline.
+ * gnat_rm.texi: Add sections explaining the syntax and semantics
+ of aspect/pragma SPARK_Mode.
+ * gnat_ugn.texi: Add pragma SPARK_Mode to the list of
+ configuration pragmas.
+ * lib.adb (Set_SPARK_Mode_Pragma): New routine.
+ (SPARK_Mode_Pragma): New routine.
+ * lib.ads: Alphabetize the comments on fields of record
+ Unit_Record. Add new field SPARK_Mode_Pragma along with
+ comment on its usage. Update the layout of record Unit_Record.
+ (Set_SPARK_Mode_Pragma): New routine and pragma Inline.
+ (SPARK_Mode_Pragma): New routine and pragma Inline.
+ * lib-load.adb (Create_Dummy_Package_Unit): Initialize
+ field SPARK_Mode_Pragma.
+ (Load_Main_Source): Initialize field SPARK_Mode_Pragma.
+ (Load_Unit): Initialize field SPARK_Mode_Pragma.
+ * lib-writ.adb (Add_Preprocessing_Dependency): Initialize field
+ SPARK_Mode_Pragma.
+ (Ensure_System_Dependency): Initialize field SPARK_Mode_Pragma.
+ * opt.ads: Alphabetize verification flags. Store the
+ compilation-wide SPARK mode in variable Global_SPARK_Mode.
+ * par-prag.adb: Pragma SPARK_Mode does not need special processing
+ by the parser.
+ * sem_ch13.adb (Analyze_Aspect_Specifications): Convert aspect
+ SPARK_Mode into a pragma.
+ (Check_Aspect_At_Freeze_Point): Aspect SPARK_Mode does not need
+ delayed processing.
+ * sem_prag.adb: Add an entry for SPARK_Mode in table Sig_Flags.
+ (Analyze_Pragma): Add processing for pragma SPARK_Mode.
+ (Get_SPARK_Mode_Id): New routine.
+ (Is_Elaboration_SPARK_Mode): New routine.
+ (Is_Private_SPARK_Mode): New routine.
+ * sem_prag.ads (Get_SPARK_Mode_Id): New routine.
+ (Is_Elaboration_SPARK_Mode): New routine.
+ (Is_Private_SPARK_Mode): New routine.
+ * sinfo.ads: Update the comment on the usage of field Next_Pragma.
+ * snames.ads-tmpl: Add new predefined name for SPARK_Mode and
+ Auto. Add new pragma Id for SPARK_Mode.
+ * types.ads: Add new type SPARK_Mode_Id.
+
2013-07-05 Ed Schonberg <schonberg@adacore.com>
* sem_ch13.adb (Analyze_Aspect_Specifications): For
Aspect_Simple_Storage_Pool_Type => Aspect_Simple_Storage_Pool_Type,
Aspect_Size => Aspect_Size,
Aspect_Small => Aspect_Small,
+ Aspect_SPARK_Mode => Aspect_SPARK_Mode,
Aspect_Static_Predicate => Aspect_Predicate,
Aspect_Storage_Pool => Aspect_Storage_Pool,
Aspect_Storage_Size => Aspect_Storage_Size,
Aspect_Simple_Storage_Pool, -- GNAT
Aspect_Size,
Aspect_Small,
+ Aspect_SPARK_Mode, -- GNAT
Aspect_Static_Predicate,
Aspect_Storage_Pool,
Aspect_Storage_Size,
Aspect_Simple_Storage_Pool => Name,
Aspect_Size => Expression,
Aspect_Small => Expression,
+ Aspect_SPARK_Mode => Name,
Aspect_Static_Predicate => Expression,
Aspect_Storage_Pool => Name,
Aspect_Storage_Size => Expression,
Aspect_Simple_Storage_Pool_Type => Name_Simple_Storage_Pool_Type,
Aspect_Size => Name_Size,
Aspect_Small => Name_Small,
+ Aspect_SPARK_Mode => Name_SPARK_Mode,
Aspect_Static_Predicate => Name_Static_Predicate,
Aspect_Storage_Pool => Name_Storage_Pool,
Aspect_Storage_Size => Name_Storage_Size,
return Node_Id (Nodes.Table (N + 5).Field7);
end Node31;
+ function Node32 (N : Node_Id) return Node_Id is
+ begin
+ pragma Assert (Nkind (N) in N_Entity);
+ return Node_Id (Nodes.Table (N + 5).Field8);
+ end Node32;
+
function List1 (N : Node_Id) return List_Id is
begin
pragma Assert (N <= Nodes.Last);
Nodes.Table (N + 5).Field7 := Union_Id (Val);
end Set_Node31;
+ procedure Set_Node32 (N : Node_Id; Val : Node_Id) is
+ begin
+ pragma Assert (Nkind (N) in N_Entity);
+ Nodes.Table (N + 5).Field8 := Union_Id (Val);
+ end Set_Node32;
+
procedure Set_List1 (N : Node_Id; Val : List_Id) is
begin
pragma Assert (N <= Nodes.Last);
function Node31 (N : Node_Id) return Node_Id;
pragma Inline (Node31);
+ function Node32 (N : Node_Id) return Node_Id;
+ pragma Inline (Node32);
+
function List1 (N : Node_Id) return List_Id;
pragma Inline (List1);
procedure Set_Node31 (N : Node_Id; Val : Node_Id);
pragma Inline (Set_Node31);
+ procedure Set_Node32 (N : Node_Id; Val : Node_Id);
+ pragma Inline (Set_Node32);
+
procedure Set_List1 (N : Node_Id; Val : List_Id);
pragma Inline (Set_List1);
-- Thunk_Entity Node31
- -- (unused) Node32
+ -- SPARK_Mode_Pragmas Node32
-- (unused) Node33
return Ureal21 (Id);
end Small_Value;
+ function SPARK_Mode_Pragmas (Id : E) return N is
+ begin
+ pragma Assert
+ (Ekind_In (Id, E_Function, -- subprogram variants
+ E_Generic_Function,
+ E_Generic_Procedure,
+ E_Procedure,
+ E_Subprogram_Body)
+ or else
+ Ekind_In (Id, E_Generic_Package, -- package variants
+ E_Package,
+ E_Package_Body));
+ return Node32 (Id);
+ end SPARK_Mode_Pragmas;
+
function Spec_Entity (Id : E) return E is
begin
pragma Assert (Ekind (Id) = E_Package_Body or else Is_Formal (Id));
Set_Ureal21 (Id, V);
end Set_Small_Value;
+ procedure Set_SPARK_Mode_Pragmas (Id : E; V : N) is
+ begin
+ pragma Assert
+ (Ekind_In (Id, E_Function, -- subprogram variants
+ E_Generic_Function,
+ E_Generic_Procedure,
+ E_Procedure,
+ E_Subprogram_Body)
+ or else
+ Ekind_In (Id, E_Generic_Package, -- package variants
+ E_Package,
+ E_Package_Body));
+
+ Set_Node32 (Id, V);
+ end Set_SPARK_Mode_Pragmas;
+
procedure Set_Spec_Entity (Id : E; V : E) is
begin
pragma Assert (Ekind (Id) = E_Package_Body or else Is_Formal (Id));
procedure Write_Field32_Name (Id : Entity_Id) is
begin
case Ekind (Id) is
+ when E_Function |
+ E_Generic_Function |
+ E_Generic_Package |
+ E_Generic_Procedure |
+ E_Package |
+ E_Package_Body |
+ E_Procedure |
+ E_Subprogram_Body =>
+ Write_Str ("SPARK_Mode_Pragmas");
+
when others =>
Write_Str ("Field32??");
end case;
-- Small of the type, either as given in a representation clause, or
-- as computed (as a power of two) by the compiler.
+-- SPARK_Mode_Pragmas (Node32)
+-- Present in the entities of subprogram specs and bodies as well as in
+-- package specs and bodies. Points to a list of SPARK_Mode pragmas that
+-- apply to the related construct.
+
-- Spec_Entity (Node19)
-- Defined in package body entities. Points to corresponding package
-- spec entity. Also defined in subprogram body parameters in the
-- Subprograms_For_Type (Node29)
-- Corresponding_Equality (Node30) (implicit /= only)
-- Thunk_Entity (Node31) (thunk case only)
+ -- SPARK_Mode_Pragmas (Node32)
-- Body_Needed_For_SAL (Flag40)
-- Elaboration_Entity_Required (Flag174)
-- Default_Expressions_Processed (Flag108)
-- Abstract_States (Elist25)
-- Package_Instantiation (Node26)
-- Current_Use_Clause (Node27)
+ -- SPARK_Mode_Pragmas (Node32)
-- Delay_Subprogram_Descriptors (Flag50)
-- Body_Needed_For_SAL (Flag40)
-- Discard_Names (Flag88)
-- Last_Entity (Node20)
-- Scope_Depth_Value (Uint22)
-- Finalizer (Node24) (non-generic case only)
+ -- SPARK_Mode_Pragmas (Node32)
-- Delay_Subprogram_Descriptors (Flag50)
-- Has_Anonymous_Master (Flag253)
-- Scope_Depth (synth)
-- Extra_Formals (Node28)
-- Static_Initialization (Node30) (init_proc only)
-- Thunk_Entity (Node31) (thunk case only)
+ -- SPARK_Mode_Pragmas (Node32)
-- Body_Needed_For_SAL (Flag40)
-- Delay_Cleanups (Flag114)
-- Discard_Names (Flag88)
-- Last_Entity (Node20)
-- Scope_Depth_Value (Uint22)
-- Extra_Formals (Node28)
+ -- SPARK_Mode_Pragmas (Node32)
-- Scope_Depth (synth)
-- E_Subprogram_Type
function Size_Depends_On_Discriminant (Id : E) return B;
function Size_Known_At_Compile_Time (Id : E) return B;
function Small_Value (Id : E) return R;
+ function SPARK_Mode_Pragmas (Id : E) return N;
function Spec_Entity (Id : E) return E;
function Static_Elaboration_Desired (Id : E) return B;
function Static_Initialization (Id : E) return N;
procedure Set_Size_Depends_On_Discriminant (Id : E; V : B := True);
procedure Set_Size_Known_At_Compile_Time (Id : E; V : B := True);
procedure Set_Small_Value (Id : E; V : R);
+ procedure Set_SPARK_Mode_Pragmas (Id : E; V : N);
procedure Set_Spec_Entity (Id : E; V : E);
procedure Set_Static_Elaboration_Desired (Id : E; V : B);
procedure Set_Static_Initialization (Id : E; V : N);
pragma Inline (Size_Depends_On_Discriminant);
pragma Inline (Size_Known_At_Compile_Time);
pragma Inline (Small_Value);
+ pragma Inline (SPARK_Mode_Pragmas);
pragma Inline (Spec_Entity);
pragma Inline (Static_Elaboration_Desired);
pragma Inline (Static_Initialization);
pragma Inline (Set_Size_Depends_On_Discriminant);
pragma Inline (Set_Size_Known_At_Compile_Time);
pragma Inline (Set_Small_Value);
+ pragma Inline (Set_SPARK_Mode_Pragmas);
pragma Inline (Set_Spec_Entity);
pragma Inline (Set_Static_Elaboration_Desired);
pragma Inline (Set_Static_Initialization);
* Pragma Source_File_Name::
* Pragma Source_File_Name_Project::
* Pragma Source_Reference::
+* Pragma SPARK_Mode::
* Pragma Static_Elaboration_Desired::
* Pragma Stream_Convert::
* Pragma Style_Checks::
* Aspect Shared::
* Aspect Simple_Storage_Pool::
* Aspect Simple_Storage_Pool_Type::
+* Aspect SPARK_Mode::
* Aspect Suppress_Debug_Info::
* Aspect Test_Case::
* Aspect Universal_Aliasing::
* Pragma Source_File_Name::
* Pragma Source_File_Name_Project::
* Pragma Source_Reference::
+* Pragma SPARK_Mode::
* Pragma Static_Elaboration_Desired::
* Pragma Stream_Convert::
* Pragma Style_Checks::
string expression other than a string literal. This is because its value
is needed for error messages issued by all phases of the compiler.
+@node Pragma SPARK_Mode
+@unnumberedsec Pragma SPARK_Mode
+@findex SPARK_Mode
+@noindent
+Syntax:
+
+@smallexample @c ada
+pragma SPARK_Mode [ (On | Off | Auto) ] ;
+@end smallexample
+
+@noindent
+This pragma is used to designate whether a contract and its implementation must
+follow the SPARK 2014 programming language syntactic and semantic rules. The
+pragma is intended for use with formal verification tools and has no effect on
+the generated code.
+
+When used as a configuration pragma over a whole compilation or in a particular
+compilation unit, it sets the mode of the units involved, in particular:
+
+@itemize @bullet
+
+@item
+@code{On}: All entities in the units must follow the SPARK 2014 language, and
+an error will be generated if not, unless locally overridden by a local
+SPARK_Mode pragma or aspect. @code{On} is the default mode when pragma
+SPARK_Mode is used without an argument.
+
+@item
+@code{Off}: The units are considered to be in Ada by default and therefore not
+part of SPARK 2014 unless overridden locally. These units may be called by SPARK
+2014 units.
+
+@item
+@code{Auto}: The formal verification tools will automatically detect whether
+each entity is in SPARK 2014 or in Ada.
+
+@end itemize
+
+Pragma SPARK_Mode can be used as a local pragma with the following semantics:
+
+@itemize @bullet
+
+@item
+Auto cannot be used as a mode argument.
+
+@item
+When the pragma appears immediately within the visible declarations of a
+package, it marks the whole package (spec and body) in or out of SPARK 2014.
+
+@item
+When the pragma appears immediately within the private declarations of a
+package, it marks the private part in or out of SPARK 2014.
+
+@item
+When the pragma appears immediately within the declarations of a package body,
+it marks the whole body in or out of SPARK 2014.
+
+@item
+When the pragma appears immediately within the elaboration statements of a
+package body, it marks the statements in or out of SPARK 2014.
+
+@item
+When the pragma appears after a subprogram declaration, it marks the whole
+subprogram (spec and body) in or out of SPARK 2014.
+
+@item
+When the pragma appears immediately within the declarations of a subprogram
+body, it marks the whole body in or out of SPARK 2014.
+
+@item
+Any other use of the pragma is illegal.
+
+@end itemize
+
@node Pragma Static_Elaboration_Desired
@unnumberedsec Pragma Static_Elaboration_Desired
@findex Static_Elaboration_Desired
subtype, and whose returned type must be the type given as the first
argument to the pragma.
-The meaning of the @var{Read}
-parameter is that if a stream attribute directly
+The meaning of the @var{Read} parameter is that if a stream attribute directly
or indirectly specifies reading of the type given as the first parameter,
then a value of the type given as the argument to the Read function is
read from the stream, and then the Read function is used to convert this
* Aspect Shared::
* Aspect Simple_Storage_Pool::
* Aspect Simple_Storage_Pool_Type::
+* Aspect SPARK_Mode::
* Aspect Suppress_Debug_Info::
* Aspect Test_Case::
* Aspect Universal_Aliasing::
@noindent
This aspect is equivalent to pragma @code{Simple_Storage_Pool_Type}.
+@node Aspect SPARK_Mode
+@unnumberedsec Aspect SPARK_Mode
+@findex SPARK_Mode
+@noindent
+This aspect is equivalent to pragma @code{SPARK_Mode}.
+
@node Aspect Suppress_Debug_Info
@unnumberedsec Aspect Suppress_Debug_Info
@findex Suppress_Debug_Info
Short_Circuit_And_Or
Source_File_Name
Source_File_Name_Project
+ SPARK_Mode
Style_Checks
Suppress
Suppress_Exception_Locations
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2012, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2013, 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- --
Unum := Units.Last;
Units.Table (Unum) := (
- Cunit => Cunit,
- Cunit_Entity => Cunit_Entity,
- Dependency_Num => 0,
- Dynamic_Elab => False,
- Error_Location => Sloc (With_Node),
- Expected_Unit => Spec_Name,
- Fatal_Error => True,
- Generate_Code => False,
- Has_Allocator => False,
- Has_RACW => False,
- Is_Compiler_Unit => False,
- Ident_String => Empty,
- Loading => False,
- Main_Priority => Default_Main_Priority,
- Main_CPU => Default_Main_CPU,
- Munit_Index => 0,
- Serial_Number => 0,
- Source_Index => No_Source_File,
- Unit_File_Name => Get_File_Name (Spec_Name, Subunit => False),
- Unit_Name => Spec_Name,
- Version => 0,
- OA_Setting => 'O');
+ Cunit => Cunit,
+ Cunit_Entity => Cunit_Entity,
+ Dependency_Num => 0,
+ Dynamic_Elab => False,
+ Error_Location => Sloc (With_Node),
+ Expected_Unit => Spec_Name,
+ Fatal_Error => True,
+ Generate_Code => False,
+ Has_Allocator => False,
+ Has_RACW => False,
+ Is_Compiler_Unit => False,
+ Ident_String => Empty,
+ Loading => False,
+ Main_Priority => Default_Main_Priority,
+ Main_CPU => Default_Main_CPU,
+ Munit_Index => 0,
+ Serial_Number => 0,
+ Source_Index => No_Source_File,
+ Unit_File_Name => Get_File_Name (Spec_Name, Subunit => False),
+ Unit_Name => Spec_Name,
+ Version => 0,
+ OA_Setting => 'O',
+ SPARK_Mode_Pragma => Empty);
Set_Comes_From_Source_Default (Save_CS);
Set_Error_Posted (Cunit_Entity);
end if;
Units.Table (Main_Unit) := (
- Cunit => Empty,
- Cunit_Entity => Empty,
- Dependency_Num => 0,
- Dynamic_Elab => False,
- Error_Location => No_Location,
- Expected_Unit => No_Unit_Name,
- Fatal_Error => False,
- Generate_Code => False,
- Has_Allocator => False,
- Has_RACW => False,
- Is_Compiler_Unit => False,
- Ident_String => Empty,
- Loading => True,
- Main_Priority => Default_Main_Priority,
- Main_CPU => Default_Main_CPU,
- Munit_Index => 0,
- Serial_Number => 0,
- Source_Index => Main_Source_File,
- Unit_File_Name => Fname,
- Unit_Name => No_Unit_Name,
- Version => Version,
- OA_Setting => 'O');
+ Cunit => Empty,
+ Cunit_Entity => Empty,
+ Dependency_Num => 0,
+ Dynamic_Elab => False,
+ Error_Location => No_Location,
+ Expected_Unit => No_Unit_Name,
+ Fatal_Error => False,
+ Generate_Code => False,
+ Has_Allocator => False,
+ Has_RACW => False,
+ Is_Compiler_Unit => False,
+ Ident_String => Empty,
+ Loading => True,
+ Main_Priority => Default_Main_Priority,
+ Main_CPU => Default_Main_CPU,
+ Munit_Index => 0,
+ Serial_Number => 0,
+ Source_Index => Main_Source_File,
+ Unit_File_Name => Fname,
+ Unit_Name => No_Unit_Name,
+ Version => Version,
+ OA_Setting => 'O',
+ SPARK_Mode_Pragma => Empty);
end if;
end Load_Main_Source;
if Src_Ind /= No_Source_File then
Units.Table (Unum) := (
- Cunit => Empty,
- Cunit_Entity => Empty,
- Dependency_Num => 0,
- Dynamic_Elab => False,
- Error_Location => Sloc (Error_Node),
- Expected_Unit => Uname_Actual,
- Fatal_Error => False,
- Generate_Code => False,
- Has_Allocator => False,
- Has_RACW => False,
- Is_Compiler_Unit => False,
- Ident_String => Empty,
- Loading => True,
- Main_Priority => Default_Main_Priority,
- Main_CPU => Default_Main_CPU,
- Munit_Index => 0,
- Serial_Number => 0,
- Source_Index => Src_Ind,
- Unit_File_Name => Fname,
- Unit_Name => Uname_Actual,
- Version => Source_Checksum (Src_Ind),
- OA_Setting => 'O');
+ Cunit => Empty,
+ Cunit_Entity => Empty,
+ Dependency_Num => 0,
+ Dynamic_Elab => False,
+ Error_Location => Sloc (Error_Node),
+ Expected_Unit => Uname_Actual,
+ Fatal_Error => False,
+ Generate_Code => False,
+ Has_Allocator => False,
+ Has_RACW => False,
+ Is_Compiler_Unit => False,
+ Ident_String => Empty,
+ Loading => True,
+ Main_Priority => Default_Main_Priority,
+ Main_CPU => Default_Main_CPU,
+ Munit_Index => 0,
+ Serial_Number => 0,
+ Source_Index => Src_Ind,
+ Unit_File_Name => Fname,
+ Unit_Name => Uname_Actual,
+ Version => Source_Checksum (Src_Ind),
+ OA_Setting => 'O',
+ SPARK_Mode_Pragma => Empty);
-- Parse the new unit
begin
Units.Increment_Last;
Units.Table (Units.Last) :=
- (Unit_File_Name => File_Name (S),
- Unit_Name => No_Unit_Name,
- Expected_Unit => No_Unit_Name,
- Source_Index => S,
- Cunit => Empty,
- Cunit_Entity => Empty,
- Dependency_Num => 0,
- Dynamic_Elab => False,
- Fatal_Error => False,
- Generate_Code => False,
- Has_Allocator => False,
- Has_RACW => False,
- Is_Compiler_Unit => False,
- Ident_String => Empty,
- Loading => False,
- Main_Priority => -1,
- Main_CPU => -1,
- Munit_Index => 0,
- Serial_Number => 0,
- Version => 0,
- Error_Location => No_Location,
- OA_Setting => 'O');
+ (Unit_File_Name => File_Name (S),
+ Unit_Name => No_Unit_Name,
+ Expected_Unit => No_Unit_Name,
+ Source_Index => S,
+ Cunit => Empty,
+ Cunit_Entity => Empty,
+ Dependency_Num => 0,
+ Dynamic_Elab => False,
+ Fatal_Error => False,
+ Generate_Code => False,
+ Has_Allocator => False,
+ Has_RACW => False,
+ Is_Compiler_Unit => False,
+ Ident_String => Empty,
+ Loading => False,
+ Main_Priority => -1,
+ Main_CPU => -1,
+ Munit_Index => 0,
+ Serial_Number => 0,
+ Version => 0,
+ Error_Location => No_Location,
+ OA_Setting => 'O',
+ SPARK_Mode_Pragma => Empty);
end Add_Preprocessing_Dependency;
------------------------------
Units.Increment_Last;
Units.Table (Units.Last) := (
- Unit_File_Name => System_Fname,
- Unit_Name => System_Uname,
- Expected_Unit => System_Uname,
- Source_Index => System_Source_File_Index,
- Cunit => Empty,
- Cunit_Entity => Empty,
- Dependency_Num => 0,
- Dynamic_Elab => False,
- Fatal_Error => False,
- Generate_Code => False,
- Has_Allocator => False,
- Has_RACW => False,
- Is_Compiler_Unit => False,
- Ident_String => Empty,
- Loading => False,
- Main_Priority => -1,
- Main_CPU => -1,
- Munit_Index => 0,
- Serial_Number => 0,
- Version => 0,
- Error_Location => No_Location,
- OA_Setting => 'O');
+ Unit_File_Name => System_Fname,
+ Unit_Name => System_Uname,
+ Expected_Unit => System_Uname,
+ Source_Index => System_Source_File_Index,
+ Cunit => Empty,
+ Cunit_Entity => Empty,
+ Dependency_Num => 0,
+ Dynamic_Elab => False,
+ Fatal_Error => False,
+ Generate_Code => False,
+ Has_Allocator => False,
+ Has_RACW => False,
+ Is_Compiler_Unit => False,
+ Ident_String => Empty,
+ Loading => False,
+ Main_Priority => -1,
+ Main_CPU => -1,
+ Munit_Index => 0,
+ Serial_Number => 0,
+ Version => 0,
+ Error_Location => No_Location,
+ OA_Setting => 'O',
+ SPARK_Mode_Pragma => Empty);
-- Parse system.ads so that the checksum is set right
-- Style checks are not applied.
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2012, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2013, 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- --
return Units.Table (U).Source_Index;
end Source_Index;
+ function SPARK_Mode_Pragma (U : Unit_Number_Type) return Node_Id is
+ begin
+ return Units.Table (U).SPARK_Mode_Pragma;
+ end SPARK_Mode_Pragma;
+
function Unit_File_Name (U : Unit_Number_Type) return File_Name_Type is
begin
return Units.Table (U).Unit_File_Name;
Units.Table (U).OA_Setting := C;
end Set_OA_Setting;
+ procedure Set_SPARK_Mode_Pragma (U : Unit_Number_Type; N : Node_Id) is
+ begin
+ Units.Table (U).SPARK_Mode_Pragma := N;
+ end Set_SPARK_Mode_Pragma;
+
procedure Set_Unit_Name (U : Unit_Number_Type; N : Unit_Name_Type) is
begin
Units.Table (U).Unit_Name := N;
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2012, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2013, 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- --
-- The first entry in the table, subscript Main_Unit, is for the main file.
-- Each entry in this units table contains the following data.
- -- Unit_File_Name
- -- The name of the source file containing the unit. Set when the entry
- -- is created by a call to Lib.Load, and then cannot be changed.
-
- -- Source_Index
- -- The index in the source file table of the corresponding source file.
- -- Set when the entry is created by a call to Lib.Load and then cannot
- -- be changed.
-
- -- Munit_Index
- -- The index of the unit within the file for multiple unit per file
- -- mode. Set to zero in normal single unit per file mode.
-
- -- Error_Location
- -- This is copied from the Sloc field of the Enode argument passed
- -- to Load_Unit. It refers to the enclosing construct which caused
- -- this unit to be loaded, e.g. most typically the with clause that
- -- referenced the unit, and is used for error handling in Par.Load.
-
- -- Expected_Unit
- -- This is the expected unit name for a file other than the main unit,
- -- since these are cases where we load the unit using Lib.Load and we
- -- know the unit that is expected. It must be the same as Unit_Name
- -- if it is set (see test in Par.Load). Expected_Unit is set to
- -- No_Name for the main unit.
-
- -- Unit_Name
- -- The name of the unit. Initialized to No_Name by Lib.Load, and then
- -- set by the parser when the unit is parsed to the unit name actually
- -- found in the file (which should, in the absence of errors) be the
- -- same name as Expected_Unit.
-
-- Cunit
-- Pointer to the N_Compilation_Unit node. Initially set to Empty by
-- Lib.Load, and then reset to the required node by the parser when
-- checks specified (as the result of using the -gnatE compilation
-- option or a pragma Elaboration_Checks (Dynamic).
+ -- Error_Location
+ -- This is copied from the Sloc field of the Enode argument passed
+ -- to Load_Unit. It refers to the enclosing construct which caused
+ -- this unit to be loaded, e.g. most typically the with clause that
+ -- referenced the unit, and is used for error handling in Par.Load.
+
+ -- Expected_Unit
+ -- This is the expected unit name for a file other than the main unit,
+ -- since these are cases where we load the unit using Lib.Load and we
+ -- know the unit that is expected. It must be the same as Unit_Name
+ -- if it is set (see test in Par.Load). Expected_Unit is set to
+ -- No_Name for the main unit.
+
-- Fatal_Error
-- A flag that is initialized to False, and gets set to True if a fatal
-- error occurs during the processing of a unit. A fatal error is one
-- code is to be generated. This includes the unit explicitly compiled,
-- together with its specification, and any subunits.
+ -- Has_Allocator
+ -- This flag is set if a subprogram unit has an allocator after the
+ -- BEGIN (it is used to set the AB flag in the M ALI line).
+
-- Has_RACW
-- A Boolean flag, initially set to False when a unit entry is created,
-- and set to True if the unit defines a remote access to class wide
-- that the default affinity is to be used (and is also used for
-- entries that do not correspond to possible main programs).
- -- Has_Allocator
- -- This flag is set if a subprogram unit has an allocator after the
- -- BEGIN (it is used to set the AB flag in the M ALI line).
+ -- Munit_Index
+ -- The index of the unit within the file for multiple unit per file
+ -- mode. Set to zero in normal single unit per file mode.
-- OA_Setting
-- This is a character field containing L if Optimize_Alignment mode
-- routine which increments the current value and returns it. This
-- serial number is separate for each unit.
+ -- Source_Index
+ -- The index in the source file table of the corresponding source file.
+ -- Set when the entry is created by a call to Lib.Load and then cannot
+ -- be changed.
+
+ -- SPARK_Mode_Pragma
+ -- Pointer to the configuration pragma SPARK_Mode that applies to the
+ -- whole unit.
+
+ -- Unit_File_Name
+ -- The name of the source file containing the unit. Set when the entry
+ -- is created by a call to Lib.Load, and then cannot be changed.
+
+ -- Unit_Name
+ -- The name of the unit. Initialized to No_Name by Lib.Load, and then
+ -- set by the parser when the unit is parsed to the unit name actually
+ -- found in the file (which should, in the absence of errors) be the
+ -- same name as Expected_Unit.
+
-- Version
-- This field holds the version of the unit, which is computed as
-- the exclusive or of the checksums of this unit, and all its
Default_Main_CPU : constant Int := -1;
-- Value used in Main_CPU field to indicate default main affinity
- function Cunit (U : Unit_Number_Type) return Node_Id;
- function Cunit_Entity (U : Unit_Number_Type) return Entity_Id;
- function Dependency_Num (U : Unit_Number_Type) return Nat;
- function Dynamic_Elab (U : Unit_Number_Type) return Boolean;
- function Error_Location (U : Unit_Number_Type) return Source_Ptr;
- function Expected_Unit (U : Unit_Number_Type) return Unit_Name_Type;
- function Fatal_Error (U : Unit_Number_Type) return Boolean;
- function Generate_Code (U : Unit_Number_Type) return Boolean;
- function Ident_String (U : Unit_Number_Type) return Node_Id;
- function Has_Allocator (U : Unit_Number_Type) return Boolean;
- function Has_RACW (U : Unit_Number_Type) return Boolean;
- function Is_Compiler_Unit (U : Unit_Number_Type) return Boolean;
- function Loading (U : Unit_Number_Type) return Boolean;
- function Main_CPU (U : Unit_Number_Type) return Int;
- function Main_Priority (U : Unit_Number_Type) return Int;
- function Munit_Index (U : Unit_Number_Type) return Nat;
- function OA_Setting (U : Unit_Number_Type) return Character;
- function Source_Index (U : Unit_Number_Type) return Source_File_Index;
- function Unit_File_Name (U : Unit_Number_Type) return File_Name_Type;
- function Unit_Name (U : Unit_Number_Type) return Unit_Name_Type;
+ function Cunit (U : Unit_Number_Type) return Node_Id;
+ function Cunit_Entity (U : Unit_Number_Type) return Entity_Id;
+ function Dependency_Num (U : Unit_Number_Type) return Nat;
+ function Dynamic_Elab (U : Unit_Number_Type) return Boolean;
+ function Error_Location (U : Unit_Number_Type) return Source_Ptr;
+ function Expected_Unit (U : Unit_Number_Type) return Unit_Name_Type;
+ function Fatal_Error (U : Unit_Number_Type) return Boolean;
+ function Generate_Code (U : Unit_Number_Type) return Boolean;
+ function Ident_String (U : Unit_Number_Type) return Node_Id;
+ function Has_Allocator (U : Unit_Number_Type) return Boolean;
+ function Has_RACW (U : Unit_Number_Type) return Boolean;
+ function Is_Compiler_Unit (U : Unit_Number_Type) return Boolean;
+ function Loading (U : Unit_Number_Type) return Boolean;
+ function Main_CPU (U : Unit_Number_Type) return Int;
+ function Main_Priority (U : Unit_Number_Type) return Int;
+ function Munit_Index (U : Unit_Number_Type) return Nat;
+ function OA_Setting (U : Unit_Number_Type) return Character;
+ function Source_Index (U : Unit_Number_Type) return Source_File_Index;
+ function SPARK_Mode_Pragma (U : Unit_Number_Type) return Node_Id;
+ function Unit_File_Name (U : Unit_Number_Type) return File_Name_Type;
+ function Unit_Name (U : Unit_Number_Type) return Unit_Name_Type;
-- Get value of named field from given units table entry
- procedure Set_Cunit (U : Unit_Number_Type; N : Node_Id);
- procedure Set_Cunit_Entity (U : Unit_Number_Type; E : Entity_Id);
- procedure Set_Dynamic_Elab (U : Unit_Number_Type; B : Boolean := True);
- procedure Set_Error_Location (U : Unit_Number_Type; W : Source_Ptr);
- procedure Set_Fatal_Error (U : Unit_Number_Type; B : Boolean := True);
- procedure Set_Generate_Code (U : Unit_Number_Type; B : Boolean := True);
- procedure Set_Has_RACW (U : Unit_Number_Type; B : Boolean := True);
- procedure Set_Has_Allocator (U : Unit_Number_Type; B : Boolean := True);
- procedure Set_Is_Compiler_Unit (U : Unit_Number_Type; B : Boolean := True);
- procedure Set_Ident_String (U : Unit_Number_Type; N : Node_Id);
- procedure Set_Loading (U : Unit_Number_Type; B : Boolean := True);
- procedure Set_Main_CPU (U : Unit_Number_Type; P : Int);
- procedure Set_Main_Priority (U : Unit_Number_Type; P : Int);
- procedure Set_OA_Setting (U : Unit_Number_Type; C : Character);
- procedure Set_Unit_Name (U : Unit_Number_Type; N : Unit_Name_Type);
+ procedure Set_Cunit (U : Unit_Number_Type; N : Node_Id);
+ procedure Set_Cunit_Entity (U : Unit_Number_Type; E : Entity_Id);
+ procedure Set_Dynamic_Elab (U : Unit_Number_Type; B : Boolean := True);
+ procedure Set_Error_Location (U : Unit_Number_Type; W : Source_Ptr);
+ procedure Set_Fatal_Error (U : Unit_Number_Type; B : Boolean := True);
+ procedure Set_Generate_Code (U : Unit_Number_Type; B : Boolean := True);
+ procedure Set_Has_RACW (U : Unit_Number_Type; B : Boolean := True);
+ procedure Set_Has_Allocator (U : Unit_Number_Type; B : Boolean := True);
+ procedure Set_Is_Compiler_Unit (U : Unit_Number_Type; B : Boolean := True);
+ procedure Set_Ident_String (U : Unit_Number_Type; N : Node_Id);
+ procedure Set_Loading (U : Unit_Number_Type; B : Boolean := True);
+ procedure Set_Main_CPU (U : Unit_Number_Type; P : Int);
+ procedure Set_Main_Priority (U : Unit_Number_Type; P : Int);
+ procedure Set_OA_Setting (U : Unit_Number_Type; C : Character);
+ procedure Set_SPARK_Mode_Pragma (U : Unit_Number_Type; N : Node_Id);
+ procedure Set_Unit_Name (U : Unit_Number_Type; N : Unit_Name_Type);
-- Set value of named field for given units table entry. Note that we
-- do not have an entry for each possible field, since some of the fields
-- can only be set by specialized interfaces (defined below).
pragma Inline (Set_Main_CPU);
pragma Inline (Set_Main_Priority);
pragma Inline (Set_OA_Setting);
+ pragma Inline (Set_SPARK_Mode_Pragma);
pragma Inline (Set_Unit_Name);
pragma Inline (Source_Index);
+ pragma Inline (SPARK_Mode_Pragma);
pragma Inline (Unit_File_Name);
pragma Inline (Unit_Name);
type Unit_Record is record
- Unit_File_Name : File_Name_Type;
- Unit_Name : Unit_Name_Type;
- Munit_Index : Nat;
- Expected_Unit : Unit_Name_Type;
- Source_Index : Source_File_Index;
- Cunit : Node_Id;
- Cunit_Entity : Entity_Id;
- Dependency_Num : Int;
- Ident_String : Node_Id;
- Main_Priority : Int;
- Main_CPU : Int;
- Serial_Number : Nat;
- Version : Word;
- Error_Location : Source_Ptr;
- Fatal_Error : Boolean;
- Generate_Code : Boolean;
- Has_RACW : Boolean;
- Is_Compiler_Unit : Boolean;
- Dynamic_Elab : Boolean;
- Loading : Boolean;
- Has_Allocator : Boolean;
- OA_Setting : Character;
+ Unit_File_Name : File_Name_Type;
+ Unit_Name : Unit_Name_Type;
+ Munit_Index : Nat;
+ Expected_Unit : Unit_Name_Type;
+ Source_Index : Source_File_Index;
+ Cunit : Node_Id;
+ Cunit_Entity : Entity_Id;
+ Dependency_Num : Int;
+ Ident_String : Node_Id;
+ Main_Priority : Int;
+ Main_CPU : Int;
+ Serial_Number : Nat;
+ Version : Word;
+ Error_Location : Source_Ptr;
+ Fatal_Error : Boolean;
+ Generate_Code : Boolean;
+ Has_RACW : Boolean;
+ Is_Compiler_Unit : Boolean;
+ Dynamic_Elab : Boolean;
+ Loading : Boolean;
+ Has_Allocator : Boolean;
+ OA_Setting : Character;
+ SPARK_Mode_Pragma : Node_Id;
end record;
-- The following representation clause ensures that the above record
-- written by Tree_Gen, we do not write uninitialized values to the file.
for Unit_Record use record
- Unit_File_Name at 0 range 0 .. 31;
- Unit_Name at 4 range 0 .. 31;
- Munit_Index at 8 range 0 .. 31;
- Expected_Unit at 12 range 0 .. 31;
- Source_Index at 16 range 0 .. 31;
- Cunit at 20 range 0 .. 31;
- Cunit_Entity at 24 range 0 .. 31;
- Dependency_Num at 28 range 0 .. 31;
- Ident_String at 32 range 0 .. 31;
- Main_Priority at 36 range 0 .. 31;
- Main_CPU at 40 range 0 .. 31;
- Serial_Number at 44 range 0 .. 31;
- Version at 48 range 0 .. 31;
- Error_Location at 52 range 0 .. 31;
- Fatal_Error at 56 range 0 .. 7;
- Generate_Code at 57 range 0 .. 7;
- Has_RACW at 58 range 0 .. 7;
- Dynamic_Elab at 59 range 0 .. 7;
- Is_Compiler_Unit at 60 range 0 .. 7;
- OA_Setting at 61 range 0 .. 7;
- Loading at 62 range 0 .. 7;
- Has_Allocator at 63 range 0 .. 7;
+ Unit_File_Name at 0 range 0 .. 31;
+ Unit_Name at 4 range 0 .. 31;
+ Munit_Index at 8 range 0 .. 31;
+ Expected_Unit at 12 range 0 .. 31;
+ Source_Index at 16 range 0 .. 31;
+ Cunit at 20 range 0 .. 31;
+ Cunit_Entity at 24 range 0 .. 31;
+ Dependency_Num at 28 range 0 .. 31;
+ Ident_String at 32 range 0 .. 31;
+ Main_Priority at 36 range 0 .. 31;
+ Main_CPU at 40 range 0 .. 31;
+ Serial_Number at 44 range 0 .. 31;
+ Version at 48 range 0 .. 31;
+ Error_Location at 52 range 0 .. 31;
+ Fatal_Error at 56 range 0 .. 7;
+ Generate_Code at 57 range 0 .. 7;
+ Has_RACW at 58 range 0 .. 7;
+ Dynamic_Elab at 59 range 0 .. 7;
+ Is_Compiler_Unit at 60 range 0 .. 7;
+ OA_Setting at 61 range 0 .. 7;
+ Loading at 62 range 0 .. 7;
+ Has_Allocator at 63 range 0 .. 7;
+ SPARK_Mode_Pragma at 64 range 0 .. 31;
end record;
- for Unit_Record'Size use 64 * 8;
+ for Unit_Record'Size use 68 * 8;
-- This ensures that we did not leave out any fields
package Units is new Table.Table (
-- Modes for Formal Verification --
-----------------------------------
+ Frame_Condition_Mode : Boolean := False;
+ -- Specific mode to be used in combination with SPARK_Mode. If set to
+ -- true, ALI files containing the frame conditions (global effects) are
+ -- generated, and Why files are *not* generated. If not true, Why files
+ -- are generated. Set by debug flag -gnatd.G.
+
+ Formal_Extensions : Boolean := False;
+ -- When this flag is set, new aspects/pragmas/attributes are accepted,
+ -- whose main purpose is to facilitate formal verification. Set by debug
+ -- flag -gnatd.V.
+
+ Global_SPARK_Mode : SPARK_Mode_Id := None;
+ -- The mode applicable to the whole compilation. The global mode can be set
+ -- in a configuration file such as gnat.adc.
+
SPARK_Mode : Boolean := False;
-- Specific compiling mode targeting formal verification through the
-- generation of Why code for those parts of the input code that belong to
-- from the SPARK restriction defined in GNAT to detect violations of a
-- subset of SPARK 2005 rules.
- Frame_Condition_Mode : Boolean := False;
- -- Specific mode to be used in combination with SPARK_Mode. If set to
- -- true, ALI files containing the frame conditions (global effects) are
- -- generated, and Why files are *not* generated. If not true, Why files
- -- are generated. Set by debug flag -gnatd.G.
-
SPARK_Strict_Mode : Boolean := False;
-- Interpret compiler permissions as strictly as possible. E.g. base ranges
-- for integers are limited to the strict minimum with this option. Set by
-- debug flag -gnatd.D.
- Formal_Extensions : Boolean := False;
- -- When this flag is set, new aspects/pragmas/attributes are accepted,
- -- whose main purpose is to facilitate formal verification. Set by debug
- -- flag -gnatd.V.
-
function Full_Expander_Active return Boolean;
pragma Inline (Full_Expander_Active);
-- Returns the value of (Expander_Active and not SPARK_Mode). This "flag"
Pragma_Short_Circuit_And_Or |
Pragma_Short_Descriptors |
Pragma_Simple_Storage_Pool_Type |
+ Pragma_SPARK_Mode |
Pragma_Storage_Size |
Pragma_Storage_Unit |
Pragma_Static_Elaboration_Desired |
Insert_Delayed_Pragma (Aitem);
goto Continue;
+ -- SPARK_Mode
+
+ when Aspect_SPARK_Mode =>
+ Make_Aitem_Pragma
+ (Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Relocate_Node (Expr))),
+ Pragma_Name => Name_SPARK_Mode);
+ Delay_Required := False;
+
-- Relative_Deadline
when Aspect_Relative_Deadline =>
Aspect_Postcondition |
Aspect_Pre |
Aspect_Precondition |
+ Aspect_SPARK_Mode |
Aspect_Test_Case =>
raise Program_Error;
-- original one, following the renaming chain) is returned. Otherwise the
-- entity is returned unchanged. Should be in Einfo???
+ function Get_SPARK_Mode_Id (N : Name_Id) return SPARK_Mode_Id;
+ -- Subsidiary to the analysis of pragma SPARK_Mode as well as subprogram
+ -- Get_SPARK_Mode_Id. Convert a name into a corresponding value of type
+ -- SPARK_Mode_Id.
+
function Original_Name (N : Node_Id) return Name_Id;
-- N is a pragma node or aspect specification node. This function returns
-- the name of the pragma or aspect in original source form, taking into
when Pragma_Source_Reference =>
GNAT_Pragma;
+ ----------------
+ -- SPARK_Mode --
+ ----------------
+
+ -- pragma SPARK_Mode (On | Off | Auto);
+
+ when Pragma_SPARK_Mode => SPARK_Mod : declare
+ procedure Chain_Pragma (Context : Entity_Id; Prag : Node_Id);
+ -- Associate a SPARK_Mode pragma with the context where it lives.
+ -- If the context is a package spec or a body, the routine checks
+ -- the consistency between modes of visible/private declarations
+ -- and body declarations/statements.
+
+ procedure Check_Conformance
+ (Governing_Id : Entity_Id;
+ New_Id : Entity_Id);
+ -- Verify the "monotonicity" of SPARK modes between two entities.
+ -- The order of modes is Off < Auto < On. Governing_Id establishes
+ -- the mode of the context. New_Id attempts to redefine the known
+ -- mode.
+
+ procedure Check_Pragma_Conformance
+ (Governing_Mode : Node_Id;
+ New_Mode : Node_Id);
+ -- Verify the "monotonicity" of two SPARK_Mode pragmas. The order
+ -- of modes is Off < Auto < On. Governing_Mode is the established
+ -- mode dictated by the context. New_Mode attempts to redefine the
+ -- governing mode.
+
+ function Get_SPARK_Mode_Name (Id : SPARK_Mode_Id) return Name_Id;
+ -- Convert a value of type SPARK_Mode_Id into a corresponding name
+
+ procedure Redefinition_Error (Mode : SPARK_Mode_Id);
+ -- Emit an error on an attempt to redefine existing mode Mode. The
+ -- message is associated with the first argument of the current
+ -- pragma.
+
+ procedure Redefinition_Error (Prag : Node_Id);
+ -- Emit an error on an attempt to redefine the mode of Prag. The
+ -- message is associated with the first argument of the current
+ -- pragma.
+
+ ------------------
+ -- Chain_Pragma --
+ ------------------
+
+ procedure Chain_Pragma (Context : Entity_Id; Prag : Node_Id) is
+ Existing_Prag : constant Node_Id :=
+ SPARK_Mode_Pragmas (Context);
+ begin
+ -- The context does not have a prior mode defined
+
+ if No (Existing_Prag) then
+ Set_SPARK_Mode_Pragmas (Context, Prag);
+
+ -- Chain the new mode on the list of SPARK_Mode pragmas. Verify
+ -- the consistency between the existing mode and the new one.
+
+ else
+ Set_Next_Pragma (Existing_Prag, Prag);
+
+ Check_Pragma_Conformance
+ (Governing_Mode => Existing_Prag,
+ New_Mode => Prag);
+ end if;
+ end Chain_Pragma;
+
+ -----------------------
+ -- Check_Conformance --
+ -----------------------
+
+ procedure Check_Conformance
+ (Governing_Id : Entity_Id;
+ New_Id : Entity_Id)
+ is
+ Gov_Prag : constant Node_Id :=
+ SPARK_Mode_Pragmas (Governing_Id);
+ New_Prag : constant Node_Id := SPARK_Mode_Pragmas (New_Id);
+
+ begin
+ -- Nothing to do when one or both entities lack a mode
+
+ if No (Gov_Prag) or else No (New_Prag) then
+ return;
+ end if;
+
+ -- Do not compare the modes of a package spec and body when the
+ -- spec mode appears in the private part. In this case the spec
+ -- mode does not affect the body.
+
+ if Ekind_In (Governing_Id, E_Generic_Package, E_Package)
+ and then Ekind (New_Id) = E_Package_Body
+ and then Is_Private_SPARK_Mode (Gov_Prag)
+ then
+ null;
+
+ -- Test the pragmas
+
+ else
+ Check_Pragma_Conformance
+ (Governing_Mode => Gov_Prag,
+ New_Mode => New_Prag);
+ end if;
+ end Check_Conformance;
+
+ ------------------------------
+ -- Check_Pragma_Conformance --
+ ------------------------------
+
+ procedure Check_Pragma_Conformance
+ (Governing_Mode : Node_Id;
+ New_Mode : Node_Id)
+ is
+ Gov_M : constant SPARK_Mode_Id :=
+ Get_SPARK_Mode_Id (Governing_Mode);
+ New_M : constant SPARK_Mode_Id := Get_SPARK_Mode_Id (New_Mode);
+
+ begin
+ -- The new mode is less restrictive than the established mode
+
+ if Gov_M < New_M then
+ Error_Msg_Name_1 := Get_SPARK_Mode_Name (New_M);
+ Error_Msg_N ("cannot define 'S'P'A'R'K mode %", New_Mode);
+
+ Error_Msg_Name_1 := Get_SPARK_Mode_Name (Gov_M);
+ Error_Msg_Sloc := Sloc (Governing_Mode);
+ Error_Msg_N
+ ("\mode is less restrictive than mode % defined #",
+ New_Mode);
+ end if;
+ end Check_Pragma_Conformance;
+
+ -------------------------
+ -- Get_SPARK_Mode_Name --
+ -------------------------
+
+ function Get_SPARK_Mode_Name (Id : SPARK_Mode_Id) return Name_Id is
+ begin
+ if Id = SPARK_On then
+ return Name_On;
+ elsif Id = SPARK_Off then
+ return Name_Off;
+ elsif Id = SPARK_Auto then
+ return Name_Auto;
+
+ -- Mode "None" should never be used in error message generation
+
+ else
+ raise Program_Error;
+ end if;
+ end Get_SPARK_Mode_Name;
+
+ ------------------------
+ -- Redefinition_Error --
+ ------------------------
+
+ procedure Redefinition_Error (Mode : SPARK_Mode_Id) is
+ begin
+ Error_Msg_Name_1 := Get_SPARK_Mode_Name (Mode);
+ Error_Msg_N
+ ("cannot redefine 'S'P'A'R'K mode, already set to %", Arg1);
+ end Redefinition_Error;
+
+ ------------------------
+ -- Redefinition_Error --
+ ------------------------
+
+ procedure Redefinition_Error (Prag : Node_Id) is
+ Mode : constant Name_Id :=
+ Chars (Get_Pragma_Arg (First
+ (Pragma_Argument_Associations (Prag))));
+ begin
+ Error_Msg_Name_1 := Mode;
+ Error_Msg_Sloc := Sloc (Prag);
+ Error_Msg_N
+ ("cannot redefine 'S'P'A'R'K mode, already set to % #", Arg1);
+ end Redefinition_Error;
+
+ -- Local variables
+
+ Body_Id : Entity_Id;
+ Context : Node_Id;
+ Mode : Name_Id;
+ Mode_Id : SPARK_Mode_Id;
+ Spec_Id : Entity_Id;
+ Stmt : Node_Id;
+ Unit_Prag : Node_Id;
+
+ -- Start of processing for SPARK_Mode
+
+ begin
+ GNAT_Pragma;
+ Check_No_Identifiers;
+ Check_At_Most_N_Arguments (1);
+
+ -- Check the legality of the mode
+
+ if Arg_Count = 1 then
+ Check_Arg_Is_One_Of (Arg1, Name_On, Name_Off, Name_Auto);
+ Mode := Chars (Get_Pragma_Arg (Arg1));
+
+ -- A SPARK_Mode without an argument defaults to "On"
+
+ else
+ Mode := Name_On;
+ end if;
+
+ Mode_Id := Get_SPARK_Mode_Id (Mode);
+ Context := Parent (N);
+
+ -- The pragma appears in a configuration file
+
+ if No (Context) then
+ Check_Valid_Configuration_Pragma;
+
+ -- Set the global mode
+
+ if Global_SPARK_Mode = None then
+ Global_SPARK_Mode := Mode_Id;
+
+ -- Catch an attempt to redefine an existing global mode by
+ -- using multiple configuration files.
+
+ elsif Global_SPARK_Mode /= Mode_Id then
+ Redefinition_Error (Global_SPARK_Mode);
+ end if;
+
+ -- When the pragma is placed before the declaration of a unit, it
+ -- configures the whole unit.
+
+ elsif Nkind (Context) = N_Compilation_Unit then
+ Check_Valid_Configuration_Pragma;
+
+ Unit_Prag := SPARK_Mode_Pragma (Current_Sem_Unit);
+
+ -- Set the unit mode
+
+ if No (Unit_Prag) then
+ Set_SPARK_Mode_Pragma (Current_Sem_Unit, N);
+
+ -- Catch an attempt to redefine the unit mode by using multiple
+ -- pragmas declared in the same region.
+
+ else
+ Redefinition_Error (Unit_Prag);
+ end if;
+
+ -- The pragma applies to a [library unit] subprogram or package
+
+ else
+ -- Mode "Auto" cannot be used in nested subprograms or packages
+
+ if Mode_Id = SPARK_Auto then
+ Error_Pragma_Arg
+ ("mode `Auto` can only apply to the configuration variant "
+ & "of pragma %", Arg1);
+ end if;
+
+ -- Verify the placement of the pragma with respect to package
+ -- or subprogram declarations and detect duplicates.
+
+ Stmt := Prev (N);
+ while Present (Stmt) loop
+
+ -- Skip prior pragmas, but check for duplicates
+
+ if Nkind (Stmt) = N_Pragma then
+ if Pragma_Name (Stmt) = Pname then
+ Error_Msg_Name_1 := Pname;
+ Error_Msg_Sloc := Sloc (Stmt);
+ Error_Msg_N
+ ("pragma % duplicates pragma declared #", N);
+ end if;
+
+ -- Skip internally generated code
+
+ elsif not Comes_From_Source (Stmt) then
+ null;
+
+ -- The pragma applies to a package or subprogram declaration
+
+ elsif Nkind_In (Stmt, N_Generic_Package_Declaration,
+ N_Generic_Subprogram_Declaration,
+ N_Package_Declaration,
+ N_Subprogram_Declaration)
+ then
+ Spec_Id := Defining_Unit_Name (Specification (Stmt));
+ Chain_Pragma (Spec_Id, N);
+ return;
+
+ -- The pragma does not apply to a legal construct, issue an
+ -- error and stop the analysis.
+
+ else
+ Pragma_Misplaced;
+ exit;
+ end if;
+
+ Stmt := Prev (Stmt);
+ end loop;
+
+ -- If we get here, then we ran out of preceding statements. The
+ -- pragma is immediately within a body.
+
+ if Nkind_In (Context, N_Package_Body,
+ N_Subprogram_Body)
+ then
+ Spec_Id := Corresponding_Spec (Context);
+
+ if Nkind (Context) = N_Subprogram_Body then
+ Context := Specification (Context);
+ end if;
+
+ Body_Id := Defining_Unit_Name (Context);
+
+ Chain_Pragma (Body_Id, N);
+ Check_Conformance (Spec_Id, Body_Id);
+
+ -- The pragma is at the top level of a package spec
+
+ elsif Nkind (Context) = N_Package_Specification then
+ Spec_Id := Defining_Unit_Name (Context);
+ Chain_Pragma (Spec_Id, N);
+
+ -- The pragma applies to the statements of a package body
+
+ elsif Nkind (Context) = N_Handled_Sequence_Of_Statements
+ and then Nkind (Parent (Context)) = N_Package_Body
+ then
+ Context := Parent (Context);
+ Spec_Id := Corresponding_Spec (Context);
+ Body_Id := Defining_Unit_Name (Context);
+
+ Chain_Pragma (Body_Id, N);
+ Check_Conformance (Spec_Id, Body_Id);
+
+ -- The pragma does not apply to a legal construct, issue an
+ -- error.
+
+ else
+ Pragma_Misplaced;
+ end if;
+ end if;
+ end SPARK_Mod;
+
--------------------------------
-- Static_Elaboration_Desired --
--------------------------------
return Result;
end Get_Base_Subprogram;
+ -----------------------
+ -- Get_SPARK_Mode_Id --
+ -----------------------
+
+ function Get_SPARK_Mode_Id (N : Name_Id) return SPARK_Mode_Id is
+ begin
+ if N = Name_On then
+ return SPARK_On;
+ elsif N = Name_Off then
+ return SPARK_Off;
+ elsif N = Name_Auto then
+ return SPARK_Auto;
+
+ -- Any other argument is erroneous
+
+ else
+ raise Program_Error;
+ end if;
+ end Get_SPARK_Mode_Id;
+
+ -----------------------
+ -- Get_SPARK_Mode_Id --
+ -----------------------
+
+ function Get_SPARK_Mode_Id (N : Node_Id) return SPARK_Mode_Id is
+ Mode : Node_Id;
+
+ begin
+ pragma Assert
+ (Nkind (N) = N_Pragma
+ and then Present (Pragma_Argument_Associations (N)));
+
+ Mode := First (Pragma_Argument_Associations (N));
+
+ return Get_SPARK_Mode_Id (Chars (Get_Pragma_Arg (Mode)));
+ end Get_SPARK_Mode_Id;
+
----------------
-- Initialize --
----------------
-- Start of processing for Is_Config_Static_String
begin
-
Name_Len := 0;
+
return Add_Config_Static_String (Arg);
end Is_Config_Static_String;
+ -------------------------------
+ -- Is_Elaboration_SPARK_Mode --
+ -------------------------------
+
+ function Is_Elaboration_SPARK_Mode (N : Node_Id) return Boolean is
+ begin
+ pragma Assert
+ (Nkind (N) = N_Pragma
+ and then Pragma_Name (N) = Name_SPARK_Mode
+ and then Is_List_Member (N));
+
+ -- Pragma SPARK_Mode affects the elaboration of a package body when it
+ -- appears in the statement part of the body.
+
+ return
+ Present (Parent (N))
+ and then Nkind (Parent (N)) = N_Handled_Sequence_Of_Statements
+ and then List_Containing (N) = Statements (Parent (N))
+ and then Present (Parent (Parent (N)))
+ and then Nkind (Parent (Parent (N))) = N_Package_Body;
+ end Is_Elaboration_SPARK_Mode;
+
-----------------------------------------
-- Is_Non_Significant_Pragma_Reference --
-----------------------------------------
Pragma_Source_File_Name => -1,
Pragma_Source_File_Name_Project => -1,
Pragma_Source_Reference => -1,
+ Pragma_SPARK_Mode => 0,
Pragma_Storage_Size => -1,
Pragma_Storage_Unit => -1,
Pragma_Static_Elaboration_Desired => -1,
end if;
end Is_Pragma_String_Literal;
+ ---------------------------
+ -- Is_Private_SPARK_Mode --
+ ---------------------------
+
+ function Is_Private_SPARK_Mode (N : Node_Id) return Boolean is
+ begin
+ pragma Assert
+ (Nkind (N) = N_Pragma
+ and then Pragma_Name (N) = Name_SPARK_Mode
+ and then Is_List_Member (N));
+
+ -- For pragma SPARK_Mode to be private, it has to appear in the private
+ -- declarations of a package.
+
+ return
+ Present (Parent (N))
+ and then Nkind (Parent (N)) = N_Package_Specification
+ and then List_Containing (N) = Private_Declarations (Parent (N));
+ end Is_Private_SPARK_Mode;
+
-----------------------------
-- Is_Valid_Assertion_Kind --
-----------------------------
-- True have their analysis delayed until after the main program is parsed
-- and analyzed.
+ function Get_SPARK_Mode_Id (N : Node_Id) return SPARK_Mode_Id;
+ -- Given a pragma SPARK_Mode node, return the corresponding mode id
+
procedure Initialize;
-- Initializes data structures used for pragma processing. Must be called
-- before analyzing each new main source program.
-- length, and then returns True. If it is not of the correct form, then an
-- appropriate error message is posted, and False is returned.
+ function Is_Elaboration_SPARK_Mode (N : Node_Id) return Boolean;
+ -- Determine whether pragma SPARK_Mode appears in the statement part of a
+ -- package body.
+
function Is_Non_Significant_Pragma_Reference (N : Node_Id) return Boolean;
-- The node N is a node for an entity and the issue is whether the
-- occurrence is a reference for the purposes of giving warnings about
-- False is returned, then the argument is treated as an entity reference
-- to the operator.
+ function Is_Private_SPARK_Mode (N : Node_Id) return Boolean;
+ -- Determine whether pragma SPARK_Mode appears in the private part of a
+ -- package.
+
function Is_Valid_Assertion_Kind (Nam : Name_Id) return Boolean;
-- Returns True if Nam is one of the names recognized as a valid assertion
-- kind by the Assertion_Policy pragma. Note that the 'Class cases are
-- Used by processing for Pre/Postcondition pragmas to store a list of
-- pragmas associated with the spec of a subprogram (see Sem_Prag for
-- details).
+ --
+ -- Used by processing for pragma SPARK_Mode to store multiple pragmas
+ -- the apply to the same construct. These are visible/private mode for
+ -- a package spec and declarative/statement mode for package body.
-- Next_Rep_Item (Node5-Sem)
-- Present in pragma nodes, attribute definition nodes, enumeration rep
Name_Short_Descriptors : constant Name_Id := N + $; -- GNAT
Name_Source_File_Name : constant Name_Id := N + $; -- GNAT
Name_Source_File_Name_Project : constant Name_Id := N + $; -- GNAT
+ Name_SPARK_Mode : constant Name_Id := N + $; -- GNAT
Name_Style_Checks : constant Name_Id := N + $; -- GNAT
Name_Suppress : constant Name_Id := N + $;
Name_Suppress_Exception_Locations : constant Name_Id := N + $; -- GNAT
Name_Assertion : constant Name_Id := N + $;
Name_Assertions : constant Name_Id := N + $;
Name_Attribute_Name : constant Name_Id := N + $;
+ Name_Auto : constant Name_Id := N + $;
Name_Body_File_Name : constant Name_Id := N + $;
Name_Boolean_Entry_Barriers : constant Name_Id := N + $;
Name_By_Any : constant Name_Id := N + $;
Pragma_Short_Descriptors,
Pragma_Source_File_Name,
Pragma_Source_File_Name_Project,
+ Pragma_SPARK_Mode,
Pragma_Style_Checks,
Pragma_Suppress,
Pragma_Suppress_Exception_Locations,
SE_Empty_Storage_Pool ..
SE_Object_Too_Large;
+ ----------------------------------------
+ -- Types Used for SPARK Mode Handling --
+ ----------------------------------------
+
+ type SPARK_Mode_Id is (None, SPARK_Off, SPARK_Auto, SPARK_On);
+ -- Type used to represent all legal modes that can be set by aspect/pragma
+ -- SPARK_Mode.
+
end Types;
projects / platform / upstream / gcc.git / commitdiff