[multiple changes]

2013-01-02  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Analyze_Pragma): Check the legality of pragma Assume.

2013-01-02  Thomas Quinot  <quinot@adacore.com>

	* sem_eval.adb (Compile_Time_Compare): For static operands, we
	can perform a compile time comparison even if in preanalysis mode.

2013-01-02  Thomas Quinot  <quinot@adacore.com>

	* par_sco.adb (SCO_Record): Always use
	Traverse_Declarations_Or_Statements to process the library level
	declaration, so that SCOs are properly generated for its aspects.

From-SVN: r194778

gcc/ada/ChangeLog

+2013-01-02  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_prag.adb (Analyze_Pragma): Check the legality of pragma Assume.
+
+2013-01-02  Thomas Quinot  <quinot@adacore.com>
+
+	* sem_eval.adb (Compile_Time_Compare): For static operands, we
+	can perform a compile time comparison even if in preanalysis mode.
+
+2013-01-02  Thomas Quinot  <quinot@adacore.com>
+
+	* par_sco.adb (SCO_Record): Always use
+	Traverse_Declarations_Or_Statements to process the library level
+	declaration, so that SCOs are properly generated for its aspects.
+
 2013-01-02  Thomas Quinot  <quinot@adacore.com>
 
 	* scos.ads (In_Decision): Add missing entry for 'a'.

gcc/ada/par_sco.adb

@@ -154,7 +154,6 @@ package body Par_SCO is
    --  Process L, a list of statements or declarations dominated by D.
    --  If P is present, it is processed as though it had been prepended to L.
 
