2012-12-05 Thomas Quinot <quinot@adacore.com>

	* par_sco.adb (Traverse_Aspects): Ensure we always have
	an entry in the sloc -> SCO map for invariants, since
	Set_SCO_Pragma_Enabled is called with that sloc when checks
	are enabled.

2012-12-05  Thomas Quinot  <quinot@adacore.com>

	* exp_ch4.adb: Minor reformatting.

2012-12-05  Hristian Kirtchev  <kirtchev@adacore.com>

	* par-prag.adb: Checks and processing of pragma Assume are
	carried out by Sem_Prag.
	* sem_prag.adb (Analyze_Pragma): Check the legality of pragma
	Assume.
	* snames.ads-tmpl: Add new name Assume. Add a pragma identifier
	for Assume.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@194215 138bc75d-0d04-0410-961f-82ee72b054a4

1 files changed, 31 insertions, 24 deletions

diff --git a/gcc/ada/par_sco.adb b/gcc/ada/par_sco.adb
index 4ce6951a755..1149a2ec37b 100644
--- a/gcc/ada/par_sco.adb
+++ b/gcc/ada/par_sco.adb
@@ -493,14 +493,14 @@ package body Par_SCO is
 
       begin
          case T is
-            when 'I' | 'E' | 'W' | 'a' =>
+            when 'I' | 'E' | 'W' | 'a' | 'A' =>
 
                --  For IF, EXIT, WHILE, or aspects, the token SLOC is that of
                --  the parent of the expression.
 
                Loc := Sloc (Parent (N));
 
-               if T = 'a' then
+               if T = 'a' or else T = 'A' then
                   Nam := Chars (Identifier (Parent (N)));
                end if;
 
@@ -1378,12 +1378,20 @@ package body Par_SCO is
       procedure Traverse_Aspects (N : Node_Id) is
          AN : Node_Id;
          AE : Node_Id;
+         C1 : Character;
 
       begin
          AN := First (Aspect_Specifications (N));
          while Present (AN) loop
             AE := Expression (AN);
 
+            --  SCOs are generated before semantic analysis/expansion:
+            --  PPCs are not split yet.
+
+            pragma Assert (not Split_PPC (AN));
+
+            C1 := ASCII.NUL;
+
             case Get_Aspect_Id (Chars (Identifier (AN))) is
 
                --  Aspects rewritten into pragmas controlled by a Check_Policy:
@@ -1394,37 +1402,24 @@ package body Par_SCO is
                when Aspect_Pre               |
                     Aspect_Precondition      |
                     Aspect_Post              |
-                    Aspect_Postcondition     =>
-
-                  --  SCOs are generated before semantic analysis/expansion:
-                  --  PPCs are not split yet.
-
-                  pragma Assert (not Split_PPC (AN));
+                    Aspect_Postcondition     |
+                    Aspect_Invariant         =>
 
-                  --  A Pre/Post aspect will be rewritten into a pragma
-                  --  Precondition/Postcondition with the same sloc.
-
-                  pragma Assert (Current_Pragma_Sloc = No_Location);
-
-                  Current_Pragma_Sloc := Sloc (AN);
-
-                  --  Create the decision as potentially disabled aspect ('a').
-                  --  Set_SCO_Pragma_Enabled will subsequently switch to 'A'.
-
-                  Process_Decisions_Defer (AE, 'a');
-                  Current_Pragma_Sloc := No_Location;
+                  C1 := 'a';
 
                --  Aspects whose checks are generated in client units,
                --  regardless of whether or not the check is activated in the
-               --  unit which contains the declaration.
+               --  unit which contains the declaration: create decision as
+               --  unconditionally enabled aspect (but still make a pragma
+               --  entry since Set_SCO_Pragma_Enabled will be called when
+               --  analyzing actual checks, possibly in other units).
 
                when Aspect_Predicate         |
                     Aspect_Static_Predicate  |
                     Aspect_Dynamic_Predicate |
-                    Aspect_Invariant         |
                     Aspect_Type_Invariant    =>
 
-                  Process_Decisions_Defer (AE, 'A');
+                  C1 := 'A';
 
                --  Other aspects: just process any decision nested in the
                --  aspect expression.
@@ -1432,11 +1427,23 @@ package body Par_SCO is
                when others =>
 
                   if Has_Decision (AE) then
-                     Process_Decisions_Defer (AE, 'X');
+                     C1 := 'X';
                   end if;
 
             end case;
 
+            if C1 /= ASCII.NUL then
+               pragma Assert (Current_Pragma_Sloc = No_Location);
+
+               if C1 = 'a' or else C1 = 'A' then
+                  Current_Pragma_Sloc := Sloc (AN);
+               end if;
+
+               Process_Decisions_Defer (AE, C1);
+
+               Current_Pragma_Sloc := No_Location;
+            end if;
+
             Next (AN);
          end loop;
       end Traverse_Aspects;