* exp_ch6.adb (Expand_Subprogram_Contract, Append_Enabled_Item):
Take into account the Split_PPC flag to ensure that conjuncts
in a composite postcondition aspect are tested in source order.
2014-02-06 Hristian Kirtchev <kirtchev@adacore.com>
* sem_ch6.adb (Analyze_Generic_Subprogram_Body): Flag illegal
use of SPARK_Mode.
* sem_ch12.adb (Analyze_Generic_Subprogram_Declaration): Flag
illegal use of SPARK_Mode.
(Instantiate_Subprogram_Body): Flag illegal use of SPARK_Mode.
* sem_prag.adb (Analyze_Pragma): Code reformatting.
* sem_util.adb Add with and use clause for Aspects.
(Check_SPARK_Mode_In_Generic): New routine.
* sem_util.ads (Check_SPARK_Mode_In_Generic): New routine.
2014-02-06 Thomas Quinot <quinot@adacore.com>
* a-calend.adb (Formatting_Operations.Split): Ensure that
Time_Error is raised for invalid time values.
git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@207536
138bc75d-0d04-0410-961f-
82ee72b054a4
+2014-02-06 Ed Schonberg <schonberg@adacore.com>
+
+ * exp_ch6.adb (Expand_Subprogram_Contract, Append_Enabled_Item):
+ Take into account the Split_PPC flag to ensure that conjuncts
+ in a composite postcondition aspect are tested in source order.
+
+2014-02-06 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_ch6.adb (Analyze_Generic_Subprogram_Body): Flag illegal
+ use of SPARK_Mode.
+ * sem_ch12.adb (Analyze_Generic_Subprogram_Declaration): Flag
+ illegal use of SPARK_Mode.
+ (Instantiate_Subprogram_Body): Flag illegal use of SPARK_Mode.
+ * sem_prag.adb (Analyze_Pragma): Code reformatting.
+ * sem_util.adb Add with and use clause for Aspects.
+ (Check_SPARK_Mode_In_Generic): New routine.
+ * sem_util.ads (Check_SPARK_Mode_In_Generic): New routine.
+
+2014-02-06 Thomas Quinot <quinot@adacore.com>
+
+ * a-calend.adb (Formatting_Operations.Split): Ensure that
+ Time_Error is raised for invalid time values.
+
2014-02-06 Arnaud Charlet <charlet@adacore.com>
* sem_prag.adb (Analyze_Pragma): Rewrite as a null statement
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2012, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2013, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
Hour_Seconds := Day_Seconds mod 3_600;
Minute := Hour_Seconds / 60;
Second := Hour_Seconds mod 60;
+
+ exception
+ when Constraint_Error =>
+ raise Time_Error;
end Split;
-------------
List := New_List;
end if;
- Append (Item, List);
+ -- If the pragma is a conjunct in a composite postcondition, it
+ -- has been processed in reverse order. In the postcondition body
+ -- if must appear before the others.
+
+ if Nkind (Item) = N_Pragma
+ and then From_Aspect_Specification (Item)
+ and then Split_PPC (Item)
+ then
+ Prepend (Item, List);
+ else
+ Append (Item, List);
+ end if;
end if;
end Append_Enabled_Item;
Set_Parent_Spec (New_N, Save_Parent);
Rewrite (N, New_N);
+ Check_SPARK_Mode_In_Generic (N);
+
-- The aspect specifications are not attached to the tree, and must
-- be copied and attached to the generic copy explicitly.
end loop;
end;
+ Check_SPARK_Mode_In_Generic (N);
+
Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
Set_SPARK_Pragma_Inherited (Body_Id, True);
Check_No_Identifiers;
Check_At_Most_N_Arguments (1);
- if Inside_A_Generic then
- Error_Pragma ("incorrect placement of pragma% in a generic");
- end if;
-
-- Check the legality of the mode (no argument = ON)
if Arg_Count = 1 then
Mode_Id := Get_SPARK_Mode_Type (Mode);
Context := Parent (N);
+ -- Packages and subprograms declared in a generic unit cannot be
+ -- subject to the pragma.
+
+ if Inside_A_Generic then
+ Error_Pragma ("incorrect placement of pragma% in a generic");
+
-- The pragma appears in a configuration pragmas file
- if No (Context) then
+ elsif No (Context) then
Check_Valid_Configuration_Pragma;
if Present (SPARK_Mode_Pragma) then
and then Nkind (Unit (Library_Unit (Context))) in
N_Generic_Declaration)
then
- Error_Pragma
- ("incorrect placement of pragma% in a generic unit");
+ Error_Pragma ("incorrect placement of pragma% in a generic");
end if;
SPARK_Mode_Pragma := N;
-- --
------------------------------------------------------------------------------
+with Aspects; use Aspects;
with Atree; use Atree;
with Casing; use Casing;
with Checks; use Checks;
end if;
end Check_Result_And_Post_State;
+ ---------------------------------
+ -- Check_SPARK_Mode_In_Generic --
+ ---------------------------------
+
+ procedure Check_SPARK_Mode_In_Generic (N : Node_Id) is
+ Aspect : Node_Id;
+
+ begin
+ -- Try to find aspect SPARK_Mode and flag it as illegal
+
+ if Has_Aspects (N) then
+ Aspect := First (Aspect_Specifications (N));
+ while Present (Aspect) loop
+ if Get_Aspect_Id (Aspect) = Aspect_SPARK_Mode then
+ Error_Msg_Name_1 := Name_SPARK_Mode;
+ Error_Msg_N
+ ("incorrect placement of aspect % on a generic", Aspect);
+ exit;
+ end if;
+
+ Next (Aspect);
+ end loop;
+ end if;
+ end Check_SPARK_Mode_In_Generic;
+
------------------------------
-- Check_Unprotected_Access --
------------------------------
-- Precondition
-- Refined_Depends
-- Refined_Global
+ -- Refined_Post
-- Refined_States
-- Test_Case
-- and post-state. Prag is a [refined] postcondition or a contract-cases
-- pragma. Result_Seen is set when the pragma mentions attribute 'Result.
+ procedure Check_SPARK_Mode_In_Generic (N : Node_Id);
+ -- Given a generic package [body] or a generic subprogram [body], inspect
+ -- the aspect specifications (if any) and flag SPARK_Mode as illegal.
+
procedure Check_Unprotected_Access
(Context : Node_Id;
Expr : Node_Id);
projects / platform / upstream / linaro-gcc.git / commitdiff