-   procedure Traverse_Generic_Instantiation       (N : Node_Id);
    procedure Traverse_Generic_Package_Declaration (N : Node_Id);
    procedure Traverse_Handled_Statement_Sequence
      (N : Node_Id;
@@ -165,7 +164,6 @@ package body Par_SCO is
    procedure Traverse_Subprogram_Or_Task_Body
      (N : Node_Id;
       D : Dominant_Info := No_Dominant);
-   procedure Traverse_Subprogram_Declaration      (N : Node_Id);
    --  Traverse the corresponding construct, generating SCO table entries
 
    procedure Write_SCOs_To_ALI_File is new Put_SCOs;
@@ -900,6 +898,23 @@ package body Par_SCO is
       Lu   : Node_Id;
       From : Nat;
 
+      procedure Traverse_Aux_Decls (N : Node_Id);
+      --  Traverse the Aux_Decl_Nodes of compilation unit N
+
+      ------------------------
+      -- Traverse_Aux_Decls --
+      ------------------------
+
+      procedure Traverse_Aux_Decls (N : Node_Id) is
+         ADN : constant Node_Id := Aux_Decls_Node (N);
+      begin
+         Traverse_Declarations_Or_Statements (Config_Pragmas (ADN));
+         Traverse_Declarations_Or_Statements (Declarations   (ADN));
+         Traverse_Declarations_Or_Statements (Pragmas_After  (ADN));
+      end Traverse_Aux_Decls;
+
+   --  Start of processing for SCO_Record
+
    begin
       --  Ignore call if not generating code and generating SCO's
 
@@ -929,27 +944,22 @@ package body Par_SCO is
 
       --  Traverse the unit
 
-      case Nkind (Lu) is
-         when N_Protected_Body =>
-            Traverse_Protected_Body (Lu);
-
-         when N_Subprogram_Body | N_Task_Body =>
-            Traverse_Subprogram_Or_Task_Body (Lu);
-
-         when N_Subprogram_Declaration =>
-            Traverse_Subprogram_Declaration (Lu);
+      Traverse_Aux_Decls (Cunit (U));
 
-         when N_Package_Declaration =>
-            Traverse_Package_Declaration (Lu);
-
-         when N_Package_Body =>
-            Traverse_Package_Body (Lu);
-
-         when N_Generic_Package_Declaration =>
-            Traverse_Generic_Package_Declaration (Lu);
-
-         when N_Generic_Instantiation =>
-            Traverse_Generic_Instantiation (Lu);
+      case Nkind (Lu) is
+         when
+           N_Package_Declaration         |
+           N_Package_Body                |
+           N_Subprogram_Declaration      |
+           N_Subprogram_Body             |
+           N_Generic_Package_Declaration |
+           N_Protected_Body              |
+           N_Task_Body                   |
+           N_Generic_Instantiation       =>
+
+            Traverse_Declarations_Or_Statements
+              (L => No_List,
+               P => Lu);
 
          when others =>
 
@@ -1989,47 +1999,29 @@ package body Par_SCO is
    --  Start of processing for Traverse_Declarations_Or_Statements
 
    begin
+      --  Process single prefixed node
+
       if Present (P) then
          Traverse_One (P);
       end if;
 
-      if Is_Non_Empty_List (L) then
-
-         --  Loop through statements or declarations
+      --  Loop through statements or declarations
 
+      if Is_Non_Empty_List (L) then
          N := First (L);
          while Present (N) loop
             Traverse_One (N);
             Next (N);
          end loop;
 
-         Set_Statement_Entry;
       end if;
-   end Traverse_Declarations_Or_Statements;
-
-   ------------------------------------
-   -- Traverse_Generic_Instantiation --
-   ------------------------------------
-
-   procedure Traverse_Generic_Instantiation (N : Node_Id) is
-      First : Source_Ptr;
-      Last  : Source_Ptr;
-
-   begin
-      --  First we need a statement entry to cover the instantiation
 
-      Sloc_Range (N, First, Last);
-      Set_Table_Entry
-        (C1   => 'S',
-         C2   => ' ',
-         From => First,
-         To   => Last,
-         Last => True);
+      --  End sequence of statements and flush deferred decisions
 
-      --  Now output any embedded decisions
-
-      Process_Decisions (N, 'X', No_Location);
-   end Traverse_Generic_Instantiation;
+      if Present (P) or else Is_Non_Empty_List (L) then
+         Set_Statement_Entry;
+      end if;
+   end Traverse_Declarations_Or_Statements;
 
    ------------------------------------------
    -- Traverse_Generic_Package_Declaration --
@@ -2114,16 +2106,4 @@ package body Par_SCO is
       Traverse_Handled_Statement_Sequence (Handled_Statement_Sequence (N), D);
    end Traverse_Subprogram_Or_Task_Body;
 
-   -------------------------------------
-   -- Traverse_Subprogram_Declaration --
-   -------------------------------------
-
-   procedure Traverse_Subprogram_Declaration (N : Node_Id) is
-      ADN : constant Node_Id := Aux_Decls_Node (Parent (N));
-   begin
-      Traverse_Declarations_Or_Statements (Config_Pragmas (ADN));
-      Traverse_Declarations_Or_Statements (Declarations   (ADN));
-      Traverse_Declarations_Or_Statements (Pragmas_After  (ADN));
-   end Traverse_Subprogram_Declaration;
-
 end Par_SCO;

gcc/ada/sem_eval.adb

@@ -744,13 +744,19 @@ package body Sem_Eval is
    begin
       Diff.all := No_Uint;
 
-      --  In preanalysis mode, always return Unknown, it is too early to be
-      --  thinking we know the result of a comparison, save that judgment for
-      --  the full analysis. This is particularly important in the case of
-      --  pre and postconditions, which otherwise can be prematurely collapsed
-      --  into having True or False conditions when this is inappropriate.
-
-      if not Full_Analysis then
+      --  In preanalysis mode, always return Unknown unless the expression
+      --  is static. It is too early to be thinking we know the result of a
+      --  comparison, save that judgment for the full analysis. This is
+      --  particularly important in the case of pre and postconditions, which
+      --  otherwise can be prematurely collapsed into having True or False
+      --  conditions when this is inappropriate.
+
+      if not (Full_Analysis
+                or else
+              (Is_Static_Expression (L)
+                 and then
+               Is_Static_Expression (R)))
+      then
          return Unknown;
       end if;
 

gcc/ada/sem_prag.adb

@@ -7013,16 +7013,27 @@ package body Sem_Prag is
 
          --  pragma Assume (boolean_EXPRESSION);
 
-         --  This should share pragma Assert code ???
-         --  Run-time check is missing completely ???
-
          when Pragma_Assume => Assume : declare
          begin
             GNAT_Pragma;
             S14_Pragma;
             Check_Arg_Count (1);
 
-            Analyze_And_Resolve (Expression (Arg1), Any_Boolean);
+            --  Pragma Assume is transformed into pragma Check in the following
+            --  manner:
+
+            --    pragma Check (Assume, Expr);
+
+            Rewrite (N,
+              Make_Pragma (Loc,
+                Chars                        => Name_Check,
+                Pragma_Argument_Associations => New_List (
+                  Make_Pragma_Argument_Association (Loc,
+                    Expression => Make_Identifier (Loc, Name_Assume)),
+
+                  Make_Pragma_Argument_Association (Loc,
+                    Expression => Relocate_Node (Expression (Arg1))))));
+            Analyze (N);
          end Assume;
 
          ------------------------------