+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,
-- 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
(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
(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
-- 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
-- | | | | |
-- +--+ +--+ +---+ | +---+
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;
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;
-----------------------
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;
--------------------
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
--------------------
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 --
----------------------
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 --
Message : String := "")
is
X : constant EOA := Exception_Propagation.Allocate_Occurrence;
+
begin
Exception_Data.Set_Exception_Msg (X, E, Message);
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
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;
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,
begin
if X.Id = null then
return;
+ else
+ Reraise_Occurrence_Always (X);
end if;
-
- Reraise_Occurrence_Always (X);
end Reraise_Occurrence;
-------------------------------
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;
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;
-- 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.
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);
("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;
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;
end SPARK_Mode;
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
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>>
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
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
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;
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
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;
projects / platform / upstream / gcc.git / commitdiff