diff options
| -rw-r--r-- | gcc/ada/ChangeLog | 57 | ||||
| -rw-r--r-- | gcc/ada/aspects.adb | 1 | ||||
| -rw-r--r-- | gcc/ada/aspects.ads | 3 | ||||
| -rw-r--r-- | gcc/ada/atree.adb | 12 | ||||
| -rw-r--r-- | gcc/ada/atree.ads | 6 | ||||
| -rw-r--r-- | gcc/ada/einfo.adb | 43 | ||||
| -rw-r--r-- | gcc/ada/einfo.ads | 14 | ||||
| -rw-r--r-- | gcc/ada/gnat_rm.texi | 87 | ||||
| -rw-r--r-- | gcc/ada/gnat_ugn.texi | 1 | ||||
| -rw-r--r-- | gcc/ada/lib-load.adb | 137 | ||||
| -rw-r--r-- | gcc/ada/lib-writ.adb | 90 | ||||
| -rw-r--r-- | gcc/ada/lib.adb | 12 | ||||
| -rw-r--r-- | gcc/ada/lib.ads | 242 | ||||
| -rw-r--r-- | gcc/ada/opt.ads | 26 | ||||
| -rw-r--r-- | gcc/ada/par-prag.adb | 1 | ||||
| -rw-r--r-- | gcc/ada/sem_ch13.adb | 11 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 432 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.ads | 11 | ||||
| -rw-r--r-- | gcc/ada/sinfo.ads | 4 | ||||
| -rw-r--r-- | gcc/ada/snames.ads-tmpl | 3 | ||||
| -rw-r--r-- | gcc/ada/types.ads | 8 |
21 files changed, 958 insertions, 243 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 6bec4e8..5d222e7 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,60 @@ +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 diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb index 71f7493..d02edb2 100644 --- a/gcc/ada/aspects.adb +++ b/gcc/ada/aspects.adb @@ -403,6 +403,7 @@ package body Aspects is 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, diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads index 6941cc1..5a093af 100644 --- a/gcc/ada/aspects.ads +++ b/gcc/ada/aspects.ads @@ -116,6 +116,7 @@ package Aspects is Aspect_Simple_Storage_Pool, -- GNAT Aspect_Size, Aspect_Small, + Aspect_SPARK_Mode, -- GNAT Aspect_Static_Predicate, Aspect_Storage_Pool, Aspect_Storage_Size, @@ -322,6 +323,7 @@ package Aspects is 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, @@ -423,6 +425,7 @@ package Aspects is 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, diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb index 40a27a1..a6105e2 100644 --- a/gcc/ada/atree.adb +++ b/gcc/ada/atree.adb @@ -2532,6 +2532,12 @@ package body Atree is 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); @@ -5243,6 +5249,12 @@ package body Atree is 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); diff --git a/gcc/ada/atree.ads b/gcc/ada/atree.ads index 07e8e51..d1056b0 100644 --- a/gcc/ada/atree.ads +++ b/gcc/ada/atree.ads @@ -1174,6 +1174,9 @@ package Atree is 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); @@ -2459,6 +2462,9 @@ package Atree is 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); diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index bfe5b37..bca2044 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -246,7 +246,7 @@ package body Einfo is -- Thunk_Entity Node31 - -- (unused) Node32 + -- SPARK_Mode_Pragmas Node32 -- (unused) Node33 @@ -2825,6 +2825,21 @@ package body Einfo is 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)); @@ -5469,6 +5484,22 @@ package body Einfo is 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)); @@ -9149,6 +9180,16 @@ package body Einfo is 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; diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index a3d05d8..0df2880 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -3757,6 +3757,11 @@ package Einfo is -- 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 @@ -5394,6 +5399,7 @@ package Einfo is -- 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) @@ -5591,6 +5597,7 @@ package Einfo is -- 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) @@ -5621,6 +5628,7 @@ package Einfo is -- 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) @@ -5667,6 +5675,7 @@ package Einfo is -- 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) @@ -5837,6 +5846,7 @@ package Einfo is -- Last_Entity (Node20) -- Scope_Depth_Value (Uint22) -- Extra_Formals (Node28) + -- SPARK_Mode_Pragmas (Node32) -- Scope_Depth (synth) -- E_Subprogram_Type @@ -6531,6 +6541,7 @@ package Einfo is 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; @@ -7145,6 +7156,7 @@ package Einfo is 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); @@ -7891,6 +7903,7 @@ package Einfo is 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); @@ -8305,6 +8318,7 @@ package Einfo is 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); diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index 1943009..4b0c37c 100644 --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -232,6 +232,7 @@ Implementation Defined Pragmas * 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:: @@ -290,6 +291,7 @@ Implementation Defined Aspects * Aspect Shared:: * Aspect Simple_Storage_Pool:: * Aspect Simple_Storage_Pool_Type:: +* Aspect SPARK_Mode:: * Aspect Suppress_Debug_Info:: * Aspect Test_Case:: * Aspect Universal_Aliasing:: @@ -1044,6 +1046,7 @@ consideration, the use of these pragmas should be minimized. * 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:: @@ -5996,6 +5999,80 @@ The second argument must be a string literal, it cannot be a static 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 @@ -6048,8 +6125,7 @@ of this type. It must name a function whose argument type may be any 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 @@ -7180,6 +7256,7 @@ clause. * Aspect Shared:: * Aspect Simple_Storage_Pool:: * Aspect Simple_Storage_Pool_Type:: +* Aspect SPARK_Mode:: * Aspect Suppress_Debug_Info:: * Aspect Test_Case:: * Aspect Universal_Aliasing:: @@ -7433,6 +7510,12 @@ attribute definition clause. @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 diff --git a/gcc/ada/gnat_ugn.texi b/gcc/ada/gnat_ugn.texi index 5a6b6af..86eb6b3 100644 --- a/gcc/ada/gnat_ugn.texi +++ b/gcc/ada/gnat_ugn.texi @@ -11611,6 +11611,7 @@ recognized by GNAT: Short_Circuit_And_Or Source_File_Name Source_File_Name_Project + SPARK_Mode Style_Checks Suppress Suppress_Exception_Locations diff --git a/gcc/ada/lib-load.adb b/gcc/ada/lib-load.adb index be4c537..6d65c81 100644 --- a/gcc/ada/lib-load.adb +++ b/gcc/ada/lib-load.adb @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -206,28 +206,29 @@ package body Lib.Load is 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); @@ -312,28 +313,29 @@ package body Lib.Load is 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; @@ -675,28 +677,29 @@ package body Lib.Load is 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 diff --git a/gcc/ada/lib-writ.adb b/gcc/ada/lib-writ.adb index e786f47..e5c0912 100644 --- a/gcc/ada/lib-writ.adb +++ b/gcc/ada/lib-writ.adb @@ -71,28 +71,29 @@ package body Lib.Writ is 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; ------------------------------ @@ -128,28 +129,29 @@ package body Lib.Writ is 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. diff --git a/gcc/ada/lib.adb b/gcc/ada/lib.adb index fc62239..e220b20 100644 --- a/gcc/ada/lib.adb +++ b/gcc/ada/lib.adb @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -166,6 +166,11 @@ package body Lib is 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; @@ -254,6 +259,11 @@ package body Lib is 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; diff --git a/gcc/ada/lib.ads b/gcc/ada/lib.ads index f2cc330..eb10a8b 100644 --- a/gcc/ada/lib.ads +++ b/gcc/ada/lib.ads @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -265,38 +265,6 @@ package Lib is -- 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 @@ -320,6 +288,19 @@ package Lib is -- 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 @@ -335,6 +316,10 @@ package Lib is -- 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 @@ -366,9 +351,9 @@ package Lib is -- 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 @@ -381,6 +366,25 @@ package Lib is -- 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 @@ -404,43 +408,45 @@ package Lib is 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). @@ -707,34 +713,37 @@ private 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 @@ -742,31 +751,32 @@ private -- 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 ( diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads index 54d39f8..a4cbafd 100644 --- a/gcc/ada/opt.ads +++ b/gcc/ada/opt.ads @@ -1970,6 +1970,21 @@ package Opt is -- 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 @@ -1978,22 +1993,11 @@ package Opt is -- 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" diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index 3587dff..07242fb 100644 --- a/gcc/ada/par-prag.adb +++ b/gcc/ada/par-prag.adb @@ -1262,6 +1262,7 @@ begin 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 | diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 0eb18f1..5378fa3 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -1659,6 +1659,16 @@ package body Sem_Ch13 is 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 => @@ -7390,6 +7400,7 @@ package body Sem_Ch13 is Aspect_Postcondition | Aspect_Pre | Aspect_Precondition | + Aspect_SPARK_Mode | Aspect_Test_Case => raise Program_Error; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 08d6f9a..36c3d7f 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -213,6 +213,11 @@ package body Sem_Prag is -- 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 @@ -16315,6 +16320,351 @@ package body Sem_Prag is 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 -- -------------------------------- @@ -18268,6 +18618,43 @@ package body Sem_Prag is 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 -- ---------------- @@ -18332,11 +18719,33 @@ package body Sem_Prag is -- 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 -- ----------------------------------------- @@ -18524,6 +18933,7 @@ package body Sem_Prag is 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, @@ -18682,6 +19092,26 @@ package body Sem_Prag is 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 -- ----------------------------- diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index 3b8a3bc..fcbe988 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -113,6 +113,9 @@ package Sem_Prag is -- 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. @@ -127,6 +130,10 @@ package Sem_Prag is -- 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 @@ -143,6 +150,10 @@ package Sem_Prag is -- 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 diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index 2879579..f66aeee 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -1539,6 +1539,10 @@ package Sinfo is -- 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 diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index ef983a7..bfe21bd 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -436,6 +436,7 @@ package Snames is 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 @@ -673,6 +674,7 @@ package Snames is 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 + $; @@ -1748,6 +1750,7 @@ package Snames is Pragma_Short_Descriptors, Pragma_Source_File_Name, Pragma_Source_File_Name_Project, + Pragma_SPARK_Mode, Pragma_Style_Checks, Pragma_Suppress, Pragma_Suppress_Exception_Locations, diff --git a/gcc/ada/types.ads b/gcc/ada/types.ads index ec723dd..4bbaa6b 100644 --- a/gcc/ada/types.ads +++ b/gcc/ada/types.ads @@ -876,4 +876,12 @@ package Types is 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; |