From ed37f25a36339a3c198c0c8d0d9e07735897d3cd Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Fri, 23 Oct 2015 12:44:35 +0200 Subject: [PATCH] [multiple changes] 2015-10-23 Gary Dismukes * bindgen.adb, restrict.adb: Minor spelling/grammar fixes. 2015-10-23 Hristian Kirtchev * sem_res.adb (Resolve_Entity_Name): Code cleanup. Check for possible elaboration issues in SPARK when the name denotes a source variable. From-SVN: r229228 --- gcc/ada/ChangeLog | 9 ++++++++ gcc/ada/bindgen.adb | 4 ++-- gcc/ada/restrict.adb | 2 +- gcc/ada/sem_res.adb | 58 ++++++++++++++++++++++++---------------------------- 4 files changed, 39 insertions(+), 34 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 03a8dd9..5235631 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,12 @@ +2015-10-23 Gary Dismukes + + * bindgen.adb, restrict.adb: Minor spelling/grammar fixes. + +2015-10-23 Hristian Kirtchev + + * sem_res.adb (Resolve_Entity_Name): Code cleanup. Check for possible + elaboration issues in SPARK when the name denotes a source variable. + 2015-10-23 Hristian Kirtchev * exp_ch7.adb (Process_Transient_Objects): Reimplement to properly diff --git a/gcc/ada/bindgen.adb b/gcc/ada/bindgen.adb index eb853b5..cf4b59f 100644 --- a/gcc/ada/bindgen.adb +++ b/gcc/ada/bindgen.adb @@ -2810,8 +2810,8 @@ package body Bindgen is procedure Check_Package (Var : in out Boolean; Name : String); -- Set Var to true iff the current identifier in Namet is Name. Do - -- nothing if it doesn't match. This procedure is just an helper to - -- avoid to explicitely deal with length. + -- nothing if it doesn't match. This procedure is just a helper to + -- avoid explicitly dealing with length. ------------------- -- Check_Package -- diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb index 37f579b..b63b426 100644 --- a/gcc/ada/restrict.adb +++ b/gcc/ada/restrict.adb @@ -503,7 +503,7 @@ package body Restrict is -- so that we have consistency between each compilation. -- In GNATprove mode restrictions are checked, except for - -- No_Initialize_Scalars, which is implicitely set in gnat1drv.adb. + -- No_Initialize_Scalars, which is implicitly set in gnat1drv.adb. -- Just checking, SPARK does not allow restrictions to be set ??? diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 0a0c289..62f82eb 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -7179,44 +7179,40 @@ package body Sem_Res is Par := Parent (Par); end if; - -- The following checks are only relevant when SPARK_Mode is on as they - -- are not standard Ada legality rules. An effectively volatile object - -- subject to enabled properties Async_Writers or Effective_Reads must - -- appear in a specific context. - - if SPARK_Mode = On - and then Is_Object (E) - and then Is_Effectively_Volatile (E) - and then (Async_Writers_Enabled (E) - or else Effective_Reads_Enabled (E)) - and then Comes_From_Source (N) - then - -- The effectively volatile objects appears in a "non-interfering - -- context" as defined in SPARK RM 7.1.3(12). + if Comes_From_Source (N) then - if Is_OK_Volatile_Context (Par, N) then - null; + -- The following checks are only relevant when SPARK_Mode is on as + -- they are not standard Ada legality rules. - -- Otherwise the context causes a side effect with respect to the - -- effectively volatile object. + if SPARK_Mode = On then - else - SPARK_Msg_N - ("volatile object cannot appear in this context " - & "(SPARK RM 7.1.3(12))", N); - end if; - end if; + -- An effectively volatile object subject to enabled properties + -- Async_Writers or Effective_Reads must appear in non-interfering + -- context (SPARK RM 7.1.3(12)). - -- A Ghost entity must appear in a specific context + if Is_Object (E) + and then Is_Effectively_Volatile (E) + and then (Async_Writers_Enabled (E) + or else Effective_Reads_Enabled (E)) + and then not Is_OK_Volatile_Context (Par, N) + then + SPARK_Msg_N + ("volatile object cannot appear in this context " + & "(SPARK RM 7.1.3(12))", N); + end if; - if Is_Ghost_Entity (E) and then Comes_From_Source (N) then - Check_Ghost_Context (E, N); - end if; + -- Check possible elaboration issues with respect to variables + + if Ekind (E) = E_Variable then + Check_Elab_Call (N); + end if; + end if; - -- In SPARK mode, need to check possible elaboration issues + -- A Ghost entity must appear in a specific context - if SPARK_Mode = On and then Ekind (E) = E_Variable then - Check_Elab_Call (N); + if Is_Ghost_Entity (E) then + Check_Ghost_Context (E, N); + end if; end if; end Resolve_Entity_Name; -- 2.7.4