diff options
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 31 | ||||
| -rw-r--r-- | gcc/ada/gnat_rm.texi | 2 | ||||
| -rw-r--r-- | gcc/ada/gnat_ugn.texi | 34 | ||||
| -rw-r--r-- | gcc/ada/lib-xref.adb | 21 | ||||
| -rw-r--r-- | gcc/ada/lib-xref.ads | 1 | ||||
| -rw-r--r-- | gcc/ada/opt.adb | 9 | ||||
| -rw-r--r-- | gcc/ada/sem.adb | 5 | ||||
| -rw-r--r-- | gcc/ada/sem_attr.adb | 14 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 42 | ||||
| -rw-r--r-- | gcc/ada/sem_util.ads | 3 | ||||
| -rw-r--r-- | gcc/ada/xr_tabls.adb | 4 |
11 files changed, 150 insertions, 16 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 8c57db8..14be351 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,34 @@ +2014-01-23 Tristan Gingold <gingold@adacore.com> + + * gnat_rm.texi: Minor editing. + +2014-01-23 Robert Dewar <dewar@adacore.com> + + * opt.adb (Set_Opt_Config_Switches): Reset SPARK mode for + with'ed internal units. + * sem.adb (Semantics): Save and restore SPARK_Mode[_Pragma]. + +2014-01-23 Javier Miranda <miranda@adacore.com> + + * lib-xref.adb (Generate_Reference): As part of processing the + "end-of-spec" reference generate an extra reference to the first + private entity of the package. + * xr_tabls.adb (Add_Reference): No action needed for the extra + 'E' reference associated; similar to the processing of the + 'e' reference. + +2014-01-23 Bob Duff <duff@adacore.com> + + * gnat_ugn.texi: Change "--&pp off" to "--!pp off". + +2014-01-23 Ed Schonberg <schonberg@adacore.com> + + * sem_util.ads, sem_util.adb (Is_Potentially_Unevaluated): new + predicate to implement rule given in 6.1.1 (20/3). + * sem_attr.adb (Analyze_Attribute, case 'Old): Reject prefix of + 'Old in a postcondition, if it is potentially unevaluated and + it is not an entity name. + 2014-01-23 Bob Duff <duff@adacore.com> * gnat_ugn.texi: Document the new "--&pp off" feature of gnatpp. diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index a4b47d9..8ad73c5 100644 --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -4249,7 +4249,7 @@ pragma Linker_Section ( @end smallexample @noindent -@var{LOCAL_NAME} must refer to an object or a subprogram that is +@var{LOCAL_NAME} must refer to an object that is declared at the library level. This pragma specifies the name of the linker section for the given entity. It is equivalent to @code{__attribute__((section))} in GNU C and causes @var{LOCAL_NAME} to diff --git a/gcc/ada/gnat_ugn.texi b/gcc/ada/gnat_ugn.texi index 88f2138..ca9209c 100644 --- a/gcc/ada/gnat_ugn.texi +++ b/gcc/ada/gnat_ugn.texi @@ -14504,12 +14504,12 @@ Display usage, then exit disregarding all other options. @item --pp-off=@var{xxx} @cindex @option{--pp-off} @command{gnatpp} Use @code{--xxx} as the command to turn off pretty printing, instead -of the default @code{--&pp off}. +of the default @code{--!pp off}. @item --pp-on=@var{xxx} @cindex @option{--pp-on} @command{gnatpp} Use @code{--xxx} as the command to turn pretty printing back on, instead -of the default @code{--&pp on}. +of the default @code{--!pp on}. @item --pp-old @cindex @option{--pp-old} @command{gnatpp} @@ -14559,22 +14559,36 @@ They provide the detailed descriptions of the switches shown above. Pretty printing is highly heuristic in nature, and sometimes doesn't do exactly what you want. If you wish to format a certain region of code by hand, you can turn off pretty printing in that region by -surrounding it with the special comments @code{--&pp off} and -@code{--&pp on}. The text in that region will then be reproduced +surrounding it with special comments that start with @code{--!pp off} +and @code{--!pp on}. The text in that region will then be reproduced verbatim in the output with no formatting. -To disable pretty printing for the whole file, put @code{--&pp off} at -the top, with no following @code{--&pp on}. +To disable pretty printing for the whole file, put @code{--!pp off} at +the top, with no following @code{--!pp on}. The comments must appear on a line by themselves, with nothing -preceding except spaces, and they must appear exactly as shown (case -sensitive). For example, @code{--&pp off -- Turn off pp because ...} -will not be recognized as a valid @code{--&pp off} command. +preceding except spaces. The initial text of the comment must be +exactly @code{--!pp off} or @code{--!pp on} (case sensitive), but may +be followed by arbitrary additional text. For example: + +@smallexample @c ada +@cartouche +package Interrupts is + --!pp off -- turn off pretty printing so "Interrupt_Kind" lines up + type Interrupt_Kind is + (Asynchronous_Interrupt_Kind, + Synchronous_Interrupt_Kind, + Green_Interrupt_Kind); + --!pp on -- reenable pretty printing + + ... +@end cartouche +@end smallexample You can specify different comment strings using the gnatpp @code{--pp-off} and @code{--pp-on} switches. For example, if you say @code{gnatpp --pp-off=' pp-' *.ad?} then gnatpp will recognize -comments of the form @code{-- pp-}, instead of @code{--&pp off} for +comments of the form @code{-- pp-} instead of @code{--!pp off} for disabling pretty printing. Note that the leading @code{--} of the comment is not included in the argument to these switches. diff --git a/gcc/ada/lib-xref.adb b/gcc/ada/lib-xref.adb index aef33ad..a01bbab 100644 --- a/gcc/ada/lib-xref.adb +++ b/gcc/ada/lib-xref.adb @@ -1069,6 +1069,27 @@ package body Lib.Xref is Ref_Scope => Empty, Ent_Scope => Empty), Ent_Scope_File => No_Unit); + + -- Generate reference to the first private entity + + if Typ = 'e' + and then Comes_From_Source (E) + and then Nkind (Ent) = N_Defining_Identifier + and then (Is_Package_Or_Generic_Package (Ent) + or else Is_Concurrent_Type (Ent)) + and then Present (First_Private_Entity (E)) + and then In_Extended_Main_Source_Unit (N) + then + Add_Entry + ((Ent => Ent, + Loc => Sloc (First_Private_Entity (E)), + Typ => 'E', + Eun => Get_Source_Unit (Def), + Lun => Get_Source_Unit (Ref), + Ref_Scope => Empty, + Ent_Scope => Empty), + Ent_Scope_File => No_Unit); + end if; end if; end if; end Generate_Reference; diff --git a/gcc/ada/lib-xref.ads b/gcc/ada/lib-xref.ads index baa07da..a0d5370 100644 --- a/gcc/ada/lib-xref.ads +++ b/gcc/ada/lib-xref.ads @@ -175,6 +175,7 @@ package Lib.Xref is -- d = discriminant of type -- D = object definition -- e = end of spec + -- E = first private entity -- H = abstract type -- i = implicit reference -- k = implicit reference to parent unit in child unit diff --git a/gcc/ada/opt.adb b/gcc/ada/opt.adb index ce23faa..636829c 100644 --- a/gcc/ada/opt.adb +++ b/gcc/ada/opt.adb @@ -167,20 +167,24 @@ package body Opt is Persistent_BSS_Mode := False; Use_VADS_Size := False; Optimize_Alignment_Local := True; - SPARK_Mode := Auto; -- For an internal unit, assertions/debug pragmas are off unless this -- is the main unit and they were explicitly enabled. We also make - -- sure we do not assume that values are necessarily valid. + -- sure we do not assume that values are necessarily valid and that + -- SPARK_Mode is set to its configuration value. if Main_Unit then Assertions_Enabled := Assertions_Enabled_Config; Assume_No_Invalid_Values := Assume_No_Invalid_Values_Config; Check_Policy_List := Check_Policy_List_Config; + SPARK_Mode := SPARK_Mode_Config; + SPARK_Mode_Pragma := SPARK_Mode_Pragma_Config; else Assertions_Enabled := False; Assume_No_Invalid_Values := False; Check_Policy_List := Empty; + SPARK_Mode := Off; + SPARK_Mode_Pragma := Empty; end if; -- Case of non-internal unit @@ -203,6 +207,7 @@ package body Opt is Optimize_Alignment_Local := False; Persistent_BSS_Mode := Persistent_BSS_Mode_Config; SPARK_Mode := SPARK_Mode_Config; + SPARK_Mode_Pragma := SPARK_Mode_Pragma_Config; Use_VADS_Size := Use_VADS_Size_Config; -- Update consistently the value of Init_Or_Norm_Scalars. The value diff --git a/gcc/ada/sem.adb b/gcc/ada/sem.adb index eea49df..db462a4 100644 --- a/gcc/ada/sem.adb +++ b/gcc/ada/sem.adb @@ -1311,6 +1311,8 @@ package body Sem is S_Inside_A_Generic : constant Boolean := Inside_A_Generic; S_Outer_Gen_Scope : constant Entity_Id := Outer_Generic_Scope; S_Style_Check : constant Boolean := Style_Check; + S_SPARK_Mode : constant SPARK_Mode_Type := SPARK_Mode; + S_SPARK_Mode_Pragma : constant Node_Id := SPARK_Mode_Pragma; Generic_Main : constant Boolean := Nkind (Unit (Cunit (Main_Unit))) @@ -1418,7 +1420,6 @@ package body Sem is Inside_A_Generic := False; In_Assertion_Expr := 0; In_Spec_Expression := False; - Set_Comes_From_Source_Default (False); -- Save current config switches and reset then appropriately @@ -1511,6 +1512,8 @@ package body Sem is Inside_A_Generic := S_Inside_A_Generic; Outer_Generic_Scope := S_Outer_Gen_Scope; Style_Check := S_Style_Check; + SPARK_Mode := S_SPARK_Mode; + SPARK_Mode_Pragma := S_SPARK_Mode_Pragma; Restore_Opt_Config_Switches (Save_Config_Switches); diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index 5727e6d..413be90 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -4337,6 +4337,8 @@ package body Sem_Attr is -- During pre-analysis, Prag is the enclosing pragma node if any begin + Prag := Empty; + -- Find enclosing scopes, excluding loops CS := Current_Scope; @@ -4515,6 +4517,18 @@ package body Sem_Attr is ("??attribute Old applied to constant has no effect", P); end if; + -- Check that the prefix of 'Old is an entity, when it appears in + -- a postcondition and may be potentially unevaluated (6.1.1 (27/3)). + + if Present (Prag) + and then Get_Pragma_Id (Prag) = Pragma_Postcondition + and then Is_Potentially_Unevaluated (N) + and then not Is_Entity_Name (P) + then + Error_Msg_N ("prefix that is potentially unevaluated must " + & "denote an entity", N); + end if; + -- The attribute appears within a pre/postcondition, but refers to -- an entity in the enclosing subprogram. If it is a component of -- a formal its expansion might generate actual subtypes that may diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 392d555a..a315e5d 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -10249,6 +10249,48 @@ package body Sem_Util is end if; end Is_Partially_Initialized_Type; + -------------------------------- + -- Is_Potentially_Unevaluated -- + -------------------------------- + + function Is_Potentially_Unevaluated (N : Node_Id) return Boolean is + Par : Node_Id; + Expr : Node_Id; + + begin + Expr := N; + Par := Parent (N); + while not Nkind_In (Par, N_If_Expression, + N_Case_Expression, + N_And_Then, + N_Or_Else, + N_In, + N_Not_In) + loop + Expr := Par; + Par := Parent (Par); + if Nkind (Par) not in N_Subexpr then + return False; + end if; + end loop; + + if Nkind (Par) = N_If_Expression then + return Is_Elsif (Par) or else Expr /= First (Expressions (Par)); + + elsif Nkind (Par) = N_Case_Expression then + return Expr /= Expression (Par); + + elsif Nkind_In (Par, N_And_Then, N_Or_Else) then + return Expr = Right_Opnd (Par); + + elsif Nkind_In (Par, N_In, N_Not_In) then + return Expr /= Left_Opnd (Par); + + else + return False; + end if; + end Is_Potentially_Unevaluated; + ------------------------------------ -- Is_Potentially_Persistent_Type -- ------------------------------------ diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index a093a39..3fb9cda 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -1116,6 +1116,9 @@ package Sem_Util is -- if Include_Implicit is False, these cases do not count as making the -- type be partially initialized. + function Is_Potentially_Unevaluated (N : Node_Id) return Boolean; + -- Predicate to implement definition given in RM 6.1.1 (20/3) + function Is_Potentially_Persistent_Type (T : Entity_Id) return Boolean; -- Determines if type T is a potentially persistent type. A potentially -- persistent type is defined (recursively) as a scalar type, a non-tagged diff --git a/gcc/ada/xr_tabls.adb b/gcc/ada/xr_tabls.adb index 61ac675..4b82b03 100644 --- a/gcc/ada/xr_tabls.adb +++ b/gcc/ada/xr_tabls.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1998-2012, Free Software Foundation, Inc. -- +-- Copyright (C) 1998-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- -- @@ -431,7 +431,7 @@ package body Xr_Tabls is Decl_Type => ' ', Is_Parameter => True); - when 'e' | 'z' | 't' | 'p' | 'P' | 'k' | 'd' => + when 'e' | 'E' | 'z' | 't' | 'p' | 'P' | 'k' | 'd' => return; when others => |