[multiple changes]

2011-08-29  Yannick Moy  <moy@adacore.com>

	* sem_prag.adb (Analyze_Pragma): Allow Test_Case pragma without
	Requires/Ensures.
	* sem_util.adb (Get_Ensures_From_Test_Case_Pragma,
	Get_Requires_From_Test_Case_Pragma): Allow Test_Case pragma without
	Requires/Ensures.

2011-08-29  Arnaud Charlet  <charlet@adacore.com>

	* gnat1drv.adb (Adjust_Global_Switches): Improve previous change.
	Add comment.

2011-08-29  Thomas Quinot  <quinot@adacore.com>

	* sem_res.adb: Minor reformatting.

From-SVN: r178224

gcc/ada/ChangeLog

+2011-08-29  Yannick Moy  <moy@adacore.com>
+
+	* sem_prag.adb (Analyze_Pragma): Allow Test_Case pragma without
+	Requires/Ensures.
+	* sem_util.adb (Get_Ensures_From_Test_Case_Pragma,
+	Get_Requires_From_Test_Case_Pragma): Allow Test_Case pragma without
+	Requires/Ensures.
+
+2011-08-29  Arnaud Charlet  <charlet@adacore.com>
+
+	* gnat1drv.adb (Adjust_Global_Switches): Improve previous change.
+	Add comment.
+
+2011-08-29  Thomas Quinot  <quinot@adacore.com>
+
+	* sem_res.adb: Minor reformatting.
+
 2011-08-29  Johannes Kanig  <kanig@adacore.com>
 
 	* exp_ch4.adb (Expand_Quantified_Expression): Do not expand in ALFA

gcc/ada/gnat1drv.adb

@@ -351,10 +351,9 @@ procedure Gnat1drv is
       if Debug_Flag_Dot_XX then
          Use_Expression_With_Actions := True;
 
-      --  Debug flag -gnatd.Y and -gnatd.F (Alfa Mode) decisively set usage
-      --  off
+      --  Debug flag -gnatd.Y decisively set usage off
 
-      elsif Debug_Flag_Dot_YY or Debug_Flag_Dot_FF then
+      elsif Debug_Flag_Dot_YY then
          Use_Expression_With_Actions := False;
 
       --  Otherwise this feature is implemented, so we allow its use
@@ -445,6 +444,17 @@ procedure Gnat1drv is
 
          Debug_Flag_HH := True;
 
+         --  Disable Expressions_With_Actions nodes
+         --  The gnat2why backend does not deal with Expressions_With_Actions
+         --  in all places (in particular assertions). It is difficult to
+         --  determine in the frontend which cases are allowed, so we disable
+         --  Expressions_With_Actions entirely. Even in the cases where
+         --  gnat2why deals with Expressions_With_Actions, it is easier to
+         --  deal with the original constructs (quantified, conditional and
+         --  case expressions) instead of the rewritten ones.
+
+         Use_Expression_With_Actions := False;
+
          --  Enable assertions and debug pragmas, since they give valuable
          --  extra information for formal verification.
 

gcc/ada/sem_prag.adb

@@ -13313,7 +13313,7 @@ package body Sem_Prag is
          when Pragma_Test_Case => Test_Case : declare
          begin
             GNAT_Pragma;
-            Check_At_Least_N_Arguments (3);
+            Check_At_Least_N_Arguments (2);
             Check_At_Most_N_Arguments (4);
             Check_Arg_Order
                  ((Name_Name, Name_Mode, Name_Requires, Name_Ensures));
@@ -13326,7 +13326,7 @@ package body Sem_Prag is
             if Arg_Count = 4 then
                Check_Identifier (Arg3, Name_Requires);
                Check_Identifier (Arg4, Name_Ensures);
-            else
+            elsif Arg_Count = 3 then
                Check_Identifier_Is_One_Of (Arg3, Name_Requires, Name_Ensures);
             end if;
 

gcc/ada/sem_res.adb

@@ -1685,6 +1685,7 @@ package body Sem_Res is
       Tsk : Node_Id := Empty;
 
       function Process_Discr (Nod : Node_Id) return Traverse_Result;
+      --  Comment needed???
 
       -------------------
       -- Process_Discr --
@@ -1793,9 +1794,8 @@ package body Sem_Res is
            Make_Explicit_Dereference (Loc,
              Prefix =>
                Make_Selected_Component (Loc,
-                 Prefix => Relocate_Node (Expr),
-                 Selector_Name =>
-               New_Occurrence_Of (Disc, Loc))));
+                 Prefix        => Relocate_Node (Expr),
+                 Selector_Name => New_Occurrence_Of (Disc, Loc))));
 
          Set_Etype (Prefix (Expr), Etype (Disc));
          Set_Etype (Expr, Typ);
