[multiple changes]
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. From-SVN: r207536
This commit is contained in:
parent
e2ef0ff683
commit
cbee4f7497
|
@ -1,3 +1,26 @@
|
|||
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
|
||||
|
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- 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- --
|
||||
|
@ -1384,6 +1384,10 @@ package body Ada.Calendar is
|
|||
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;
|
||||
|
||||
-------------
|
||||
|
|
|
@ -8887,7 +8887,18 @@ package body Exp_Ch6 is
|
|||
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;
|
||||
|
||||
|
|
|
@ -3118,6 +3118,8 @@ package body Sem_Ch12 is
|
|||
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.
|
||||
|
||||
|
|
|
@ -1193,6 +1193,8 @@ package body Sem_Ch6 is
|
|||
end loop;
|
||||
end;
|
||||
|
||||
Check_SPARK_Mode_In_Generic (N);
|
||||
|
||||
Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
|
||||
Set_SPARK_Pragma_Inherited (Body_Id, True);
|
||||
|
||||
|
|
|
@ -19217,10 +19217,6 @@ package body Sem_Prag is
|
|||
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
|
||||
|
@ -19233,9 +19229,15 @@ package body Sem_Prag is
|
|||
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
|
||||
|
@ -19258,8 +19260,7 @@ package body Sem_Prag is
|
|||
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;
|
||||
|
|
|
@ -23,6 +23,7 @@
|
|||
-- --
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
with Aspects; use Aspects;
|
||||
with Atree; use Atree;
|
||||
with Casing; use Casing;
|
||||
with Checks; use Checks;
|
||||
|
@ -2699,6 +2700,31 @@ package body Sem_Util is
|
|||
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 --
|
||||
------------------------------
|
||||
|
|
|
@ -62,6 +62,7 @@ package Sem_Util is
|
|||
-- Precondition
|
||||
-- Refined_Depends
|
||||
-- Refined_Global
|
||||
-- Refined_Post
|
||||
-- Refined_States
|
||||
-- Test_Case
|
||||
|
||||
|
@ -289,6 +290,10 @@ package Sem_Util is
|
|||
-- 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);
|
||||
|
|
Loading…
Reference in New Issue