aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--gcc/ada/ChangeLog31
-rw-r--r--gcc/ada/gnat_rm.texi2
-rw-r--r--gcc/ada/gnat_ugn.texi34
-rw-r--r--gcc/ada/lib-xref.adb21
-rw-r--r--gcc/ada/lib-xref.ads1
-rw-r--r--gcc/ada/opt.adb9
-rw-r--r--gcc/ada/sem.adb5
-rw-r--r--gcc/ada/sem_attr.adb14
-rw-r--r--gcc/ada/sem_util.adb42
-rw-r--r--gcc/ada/sem_util.ads3
-rw-r--r--gcc/ada/xr_tabls.adb4
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 =>
generated by cgit v1.1 at 2025-05-28 18:29:29 +0000