+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
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
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.
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));
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;
Tsk : Node_Id := Empty;
function Process_Discr (Nod : Node_Id) return Traverse_Result;
+ -- Comment needed???
-------------------
-- Process_Discr --
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);
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))));
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,
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;
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
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
else
-- In ALFA_Mode, no such magic needs to happen, we just resolve the
- -- underlying nodes
+ -- underlying nodes.
Resolve (Condition (N), Typ);
end if;
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;
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;