diff options
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 22 | ||||
| -rw-r--r-- | gcc/ada/a-except-2005.adb | 77 | ||||
| -rw-r--r-- | gcc/ada/exp_pakd.adb | 4 | ||||
| -rw-r--r-- | gcc/ada/sem_ch12.adb | 15 | ||||
| -rw-r--r-- | gcc/ada/sem_ch13.adb | 16 | ||||
| -rw-r--r-- | gcc/ada/sem_ch3.adb | 11 | ||||
| -rw-r--r-- | gcc/ada/sem_ch6.adb | 13 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 11 | ||||
| -rw-r--r-- | gcc/ada/sem_res.adb | 28 |
9 files changed, 113 insertions, 84 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 6bb46e7..fccd692 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -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, diff --git a/gcc/ada/a-except-2005.adb b/gcc/ada/a-except-2005.adb index 4fc60e5..9d6354c 100644 --- a/gcc/ada/a-except-2005.adb +++ b/gcc/ada/a-except-2005.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; diff --git a/gcc/ada/exp_pakd.adb b/gcc/ada/exp_pakd.adb index 0baab98..601030c 100644 --- a/gcc/ada/exp_pakd.adb +++ b/gcc/ada/exp_pakd.adb @@ -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); diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 0e2787f..b59c895 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -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; diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 630892a..736a8ae 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -2157,6 +2157,22 @@ package body Sem_Ch13 is 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; diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 99f85cb..5d27710 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -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 diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index edf2c84..7cde513 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -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>> diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 54ef5f3..e533d26 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -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 diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index c308ed7..c42a7fa 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -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; |