@@ -1819,18 +1819,14 @@ package body Sem_Res is
 
       procedure Patch_Up_Value (N : Node_Id; Typ : Entity_Id) is
       begin
-         if Nkind (N) = N_Integer_Literal
-           and then Is_Real_Type (Typ)
-         then
+         if Nkind (N) = N_Integer_Literal and then Is_Real_Type (Typ) then
             Rewrite (N,
               Make_Real_Literal (Sloc (N),
                 Realval => UR_From_Uint (Intval (N))));
             Set_Etype (N, Universal_Real);
             Set_Is_Static_Expression (N);
 
-         elsif Nkind (N) = N_Real_Literal
-           and then Is_Integer_Type (Typ)
-         then
+         elsif Nkind (N) = N_Real_Literal and then Is_Integer_Type (Typ) then
             Rewrite (N,
               Make_Integer_Literal (Sloc (N),
                 Intval => UR_To_Uint (Realval (N))));
@@ -1838,7 +1834,7 @@ package body Sem_Res is
             Set_Is_Static_Expression (N);
 
          elsif Nkind (N) = N_String_Literal
-           and then Is_Character_Type (Typ)
+                 and then Is_Character_Type (Typ)
          then
             Set_Character_Literal_Name (Char_Code (Character'Pos ('A')));
             Rewrite (N,
@@ -1849,15 +1845,13 @@ package body Sem_Res is
             Set_Etype (N, Any_Character);
             Set_Is_Static_Expression (N);
 
-         elsif Nkind (N) /= N_String_Literal
-           and then Is_String_Type (Typ)
-         then
+         elsif Nkind (N) /= N_String_Literal and then Is_String_Type (Typ) then
             Rewrite (N,
               Make_String_Literal (Sloc (N),
                 Strval => End_String));
 
          elsif Nkind (N) = N_Range then
-            Patch_Up_Value (Low_Bound (N), Typ);
+            Patch_Up_Value (Low_Bound (N),  Typ);
             Patch_Up_Value (High_Bound (N), Typ);
          end if;
       end Patch_Up_Value;
@@ -1878,7 +1872,7 @@ package body Sem_Res is
          then
             Error_Msg_NE ("ambiguous call to&", Arg, Name (Arg));
 
-            --  Could use comments on what is going on here ???
+            --  Could use comments on what is going on here???
 
             Get_First_Interp (Name (Arg), I, It);
             while Present (It.Nam) loop
@@ -1926,8 +1920,8 @@ package body Sem_Res is
          return;
       end if;
 
-      --  Access attribute on remote subprogram cannot be used for
-      --  a non-remote access-to-subprogram type.
+      --  Access attribute on remote subprogram cannot be used for a non-remote
+      --  access-to-subprogram type.
 
       if Nkind (N) = N_Attribute_Reference
         and then (Attribute_Name (N) = Name_Access              or else
@@ -8095,7 +8089,7 @@ package body Sem_Res is
       else
 
          --  In ALFA_Mode, no such magic needs to happen, we just resolve the
-         --  underlying nodes
+         --  underlying nodes.
 
          Resolve (Condition (N), Typ);
       end if;

gcc/ada/sem_util.adb

@@ -4274,13 +4274,13 @@ package body Sem_Util is
 
    function Get_Ensures_From_Test_Case_Pragma (N : Node_Id) return Node_Id is
       Args : constant List_Id := Pragma_Argument_Associations (N);
-      Res  : Node_Id;
+      Res  : Node_Id := Empty;
 
    begin
       if List_Length (Args) = 4 then
          Res := Pick (Args, 4);
 
-      else
+      elsif List_Length (Args) = 3 then
          Res := Pick (Args, 3);
          if Chars (Res) /= Name_Ensures then
             Res := Empty;
@@ -4436,12 +4436,14 @@ package body Sem_Util is
 
    function Get_Requires_From_Test_Case_Pragma (N : Node_Id) return Node_Id is
       Args : constant List_Id := Pragma_Argument_Associations (N);
-      Res  : Node_Id;
+      Res  : Node_Id := Empty;
 
    begin
-      Res := Pick (Args, 3);
-      if Chars (Res) /= Name_Requires then
-         Res := Empty;
+      if List_Length (Args) >= 3 then
+         Res := Pick (Args, 3);
+         if Chars (Res) /= Name_Requires then
+            Res := Empty;
+         end if;
       end if;
 
       return Res;