diff options
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 18 | ||||
| -rw-r--r-- | gcc/ada/debug.adb | 25 | ||||
| -rw-r--r-- | gcc/ada/exp_prag.adb | 13 | ||||
| -rw-r--r-- | gcc/ada/frontend.adb | 7 | ||||
| -rw-r--r-- | gcc/ada/gnat_rm.texi | 69 | ||||
| -rw-r--r-- | gcc/ada/par-prag.adb | 2 | ||||
| -rw-r--r-- | gcc/ada/sem_ch13.adb | 1 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 51 | ||||
| -rw-r--r-- | gcc/ada/snames.ads-tmpl | 8 |
9 files changed, 154 insertions, 40 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 1c86e5ccf18..e5fcfaca1bd 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,21 @@ +2013-10-14 Robert Dewar <dewar@adacore.com> + + * exp_prag.adb (Expand_Pragma_Check): Generate proper string + for invariant + * gnat_rm.texi: Add documentation for pragmas + Type_Invariant[_Class] + * par-prag.adb: Add entries for pragmas Type_Invariant[_Class] + * sem_ch13.adb: Minor reformatting + * sem_prag.adb: Implement pragmas Type_Invariant[_Class] + * snames.ads-tmpl: Add entries for pragmas Type_Invariant[_Class] + +2013-10-14 Johannes Kanig <kanig@adacore.com> + + * debug.adb: Release now unused debug switches that were only + relevant for gnat2why backend, not the frontend + * frontend.adb (Frontend) Do not stop when -gnatd.H is present, + was unused + 2013-10-14 Hristian Kirtchev <kirtchev@adacore.com> * sem_prag.adb (Analyze_Global_Item): Allow diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index 8775af7090f..5364574421b 100644 --- a/gcc/ada/debug.adb +++ b/gcc/ada/debug.adb @@ -125,16 +125,16 @@ package body Debug is -- d.E -- d.F SPARK mode -- d.G Frame condition mode for gnat2why - -- d.H Standard package only mode for gnat2why + -- d.H -- d.I Do not ignore enum representation clauses in CodePeer mode -- d.J Disable parallel SCIL generation mode - -- d.K SPARK check mode for gnat2why + -- d.K -- d.L Depend on back end for limited types in if and case expressions -- d.M Relaxed RM semantics -- d.N Add node to all entities -- d.O Dump internal SCO tables -- d.P Previous (non-optimized) handling of length comparisons - -- d.Q Flow Analysis mode for gnat2why + -- d.Q -- d.R Restrictions in ali files in positional form -- d.S Force Optimize_Alignment (Space) -- d.T Force Optimize_Alignment (Time) @@ -143,7 +143,7 @@ package body Debug is -- d.W Print out debugging information for Walk_Library_Items -- d.X -- d.Y - -- d.Z Dump flow analysis graphs, for debugging purposes (gnat2why) + -- d.Z -- d1 Error msgs have node numbers where possible -- d2 Eliminate error flags in verbose form error messages @@ -596,7 +596,7 @@ package body Debug is -- d.D SPARK strict mode. Interpret compiler permissions as strictly as -- possible in SPARK mode. - + -- -- d.F SPARK mode. Generate AST in a form suitable for formal -- verification, as well as additional cross reference information in -- ALI files to compute effects of subprograms. Note that ALI files @@ -606,10 +606,6 @@ package body Debug is -- generate Why code. Instead, it generates ALI files with an extra -- section which contains the effects of subprograms. - -- d.H Standard package only mode for gnat2why. In this mode, gnat2why - -- will only generate Why code for package Standard. Any given input - -- file will be ignored. - -- d.I Do not ignore enum representation clauses in CodePeer mode. -- The default of ignoring representation clauses for enumeration -- types in CodePeer is good for the majority of Ada code, but in some @@ -620,9 +616,6 @@ package body Debug is -- done in parallel to speed processing. This switch disables this -- behavior. - -- d.K SPARK check mode for gnat2why. In this mode, gnat2why does not - -- generate Why code. - -- d.L Normally the front end generates special expansion for conditional -- expressions of a limited type. This debug flag removes this special -- case expansion, leaving it up to the back end to handle conditional @@ -644,9 +637,6 @@ package body Debug is -- This is there in case we find a situation where the optimization -- malfunctions, to provide a work around. - -- d.Q Flow Analysis mode for gnat2why. When this flag is given, - -- gnat2why will do flow analysis, and no translation to Why is done. - -- d.R As documented in lib-writ.ads, restrictions in the ali file can -- have two forms, positional and named. The named notation is the -- current preferred form, but the use of this debug switch will force @@ -671,11 +661,6 @@ package body Debug is -- the order in which units are walked. This is primarily for use in -- debugging CodePeer mode. - -- d.Z In gnat2why, in Flow analysis mode (-gnatd.Q), dump the different - -- graphs (control flow, control dependence) for debugging purposes. - -- This debug flag will be removed when flow analysis is sufficiently - -- stable. - -- d.Y Prevents the use of the N_Expression_With_Actions node even in the -- case of the gcc back end. Provided as a back up in case the new -- scheme has problems. diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb index eeafa72d356..5544e471949 100644 --- a/gcc/ada/exp_prag.adb +++ b/gcc/ada/exp_prag.adb @@ -311,6 +311,10 @@ package body Exp_Prag is -- at" is omitted for name = Assertion, since it is redundant, given -- that the name of the exception is Assert_Failure.) + -- Also, instead of "XXX failed at", we generate slightly + -- different messages for some of the contract assertions (see + -- code below for details). + -- An alternative expansion is used when the No_Exception_Propagation -- restriction is active and there is a local Assert_Failure handler. -- This is not a common combination of circumstances, but it occurs in @@ -400,6 +404,15 @@ package body Exp_Prag is Insert_Str_In_Name_Buffer ("failed ", 1); Add_Str_To_Name_Buffer (" from "); + -- For special case of Invariant, the string is "failed + -- invariant from yy", to be consistent with the string that is + -- generated for the aspect case (the code later on checks for + -- this specific string to modify it in some cases, so this is + -- functionally important). + + elsif Nam = Name_Invariant then + Add_Str_To_Name_Buffer ("failed invariant from "); + -- For all other checks, the string is "xxx failed at yyy" -- where xxx is the check name with current source file casing. diff --git a/gcc/ada/frontend.adb b/gcc/ada/frontend.adb index 7c56ac9789f..8a64134d91d 100644 --- a/gcc/ada/frontend.adb +++ b/gcc/ada/frontend.adb @@ -99,13 +99,6 @@ begin CStand.Create_Standard; - -- If the -gnatd.H flag is present, we are only interested in the Standard - -- package, so the frontend has done its job here. - - if Debug_Flag_Dot_HH then - return; - end if; - -- Check possible symbol definitions specified by -gnateD switches Prepcomp.Process_Command_Line_Symbol_Definitions; diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index 833922e4650..9ea370b2c78 100644 --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -253,6 +253,8 @@ Implementation Defined Pragmas * Pragma Thread_Local_Storage:: * Pragma Time_Slice:: * Pragma Title:: +* Pragma Type_Invariant:: +* Pragma Type_Invariant_Class:: * Pragma Unchecked_Union:: * Pragma Unimplemented_Unit:: * Pragma Universal_Aliasing :: @@ -1073,6 +1075,8 @@ consideration, the use of these pragmas should be minimized. * Pragma Thread_Local_Storage:: * Pragma Time_Slice:: * Pragma Title:: +* Pragma Type_Invariant:: +* Pragma Type_Invariant_Class:: * Pragma Unchecked_Union:: * Pragma Unimplemented_Unit:: * Pragma Universal_Aliasing :: @@ -5367,6 +5371,21 @@ subtype Q is R with Dynamic_Predicate => F(Q) or G(Q); @end smallexample +Note that there is are no pragmas @code{Dynamic_Predicate} +or @code{Static_Predicate}. That is +because these pragmas would affect legality and semantics of +the program and thus do not have a neutral effect if ignored. +The motivation behind providing pragmas equivalent to +corresponding aspects is to allow a program to be written +using the pragmas, and then compiled with a compiler that +will ignore the pragmas. That doesn't work in the case of +static and dynamic predicates, since if the corresponding +pragmas are ignored, then the behavior of the program is +fundamentally changed (for example a membership test +@code{A in B} would not take into account a predicate +defined for subtype B). When following this approach, the +use of predicates should be avoided. + @node Pragma Preelaborable_Initialization @unnumberedsec Pragma Preelaborable_Initialization @findex Preelaborable_Initialization @@ -6786,6 +6805,56 @@ for this pragma, i.e.@: the parameters may be given in any order if named notation is used, and named and positional notation can be mixed following the normal rules for procedure calls in Ada. +@node Pragma Type_Invariant +@unnumberedsec Pragma Type_Invariant +@findex Invariant +@findex Type_Invariant pragma +@noindent +Syntax: + +@smallexample @c ada +pragma Type_Invariant + ([Entity =>] type_LOCAL_NAME, + [Check =>] EXPRESSION); +@end smallexample + +@noindent +The @code{Type_Invariant} pragma is intended to be an exact +replacement for the language-defined @code{Type_Invariant} +aspect, and shares its restrictions and semantics. It differs +from the language defined @code{Invariant} pragma in that it +does not permit a string parameter, and it is +controlled by the assertion identifier @code{Type_Invariant} +rather than @code{Invariant}. + +@node Pragma Type_Invariant_Class +@unnumberedsec Pragma Type_Invariant_Class +@findex Invariant +@findex Type_Invariant_Class pragma +@noindent +Syntax: + +@smallexample @c ada +pragma Type_Invariant_Class + ([Entity =>] type_LOCAL_NAME, + [Check =>] EXPRESSION); +@end smallexample + +@noindent +The @code{Type_Invariant_Class} pragma is intended to be an exact +replacement for the language-defined @code{Type_Invariant'Class} +aspect, and shares its restrictions and semantics. + +Note: This pragma is called @code{Type_Invariant_Class} rather than +@code{Type_Invariant'Class} because the latter would not be strictly +conforming to the allowed syntax for pragmas. The motivation +for providing pragmas equivalent to the aspects is to allow a program +to be written using the pragmas, and then compiled if necessary +using an Ada compiler that does not recognize the pragmas or +aspects, but is prepared to ignore the pragmas. The assertion +policy that controls this pragma is @code{Type_Invariant'Class}, +not @code{Type_Invariant_Class}. + @node Pragma Unchecked_Union @unnumberedsec Pragma Unchecked_Union @cindex Unions in C diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index 22e79d78921..a965e12972c 100644 --- a/gcc/ada/par-prag.adb +++ b/gcc/ada/par-prag.adb @@ -1293,6 +1293,8 @@ begin Pragma_Thread_Local_Storage | Pragma_Time_Slice | Pragma_Title | + Pragma_Type_Invariant | + Pragma_Type_Invariant_Class | Pragma_Unchecked_Union | Pragma_Unimplemented_Unit | Pragma_Universal_Aliasing | diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 29fc1c79382..c584560b22f 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -5961,7 +5961,6 @@ package body Sem_Ch13 is if Present (SId) then PDecl := Unit_Declaration_Node (SId); - else PDecl := Build_Invariant_Procedure_Declaration (Typ); end if; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 09c0473cc7b..30816d5ee0e 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -846,7 +846,7 @@ package body Sem_Prag is if Is_Input then if (Ekind (Item_Id) = E_Out_Parameter - and then not Is_Unconstrained_Or_Tagged_Item (Item_Id)) + and then not Is_Unconstrained_Or_Tagged_Item (Item_Id)) or else (Global_Seen and then not Appears_In (Subp_Inputs, Item_Id)) then @@ -11772,7 +11772,6 @@ package body Sem_Prag is Name_Link_Name)); Check_At_Least_N_Arguments (2); - Check_At_Most_N_Arguments (4); Process_Convention (C, Def_Id); @@ -13716,7 +13715,7 @@ package body Sem_Prag is begin GNAT_Pragma; Check_At_Least_N_Arguments (2); - Check_At_Most_N_Arguments (3); + Check_At_Most_N_Arguments (3); Check_Optional_Identifier (Arg1, Name_Entity); Check_Optional_Identifier (Arg2, Name_Check); @@ -15316,7 +15315,7 @@ package body Sem_Prag is begin GNAT_Pragma; Check_At_Least_N_Arguments (1); - Check_At_Most_N_Arguments (2); + Check_At_Most_N_Arguments (2); -- Process first argument @@ -15700,11 +15699,13 @@ package body Sem_Prag is begin GNAT_Pragma; - Check_At_Least_N_Arguments (1); - Check_At_Most_N_Arguments (1); + Check_Arg_Count (1); Check_No_Identifiers; Check_Pre_Post; + -- Rewrite Post[_Class] pragma as Precondition pragma setting the + -- flag Class_Present to True for the Post_Class case. + Set_Class_Present (N, Prag_Id = Pragma_Pre_Class); PC_Pragma := New_Copy (N); Set_Pragma_Identifier @@ -15760,11 +15761,13 @@ package body Sem_Prag is begin GNAT_Pragma; - Check_At_Least_N_Arguments (1); - Check_At_Most_N_Arguments (1); + Check_Arg_Count (1); Check_No_Identifiers; Check_Pre_Post; + -- Rewrite Pre[_Class] pragma as Precondition pragma setting the + -- flag Class_Present to True for the Pre_Class case. + Set_Class_Present (N, Prag_Id = Pragma_Pre_Class); PC_Pragma := New_Copy (N); Set_Pragma_Identifier @@ -15787,7 +15790,7 @@ package body Sem_Prag is begin GNAT_Pragma; Check_At_Least_N_Arguments (1); - Check_At_Most_N_Arguments (2); + Check_At_Most_N_Arguments (2); Check_Optional_Identifier (Arg1, Name_Check); Check_Precondition_Postcondition (In_Body); @@ -18317,6 +18320,34 @@ package body Sem_Prag is end loop; end Title; + ---------------------------- + -- Type_Invariant[_Class] -- + ---------------------------- + + -- pragma Type_Invariant[_Class] + -- ([Entity =>] type_LOCAL_NAME, + -- [Check =>] EXPRESSION); + + when Pragma_Type_Invariant | + Pragma_Type_Invariant_Class => + Type_Invariant : declare + I_Pragma : Node_Id; + + begin + Check_Arg_Count (2); + + -- Rewrite Type_Invariant[_Class] pragma as an Invariant pragma, + -- setting Class_Present for the Type_Invariant_Class case. + + Set_Class_Present (N, Prag_Id = Pragma_Type_Invariant_Class); + I_Pragma := New_Copy (N); + Set_Pragma_Identifier + (I_Pragma, Make_Identifier (Loc, Name_Invariant)); + Rewrite (N, I_Pragma); + Set_Analyzed (N, False); + Analyze (N); + end Type_Invariant; + --------------------- -- Unchecked_Union -- --------------------- @@ -21493,6 +21524,8 @@ package body Sem_Prag is Pragma_Thread_Local_Storage => 0, Pragma_Time_Slice => -1, Pragma_Title => -1, + Pragma_Type_Invariant => -1, + Pragma_Type_Invariant_Class => -1, Pragma_Unchecked_Union => 0, Pragma_Unimplemented_Unit => -1, Pragma_Universal_Aliasing => -1, diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index 0a5d9460e36..cca70eb9a7c 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -144,8 +144,6 @@ package Snames is Name_Dynamic_Predicate : constant Name_Id := N + $; Name_Static_Predicate : constant Name_Id := N + $; Name_Synchronization : constant Name_Id := N + $; - Name_Type_Invariant : constant Name_Id := N + $; - Name_Type_Invariant_Class : constant Name_Id := N + $; -- Some special names used by the expander. Note that the lower case u's -- at the start of these names get translated to extra underscores. These @@ -448,7 +446,7 @@ package Snames is Name_Wide_Character_Encoding : constant Name_Id := N + $; -- GNAT Last_Configuration_Pragma_Name : constant Name_Id := N + $; - -- Remaining pragma names + -- Remaining pragma names (non-configuration pragmas) Name_Abort_Defer : constant Name_Id := N + $; -- GNAT Name_Abstract_State : constant Name_Id := N + $; -- GNAT @@ -621,6 +619,8 @@ package Snames is Name_Thread_Local_Storage : constant Name_Id := N + $; -- GNAT Name_Time_Slice : constant Name_Id := N + $; -- GNAT Name_Title : constant Name_Id := N + $; -- GNAT + Name_Type_Invariant : constant Name_Id := N + $; -- GNAT + Name_Type_Invariant_Class : constant Name_Id := N + $; -- GNAT Name_Unchecked_Union : constant Name_Id := N + $; -- Ada 05 Name_Unimplemented_Unit : constant Name_Id := N + $; -- GNAT Name_Universal_Aliasing : constant Name_Id := N + $; -- GNAT @@ -1905,6 +1905,8 @@ package Snames is Pragma_Thread_Local_Storage, Pragma_Time_Slice, Pragma_Title, + Pragma_Type_Invariant, + Pragma_Type_Invariant_Class, Pragma_Unchecked_Union, Pragma_Unimplemented_Unit, Pragma_Universal_Aliasing, |