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

6 files changed, 90 insertions, 32 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 7b4634c8b5d..eea922d6000 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,23 @@
+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.
+
 2012-12-05  Ed Schonberg  <schonberg@adacore.com>
 
 	* aspects.ads, aspects.adb: Add aspect Relative_Deadline.
diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb
index 07e7ab8b4b8..b7ecd830048 100644
--- a/gcc/ada/exp_ch4.adb
+++ b/gcc/ada/exp_ch4.adb
@@ -10405,14 +10405,14 @@ package body Exp_Ch4 is
             --  Convert: x(y) to x'val (ytyp'val (y))
 
             Rewrite (N,
-               Make_Attribute_Reference (Loc,
-                 Prefix => New_Occurrence_Of (Target_Type, Loc),
-                 Attribute_Name => Name_Val,
-                 Expressions => New_List (
-                   Make_Attribute_Reference (Loc,
-                     Prefix => New_Occurrence_Of (Operand_Type, Loc),
-                     Attribute_Name => Name_Pos,
-                     Expressions => New_List (Operand)))));
+              Make_Attribute_Reference (Loc,
+                Prefix         => New_Occurrence_Of (Target_Type, Loc),
+                Attribute_Name => Name_Val,
+                Expressions    => New_List (
+                  Make_Attribute_Reference (Loc,
+                    Prefix         => New_Occurrence_Of (Operand_Type, Loc),
+                    Attribute_Name => Name_Pos,
+                    Expressions    => New_List (Operand)))));
 
             Analyze_And_Resolve (N, Target_Type);
          end if;
diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb
index 9d974f3b09a..e1f394b2853 100644
--- a/gcc/ada/par-prag.adb
+++ b/gcc/ada/par-prag.adb
@@ -1093,6 +1093,7 @@ begin
 
       when Pragma_Abort_Defer                    |
            Pragma_Assertion_Policy               |
+           Pragma_Assume                         |
            Pragma_Assume_No_Invalid_Values       |
            Pragma_AST_Entry                      |
            Pragma_All_Calls_Remote               |
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;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index be5afe028a6..36251b8bad1 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -2233,6 +2233,18 @@ package body Sem_Prag is
               (Get_Pragma_Arg (Arg2), Standard_String);
          end if;
 
+         --  For a pragma in the extended main source unit, record enabled
+         --  status in SCO.
+
+         --  This may seem redundant with the call to Check_Enabled occurring
+         --  later on when the pragma is rewritten into a pragma Check but
+         --  is actually required in the case of a postcondition within a
+         --  generic.
+
+         if Check_Enabled (Pname) and then not Split_PPC (N) then
+            Set_SCO_Pragma_Enabled (Loc);
+         end if;
+
          --  If we are within an inlined body, the legality of the pragma
          --  has been checked already.
 
@@ -6995,6 +7007,21 @@ package body Sem_Prag is
             Opt.Check_Policy_List := N;
          end Assertion_Policy;
 
+         ------------
+         -- Assume --
+         ------------
+
+         --  pragma Assume (boolean_EXPRESSION);
+
+         when Pragma_Assume => Assume : declare
+         begin
+            GNAT_Pragma;
+            S14_Pragma;
+            Check_Arg_Count (1);
+
+            Analyze_And_Resolve (Expression (Arg1), Any_Boolean);
+         end Assume;
+
          ------------------------------
          -- Assume_No_Invalid_Values --
          ------------------------------
@@ -15668,6 +15695,7 @@ package body Sem_Prag is
       Pragma_Assert                         => -1,
       Pragma_Assert_And_Cut                 => -1,
       Pragma_Assertion_Policy               =>  0,
+      Pragma_Assume                         =>  0,
       Pragma_Assume_No_Invalid_Values       =>  0,
       Pragma_Attribute_Definition           => +3,
       Pragma_Asynchronous                   => -1,
diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
index cc269a1446c..bffa6004ba7 100644
--- a/gcc/ada/snames.ads-tmpl
+++ b/gcc/ada/snames.ads-tmpl
@@ -362,6 +362,7 @@ package Snames is
    Name_Ada_2012                       : constant Name_Id := N + $; -- GNAT
    Name_Annotate                       : constant Name_Id := N + $; -- GNAT
    Name_Assertion_Policy               : constant Name_Id := N + $; -- Ada 05
+   Name_Assume                         : constant Name_Id := N + $; -- GNAT
    Name_Assume_No_Invalid_Values       : constant Name_Id := N + $; -- GNAT
    Name_Attribute_Definition           : constant Name_Id := N + $; -- GNAT
    Name_C_Pass_By_Copy                 : constant Name_Id := N + $; -- GNAT
@@ -1660,6 +1661,7 @@ package Snames is
       Pragma_Ada_2012,
       Pragma_Annotate,
       Pragma_Assertion_Policy,
+      Pragma_Assume,
       Pragma_Assume_No_Invalid_Values,
       Pragma_Attribute_Definition,
       Pragma_C_Pass_By_Copy,