[multiple changes]
2014-01-21 Thomas Quinot <quinot@adacore.com> * exp_pakd.adb: Update comment, minor reformatting. 2014-01-21 Hristian Kirtchev <kirtchev@adacore.com> * sem_ch3.adb (Analyze_Variable_Contract): Trigger the volatile object check when SPARK_Mode is on. * sem_ch6.adb (Process_Formals): Trigger the volatile object check when SPARK_Mode is on. * sem_ch12.adb (Instantiate_Object): Trigger the volatile object check when SPARK_Mode is on. * sem_ch13.adb (Analyze_Aspect_Specifications): Insert the corresponding pragma of aspect SPARK_Mode in the visible declarations of a package declaration. * sem_prag.adb (Analyze_Pragma): Trigger the volatile object check when SPARK_Mode is on. * sem_res.adb (Resolve_Actuals): Trigger the volatile object check when SPARK_Mode is on. (Resolve_Entity_Name): Trigger the volatile object check when SPARK_Mode is on. 2014-01-21 Robert Dewar <dewar@adacore.com> * a-except-2005.adb: Minor reformatting From-SVN: r206888
This commit is contained in:
Arnaud Charlet
parent
84f80f5bf1
commit
fb1fdf7d6b
|
|
@ -1,3 +1,25 @@
|
|||
2014-01-21 Thomas Quinot <quinot@adacore.com>
|
||||
|
||||
* exp_pakd.adb: Update comment, minor reformatting.
|
||||
|
||||
2014-01-21 Hristian Kirtchev <kirtchev@adacore.com>
|
||||
|
||||
* sem_ch3.adb (Analyze_Variable_Contract): Trigger the volatile
|
||||
object check when SPARK_Mode is on.
|
||||
* sem_ch6.adb (Process_Formals): Trigger the volatile object
|
||||
check when SPARK_Mode is on.
|
||||
* sem_ch12.adb (Instantiate_Object): Trigger the volatile object
|
||||
check when SPARK_Mode is on.
|
||||
* sem_ch13.adb (Analyze_Aspect_Specifications): Insert the
|
||||
corresponding pragma of aspect SPARK_Mode in the visible
|
||||
declarations of a package declaration.
|
||||
* sem_prag.adb (Analyze_Pragma): Trigger the volatile object
|
||||
check when SPARK_Mode is on.
|
||||
* sem_res.adb (Resolve_Actuals): Trigger the volatile object
|
||||
check when SPARK_Mode is on.
|
||||
(Resolve_Entity_Name): Trigger
|
||||
the volatile object check when SPARK_Mode is on.
|
||||
|
||||
2014-01-21 Robert Dewar <dewar@adacore.com>
|
||||
|
||||
* sem_ch3.adb, sem_prag.adb, sem_prag.ads, sem_ch12.adb, sem_res.adb,
|
||||
|
|
|
|||
|
|
@ -315,12 +315,9 @@ package body Ada.Exceptions is
|
|||
-- occurrence and in addition a column and a string message M may be
|
||||
-- appended to this (if not null/0).
|
||||
|
||||
procedure Raise_Constraint_Error
|
||||
(File : System.Address;
|
||||
Line : Integer);
|
||||
procedure Raise_Constraint_Error (File : System.Address; Line : Integer);
|
||||
pragma No_Return (Raise_Constraint_Error);
|
||||
pragma Export
|
||||
(C, Raise_Constraint_Error, "__gnat_raise_constraint_error");
|
||||
pragma Export (C, Raise_Constraint_Error, "__gnat_raise_constraint_error");
|
||||
-- Raise constraint error with file:line information
|
||||
|
||||
procedure Raise_Constraint_Error_Msg
|
||||
|
|
@ -333,12 +330,9 @@ package body Ada.Exceptions is
|
|||
(C, Raise_Constraint_Error_Msg, "__gnat_raise_constraint_error_msg");
|
||||
-- Raise constraint error with file:line:col + msg information
|
||||
|
||||
procedure Raise_Program_Error
|
||||
(File : System.Address;
|
||||
Line : Integer);
|
||||
procedure Raise_Program_Error (File : System.Address; Line : Integer);
|
||||
pragma No_Return (Raise_Program_Error);
|
||||
pragma Export
|
||||
(C, Raise_Program_Error, "__gnat_raise_program_error");
|
||||
pragma Export (C, Raise_Program_Error, "__gnat_raise_program_error");
|
||||
-- Raise program error with file:line information
|
||||
|
||||
procedure Raise_Program_Error_Msg
|
||||
|
|
@ -350,12 +344,9 @@ package body Ada.Exceptions is
|
|||
(C, Raise_Program_Error_Msg, "__gnat_raise_program_error_msg");
|
||||
-- Raise program error with file:line + msg information
|
||||
|
||||
procedure Raise_Storage_Error
|
||||
(File : System.Address;
|
||||
Line : Integer);
|
||||
procedure Raise_Storage_Error (File : System.Address; Line : Integer);
|
||||
pragma No_Return (Raise_Storage_Error);
|
||||
pragma Export
|
||||
(C, Raise_Storage_Error, "__gnat_raise_storage_error");
|
||||
pragma Export (C, Raise_Storage_Error, "__gnat_raise_storage_error");
|
||||
-- Raise storage error with file:line information
|
||||
|
||||
procedure Raise_Storage_Error_Msg
|
||||
|
|
@ -372,10 +363,10 @@ package body Ada.Exceptions is
|
|||
-- graph below illustrates the relations between the Raise_ subprograms
|
||||
-- and identifies the points where basic flags such as Exception_Raised
|
||||
-- are initialized.
|
||||
--
|
||||
|
||||
-- (i) signs indicate the flags initialization points. R stands for Raise,
|
||||
-- W for With, and E for Exception.
|
||||
--
|
||||
|
||||
-- R_No_Msg R_E R_Pe R_Ce R_Se
|
||||
-- | | | | |
|
||||
-- +--+ +--+ +---+ | +---+
|
||||
|
|
@ -391,10 +382,10 @@ package body Ada.Exceptions is
|
|||
procedure Reraise;
|
||||
pragma No_Return (Reraise);
|
||||
pragma Export (C, Reraise, "__gnat_reraise");
|
||||
-- Reraises the exception referenced by the Current_Excep field of
|
||||
-- the TSD (all fields of this exception occurrence are set). Abort
|
||||
-- is deferred before the reraise operation.
|
||||
-- Called from System.Tasking.RendezVous.Exceptional_Complete_RendezVous
|
||||
-- Reraises the exception referenced by the Current_Excep field
|
||||
-- of the TSD (all fields of this exception occurrence are set).
|
||||
-- Abort is deferred before the reraise operation. Called from
|
||||
-- System.Tasking.RendezVous.Exceptional_Complete_RendezVous
|
||||
|
||||
procedure Transfer_Occurrence
|
||||
(Target : Exception_Occurrence_Access;
|
||||
|
|
@ -774,9 +765,9 @@ package body Ada.Exceptions is
|
|||
begin
|
||||
if X.Id = Null_Id then
|
||||
raise Constraint_Error;
|
||||
else
|
||||
return Exception_Data.Exception_Information (X);
|
||||
end if;
|
||||
|
||||
return Exception_Data.Exception_Information (X);
|
||||
end Exception_Information;
|
||||
|
||||
-----------------------
|
||||
|
|
@ -787,9 +778,9 @@ package body Ada.Exceptions is
|
|||
begin
|
||||
if X.Id = Null_Id then
|
||||
raise Constraint_Error;
|
||||
else
|
||||
return X.Msg (1 .. X.Msg_Length);
|
||||
end if;
|
||||
|
||||
return X.Msg (1 .. X.Msg_Length);
|
||||
end Exception_Message;
|
||||
|
||||
--------------------
|
||||
|
|
@ -800,9 +791,9 @@ package body Ada.Exceptions is
|
|||
begin
|
||||
if Id = null then
|
||||
raise Constraint_Error;
|
||||
else
|
||||
return To_Ptr (Id.Full_Name) (1 .. Id.Name_Length - 1);
|
||||
end if;
|
||||
|
||||
return To_Ptr (Id.Full_Name) (1 .. Id.Name_Length - 1);
|
||||
end Exception_Name;
|
||||
|
||||
function Exception_Name (X : Exception_Occurrence) return String is
|
||||
|
|
@ -839,8 +830,8 @@ package body Ada.Exceptions is
|
|||
--------------------
|
||||
|
||||
package body Exception_Data is separate;
|
||||
-- This package can be easily dummied out if we do not want the
|
||||
-- basic support for exception messages (such as in Ada 83).
|
||||
-- This package can be easily dummied out if we do not want the basic
|
||||
-- support for exception messages (such as in Ada 83).
|
||||
|
||||
---------------------------
|
||||
-- Exception_Propagation --
|
||||
|
|
@ -856,10 +847,10 @@ package body Ada.Exceptions is
|
|||
----------------------
|
||||
|
||||
package body Exception_Traces is separate;
|
||||
-- Depending on the underlying support for IO the implementation
|
||||
-- will differ. Moreover we would like to dummy out this package
|
||||
-- in case we do not want any exception tracing support. This is
|
||||
-- why this package is separated.
|
||||
-- Depending on the underlying support for IO the implementation will
|
||||
-- differ. Moreover we would like to dummy out this package in case we
|
||||
-- do not want any exception tracing support. This is why this package
|
||||
-- is separated.
|
||||
|
||||
--------------------------------------
|
||||
-- Get_Exception_Machine_Occurrence --
|
||||
|
|
@ -1011,6 +1002,7 @@ package body Ada.Exceptions is
|
|||
Message : String := "")
|
||||
is
|
||||
X : constant EOA := Exception_Propagation.Allocate_Occurrence;
|
||||
|
||||
begin
|
||||
Exception_Data.Set_Exception_Msg (X, E, Message);
|
||||
|
||||
|
|
@ -1029,10 +1021,11 @@ package body Ada.Exceptions is
|
|||
Prefix : constant String := "adjust/finalize raised ";
|
||||
Orig_Msg : constant String := Exception_Message (X);
|
||||
Orig_Prefix_Length : constant Natural :=
|
||||
Integer'Min (Prefix'Length, Orig_Msg'Length);
|
||||
Orig_Prefix : String renames Orig_Msg
|
||||
(Orig_Msg'First ..
|
||||
Orig_Msg'First + Orig_Prefix_Length - 1);
|
||||
Integer'Min (Prefix'Length, Orig_Msg'Length);
|
||||
|
||||
Orig_Prefix : String renames
|
||||
Orig_Msg (Orig_Msg'First .. Orig_Msg'First + Orig_Prefix_Length - 1);
|
||||
|
||||
begin
|
||||
-- Message already has the proper prefix, just re-raise
|
||||
|
||||
|
|
@ -1526,6 +1519,7 @@ package body Ada.Exceptions is
|
|||
procedure Reraise is
|
||||
Excep : constant EOA := Exception_Propagation.Allocate_Occurrence;
|
||||
Saved_MO : constant System.Address := Excep.Machine_Occurrence;
|
||||
|
||||
begin
|
||||
if not ZCX_By_Default then
|
||||
Abort_Defer.all;
|
||||
|
|
@ -1542,9 +1536,11 @@ package body Ada.Exceptions is
|
|||
|
||||
procedure Reraise_Library_Exception_If_Any is
|
||||
LE : Exception_Occurrence;
|
||||
|
||||
begin
|
||||
if Library_Exception_Set then
|
||||
LE := Library_Exception;
|
||||
|
||||
if LE.Id = Null_Id then
|
||||
Raise_Exception_No_Defer
|
||||
(E => Program_Error'Identity,
|
||||
|
|
@ -1563,9 +1559,9 @@ package body Ada.Exceptions is
|
|||
begin
|
||||
if X.Id = null then
|
||||
return;
|
||||
else
|
||||
Reraise_Occurrence_Always (X);
|
||||
end if;
|
||||
|
||||
Reraise_Occurrence_Always (X);
|
||||
end Reraise_Occurrence;
|
||||
|
||||
-------------------------------
|
||||
|
|
@ -1646,10 +1642,8 @@ package body Ada.Exceptions is
|
|||
|
||||
procedure To_Stderr (C : Character) is
|
||||
type int is new Integer;
|
||||
|
||||
procedure put_char_stderr (C : int);
|
||||
pragma Import (C, put_char_stderr, "put_char_stderr");
|
||||
|
||||
begin
|
||||
put_char_stderr (Character'Pos (C));
|
||||
end To_Stderr;
|
||||
|
|
@ -1681,7 +1675,6 @@ package body Ada.Exceptions is
|
|||
|
||||
function Triggered_By_Abort return Boolean is
|
||||
Ex : constant Exception_Occurrence_Access := Get_Current_Excep.all;
|
||||
|
||||
begin
|
||||
return Ex /= null
|
||||
and then Exception_Identity (Ex.all) = Standard'Abort_Signal'Identity;
|
||||
|
|
|
|||
|
|
@ -1127,7 +1127,7 @@ package body Exp_Pakd is
|
|||
|
||||
-- The name of the packed array subtype is
|
||||
|
||||
-- ttt___Xsss
|
||||
-- ttt___XPsss
|
||||
|
||||
-- where sss is the component size in bits and ttt is the name of
|
||||
-- the parent packed type.
|
||||
|
|
@ -1565,7 +1565,7 @@ package body Exp_Pakd is
|
|||
declare
|
||||
T : constant Entity_Id := Etype (Obj);
|
||||
begin
|
||||
New_Lhs := Duplicate_Subexpr (Obj, True);
|
||||
New_Lhs := Duplicate_Subexpr (Obj, Name_Req => True);
|
||||
New_Rhs := Duplicate_Subexpr_No_Checks (Obj);
|
||||
Set_Etype (Obj, T);
|
||||
Set_Etype (New_Lhs, T);
|
||||
|
|
|
|||
|
|
@ -9840,17 +9840,14 @@ package body Sem_Ch12 is
|
|||
("actual must exclude null to match generic formal#", Actual);
|
||||
end if;
|
||||
|
||||
-- The following check is only relevant in formal verification mode as
|
||||
-- it is not a standard Ada legality rule. A volatile object cannot be
|
||||
-- used as an actual in a generic instantiation.
|
||||
-- A volatile object cannot be used as an actual in a generic instance.
|
||||
-- The following check is only relevant when SPARK_Mode is on as it is
|
||||
-- not a standard Ada legality rule.
|
||||
|
||||
-- Should mention that this is a rule for SPARK only, perhaps with
|
||||
-- a SPARK RM reference???
|
||||
|
||||
if GNATprove_Mode and then Is_Volatile_Object (Actual) then
|
||||
if SPARK_Mode = On and then Is_Volatile_Object (Actual) then
|
||||
Error_Msg_N
|
||||
("volatile object cannot act as actual in generic instantiation",
|
||||
Actual);
|
||||
("volatile object cannot act as actual in generic instantiation "
|
||||
& "(SPARK RM 7.1.3(4))", Actual);
|
||||
end if;
|
||||
|
||||
return List;
|
||||
|
|
|
|||
|
|
@ -2155,6 +2155,22 @@ package body Sem_Ch13 is
|
|||
Set_Declarations (N, Decls);
|
||||
end if;
|
||||
|
||||
Prepend_To (Decls, Aitem);
|
||||
goto Continue;
|
||||
|
||||
-- When the aspect is associated with package declaration,
|
||||
-- insert the generated pragma at the top of the visible
|
||||
-- declarations to emulate the behavior of a source pragma.
|
||||
|
||||
elsif Nkind (N) = N_Package_Declaration then
|
||||
Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
|
||||
Decls := Visible_Declarations (Specification (N));
|
||||
|
||||
if No (Decls) then
|
||||
Decls := New_List;
|
||||
Set_Visible_Declarations (Specification (N), Decls);
|
||||
end if;
|
||||
|
||||
Prepend_To (Decls, Aitem);
|
||||
goto Continue;
|
||||
end if;
|
||||
|
|
|
|||
|
|
@ -4801,16 +4801,17 @@ package body Sem_Ch3 is
|
|||
Seen : Boolean := False;
|
||||
|
||||
begin
|
||||
-- The following check is only relevant in formal verification mode as
|
||||
-- it is not standard Ada legality rule. The declaration of a volatile
|
||||
-- variable must appear at the library level.
|
||||
-- The declaration of a volatile variable must appear at the library
|
||||
-- level. The check is only relevant when SPARK_Mode is on as it is not
|
||||
-- standard Ada legality rule.
|
||||
|
||||
if GNATprove_Mode
|
||||
if SPARK_Mode = On
|
||||
and then Is_Volatile_Object (Var_Id)
|
||||
and then not Is_Library_Level_Entity (Var_Id)
|
||||
then
|
||||
Error_Msg_N
|
||||
("volatile variable & must be declared at library level", Var_Id);
|
||||
("volatile variable & must be declared at library level (SPARK RM "
|
||||
& "7.1.3(3))", Var_Id);
|
||||
end if;
|
||||
|
||||
-- Examine the contract
|
||||
|
|
|
|||
|
|
@ -11117,18 +11117,17 @@ package body Sem_Ch6 is
|
|||
Null_Exclusion_Static_Checks (Param_Spec);
|
||||
end if;
|
||||
|
||||
-- The following check is only relevant in formal verification mode
|
||||
-- as it is not a standard Ada legality rule. A function cannot have
|
||||
-- a volatile formal parameter.
|
||||
-- A function cannot have a volatile formal parameter. The following
|
||||
-- check is relevant when SPARK_Mode is on as it is not a standard
|
||||
-- Ada legality rule.
|
||||
|
||||
-- Need to mention this is a SPARK rule, with SPARK RM reference ???
|
||||
|
||||
if GNATprove_Mode
|
||||
if SPARK_Mode = On
|
||||
and then Is_Volatile_Object (Formal)
|
||||
and then Ekind_In (Scope (Formal), E_Function, E_Generic_Function)
|
||||
then
|
||||
Error_Msg_N
|
||||
("function cannot have a volatile formal parameter", Formal);
|
||||
("function cannot have a volatile formal parameter (SPARK RM "
|
||||
& "7.1.3(6))", Formal);
|
||||
end if;
|
||||
|
||||
<<Continue>>
|
||||
|
|
|
|||
|
|
@ -1877,14 +1877,17 @@ package body Sem_Prag is
|
|||
Check_Mode_Restriction_In_Enclosing_Context (Item, Item_Id);
|
||||
end if;
|
||||
|
||||
-- A volatile object cannot appear as a global item of a function
|
||||
-- A volatile object cannot appear as a global item of a function.
|
||||
-- This check is only relevant when SPARK_Mode is on as it is not
|
||||
-- a standard Ada legality rule.
|
||||
|
||||
if Is_Volatile_Object (Item)
|
||||
if SPARK_Mode = On
|
||||
and then Is_Volatile_Object (Item)
|
||||
and then Ekind_In (Spec_Id, E_Function, E_Generic_Function)
|
||||
then
|
||||
Error_Msg_N
|
||||
("volatile object cannot act as global item of a function",
|
||||
Item);
|
||||
("volatile object cannot act as global item of a function "
|
||||
& "(SPARK RM 7.1.3(5))", Item);
|
||||
end if;
|
||||
|
||||
-- The same entity might be referenced through various way. Check
|
||||
|
|
|
|||
|
|
@ -4249,10 +4249,10 @@ package body Sem_Res is
|
|||
Check_Unset_Reference (A);
|
||||
end if;
|
||||
|
||||
-- The following checks are only relevant in formal verification
|
||||
-- mode as they are not standard Ada legality rule.
|
||||
-- The following checks are only relevant when SPARK_Mode is on as
|
||||
-- they are not standard Ada legality rule.
|
||||
|
||||
if GNATprove_Mode
|
||||
if SPARK_Mode = On
|
||||
and then Is_Volatile_Object (A)
|
||||
then
|
||||
-- A volatile object may act as an actual parameter when the
|
||||
|
|
@ -4270,11 +4270,9 @@ package body Sem_Res is
|
|||
null;
|
||||
|
||||
else
|
||||
-- Error message should mention SPARK, and perhaps give
|
||||
-- a SPARK RM reference ???
|
||||
|
||||
Error_Msg_N
|
||||
("volatile object cannot act as actual in a call", A);
|
||||
("volatile object cannot act as actual in a call (SPARK "
|
||||
& "RM 7.1.3(8))", A);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
|
|
@ -6459,12 +6457,12 @@ package body Sem_Res is
|
|||
Eval_Entity_Name (N);
|
||||
end if;
|
||||
|
||||
-- The following checks are only relevant in formal verification mode as
|
||||
-- they are not standard Ada legality rule. A volatile object subject to
|
||||
-- enabled properties Async_Writers or Effective_Reads must appear in a
|
||||
-- specific context.
|
||||
-- A volatile object subject to enabled properties Async_Writers or
|
||||
-- Effective_Reads must appear in a specific context. The following
|
||||
-- checks are only relevant when SPARK_Mode is on as they are not
|
||||
-- standard Ada legality rules.
|
||||
|
||||
if GNATprove_Mode
|
||||
if SPARK_Mode = On
|
||||
and then Ekind (E) = E_Variable
|
||||
and then Is_Volatile_Object (E)
|
||||
and then
|
||||
|
|
@ -6520,10 +6518,10 @@ package body Sem_Res is
|
|||
Par := Parent (Par);
|
||||
end loop;
|
||||
|
||||
-- Message should mention SPARK, and perhaps SPARK RM ref ???
|
||||
|
||||
if not Usage_OK then
|
||||
Error_Msg_N ("volatile object cannot appear in this context", N);
|
||||
Error_Msg_N
|
||||
("volatile object cannot appear in this context (SPARK RM "
|
||||
& "7.1.3(9))", N);
|
||||
end if;
|
||||
end if;
|
||||
end Resolve_Entity_Name;
|
||||
|
|
|
|||
Loading…
Reference in New Issue