From e02965831e0ec57a216cc64e38ebcdb10bc1e77f Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 29 Aug 2011 15:27:37 +0200 Subject: [PATCH] [multiple changes] 2011-08-29 Yannick Moy * 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 * gnat1drv.adb (Adjust_Global_Switches): Improve previous change. Add comment. 2011-08-29 Thomas Quinot * sem_res.adb: Minor reformatting. From-SVN: r178224 --- gcc/ada/ChangeLog | 17 +++++++++++++++++ gcc/ada/gnat1drv.adb | 16 +++++++++++++--- gcc/ada/sem_prag.adb | 4 ++-- gcc/ada/sem_res.adb | 30 ++++++++++++------------------ gcc/ada/sem_util.adb | 14 ++++++++------ 5 files changed, 52 insertions(+), 29 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 7e3b17366fa..d99c28ab75e 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,20 @@ +2011-08-29 Yannick Moy + + * 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 + + * gnat1drv.adb (Adjust_Global_Switches): Improve previous change. + Add comment. + +2011-08-29 Thomas Quinot + + * sem_res.adb: Minor reformatting. + 2011-08-29 Johannes Kanig * exp_ch4.adb (Expand_Quantified_Expression): Do not expand in ALFA diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index 56195330773..6c1292e7b70 100644 --- a/gcc/ada/gnat1drv.adb +++ b/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. diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 8bf98ba7ea9..081d9aeffef 100644 --- a/gcc/ada/sem_prag.adb +++ b/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; diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 375ca904a82..ab57f46f7e8 100644 --- a/gcc/ada/sem_res.adb +++ b/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; diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 3072f6a3522..86c57267b65 100644 --- a/gcc/ada/sem_util.adb +++ b/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; -- 2.30.2