From b91f986b2d9cd7c80dea854258a9f078d61345a9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie de Rodat Date: Tue, 5 Dec 2017 12:22:46 +0000 Subject: [PATCH] [multiple changes] 2017-12-05 Hristian Kirtchev * sem_elab.adb: Update the terminology and switch sections. (Check_SPARK_Model_In_Effect): New routine. (Check_SPARK_Scenario): Verify the model in effect for SPARK. (Process_Conditional_ABE_Call_SPARK): Verify the model in effect for SPARK. (Process_Conditional_ABE_Instantiation_SPARK): Verify the model in effect for SPARK. (Process_Conditional_ABE_Variable_Assignment_SPARK): Verify the model in effect for SPARK. 2017-12-05 Nicolas Setton * terminals.c (__gnat_setup_child_communication): As documented, __gnat_setup_child_communication should not terminate - it is intended to be used as the child process of a call to fork(). However, execvp might actually return in some cases, for instance when attempting to run a 32-bit binary on a 64-bit Linux distribution when the compatibility packages are not installed. In these cases, exit the program to conform to the documentation. 2017-12-05 Olivier Hainque * libgnat/s-tsmona.adb: Fix for oversight in the tsmona interface update. 2017-12-05 Gary Dismukes * doc/gnat_ugn/elaboration_order_handling_in_gnat.rst: Minor typo fix and reformatting. * gnat_ugn.texi: Regenerate. 2017-12-05 Olivier Hainque * sem_util.adb (Set_Convention): Always clear Can_Use_Internal_Rep on access to subprogram types with foreign convention. 2017-12-05 Yannick Moy * doc/gnat_ugn/building_executable_programs_with_gnat.rst: Fix User's Guide description of default settings of warnings. From-SVN: r255413 --- gcc/ada/ChangeLog | 43 +++++++++++++ .../building_executable_programs_with_gnat.rst | 24 ++++++- .../elaboration_order_handling_in_gnat.rst | 4 +- gcc/ada/gnat_ugn.texi | 37 +++++++++-- gcc/ada/libgnat/s-tsmona.adb | 6 +- gcc/ada/sem_elab.adb | 75 +++++++++++++++++++++- gcc/ada/sem_util.adb | 12 +--- gcc/ada/terminals.c | 5 +- 8 files changed, 179 insertions(+), 27 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 3507a1f..653d1e9 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,46 @@ +2017-12-05 Hristian Kirtchev + + * sem_elab.adb: Update the terminology and switch sections. + (Check_SPARK_Model_In_Effect): New routine. + (Check_SPARK_Scenario): Verify the model in effect for SPARK. + (Process_Conditional_ABE_Call_SPARK): Verify the model in effect for + SPARK. + (Process_Conditional_ABE_Instantiation_SPARK): Verify the model in + effect for SPARK. + (Process_Conditional_ABE_Variable_Assignment_SPARK): Verify the model + in effect for SPARK. + +2017-12-05 Nicolas Setton + + * terminals.c (__gnat_setup_child_communication): As documented, + __gnat_setup_child_communication should not terminate - it is intended + to be used as the child process of a call to fork(). However, execvp + might actually return in some cases, for instance when attempting to + run a 32-bit binary on a 64-bit Linux distribution when the + compatibility packages are not installed. In these cases, exit the + program to conform to the documentation. + +2017-12-05 Olivier Hainque + + * libgnat/s-tsmona.adb: Fix for oversight in the tsmona interface + update. + +2017-12-05 Gary Dismukes + + * doc/gnat_ugn/elaboration_order_handling_in_gnat.rst: Minor typo fix + and reformatting. + * gnat_ugn.texi: Regenerate. + +2017-12-05 Olivier Hainque + + * sem_util.adb (Set_Convention): Always clear Can_Use_Internal_Rep + on access to subprogram types with foreign convention. + +2017-12-05 Yannick Moy + + * doc/gnat_ugn/building_executable_programs_with_gnat.rst: Fix User's + Guide description of default settings of warnings. + 2017-12-05 Olivier Hainque * s-dwalin.adb (Read_And_Execute_Isn): Adjust test checking for the end diff --git a/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst b/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst index b6447d0..802e905 100644 --- a/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst +++ b/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst @@ -4075,20 +4075,28 @@ When no switch :switch:`-gnatw` is used, this is equivalent to: * :switch:`-gnatwD` + * :switch:`-gnatw.D` + * :switch:`-gnatwF` + * :switch:`-gnatw.F` + * :switch:`-gnatwg` * :switch:`-gnatwH` - * :switch:`-gnatwi` + * :switch:`-gnatw.H` - * :switch:`-gnatw.I` + * :switch:`-gnatwi` * :switch:`-gnatwJ` + * :switch:`-gnatw.J` + * :switch:`-gnatwK` + * :switch:`-gnatw.K` + * :switch:`-gnatwL` * :switch:`-gnatw.L` @@ -4099,6 +4107,8 @@ When no switch :switch:`-gnatw` is used, this is equivalent to: * :switch:`-gnatwn` + * :switch:`-gnatw.N` + * :switch:`-gnatwo` * :switch:`-gnatw.O` @@ -4119,12 +4129,16 @@ When no switch :switch:`-gnatw` is used, this is equivalent to: * :switch:`-gnatwT` - * :switch:`-gnatw.T` + * :switch:`-gnatw.t` * :switch:`-gnatwU` + * :switch:`-gnatw.U` + * :switch:`-gnatwv` + * :switch:`-gnatw.v` + * :switch:`-gnatww` * :switch:`-gnatw.W` @@ -4135,8 +4149,12 @@ When no switch :switch:`-gnatw` is used, this is equivalent to: * :switch:`-gnatwy` + * :switch:`-gnatw.Y` + * :switch:`-gnatwz` + * :switch:`-gnatw.z` + .. _Debugging_and_Assertion_Control: Debugging and Assertion Control diff --git a/gcc/ada/doc/gnat_ugn/elaboration_order_handling_in_gnat.rst b/gcc/ada/doc/gnat_ugn/elaboration_order_handling_in_gnat.rst index d29a915..a4b8b7f 100644 --- a/gcc/ada/doc/gnat_ugn/elaboration_order_handling_in_gnat.rst +++ b/gcc/ada/doc/gnat_ugn/elaboration_order_handling_in_gnat.rst @@ -634,7 +634,7 @@ elaboration order and to diagnose elaboration problems. * *Legacy elaboration model* - In addition to the three elabortaion models outlined above, GNAT provides the + In addition to the three elaboration models outlined above, GNAT provides the elaboration model of pre-18.x versions referred to as `legacy elaboration model`. The legacy elaboration model is enabled with compiler switch :switch:`-gnatH`. @@ -1515,7 +1515,7 @@ the elaboration order chosen by the binder. :switch:`-gnatJ` Relaxed elaboration checking mode enabled - When this switch is in effect, GNAT will not process certain scenarios + When this switch is in effect, GNAT will not process certain scenarios, resulting in a more permissive elaboration model. Note that this may eliminate some diagnostics and run-time checks. diff --git a/gcc/ada/gnat_ugn.texi b/gcc/ada/gnat_ugn.texi index cc902b3..7987430 100644 --- a/gcc/ada/gnat_ugn.texi +++ b/gcc/ada/gnat_ugn.texi @@ -12729,27 +12729,39 @@ When no switch @code{-gnatw} is used, this is equivalent to: @code{-gnatwD} @item +@code{-gnatw.D} + +@item @code{-gnatwF} @item +@code{-gnatw.F} + +@item @code{-gnatwg} @item @code{-gnatwH} @item -@code{-gnatwi} +@code{-gnatw.H} @item -@code{-gnatw.I} +@code{-gnatwi} @item @code{-gnatwJ} @item +@code{-gnatw.J} + +@item @code{-gnatwK} @item +@code{-gnatw.K} + +@item @code{-gnatwL} @item @@ -12765,6 +12777,9 @@ When no switch @code{-gnatw} is used, this is equivalent to: @code{-gnatwn} @item +@code{-gnatw.N} + +@item @code{-gnatwo} @item @@ -12795,15 +12810,21 @@ When no switch @code{-gnatw} is used, this is equivalent to: @code{-gnatwT} @item -@code{-gnatw.T} +@code{-gnatw.t} @item @code{-gnatwU} @item +@code{-gnatw.U} + +@item @code{-gnatwv} @item +@code{-gnatw.v} + +@item @code{-gnatww} @item @@ -12819,7 +12840,13 @@ When no switch @code{-gnatw} is used, this is equivalent to: @code{-gnatwy} @item +@code{-gnatw.Y} + +@item @code{-gnatwz} + +@item +@code{-gnatw.z} @end itemize @end quotation @@ -27841,7 +27868,7 @@ effect. @item @emph{Legacy elaboration model} -In addition to the three elabortaion models outlined above, GNAT provides the +In addition to the three elaboration models outlined above, GNAT provides the elaboration model of pre-18.x versions referred to as @cite{legacy elaboration model}. The legacy elaboration model is enabled with compiler switch @code{-gnatH}. @end itemize @@ -28811,7 +28838,7 @@ model. Relaxed elaboration checking mode enabled -When this switch is in effect, GNAT will not process certain scenarios +When this switch is in effect, GNAT will not process certain scenarios, resulting in a more permissive elaboration model. Note that this may eliminate some diagnostics and run-time checks. @end table diff --git a/gcc/ada/libgnat/s-tsmona.adb b/gcc/ada/libgnat/s-tsmona.adb index 95edb6b..e04652d 100644 --- a/gcc/ada/libgnat/s-tsmona.adb +++ b/gcc/ada/libgnat/s-tsmona.adb @@ -48,8 +48,12 @@ package body Module_Name is -- Get -- --------- - function Get (Addr : access System.Address) return String is + function Get (Addr : System.Address; + Load_Addr : access System.Address) + return String + is pragma Unreferenced (Addr); + pragma Unreferenced (Load_Addr); begin return ""; diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb index 99f2dd1..b2e56e6 100644 --- a/gcc/ada/sem_elab.adb +++ b/gcc/ada/sem_elab.adb @@ -117,6 +117,9 @@ package body Sem_Elab is -- Terminology -- ----------------- + -- * ABE - An attempt to activate, call, or instantiate a scenario which + -- has not been fully elaborated. + -- -- * Bridge target - A type of target. A bridge target is a link between -- scenarios. It is usually a byproduct of expansion and does not have -- any direct ABE ramifications. @@ -421,6 +424,8 @@ package body Sem_Elab is -- calls to subprograms which verify the run-time semantics of -- the following assertion pragmas: -- + -- Default_Initial_Condition + -- Initial_Condition -- Invariant -- Invariant'Class -- Post @@ -429,8 +434,8 @@ package body Sem_Elab is -- Type_Invariant -- Type_Invariant_Class -- - -- As a result, the assertion expressions of the pragmas will not - -- be processed. + -- As a result, the assertion expressions of the pragmas are not + -- processed. -- -- -gnatd.U ignore indirect calls for static elaboration -- @@ -1044,6 +1049,12 @@ package body Sem_Elab is -- Verify that expanded instance Exp_Inst does not precede the generic body -- it instantiates (SPARK RM 7.7(6)). + procedure Check_SPARK_Model_In_Effect (N : Node_Id); + pragma Inline (Check_SPARK_Model_In_Effect); + -- Determine whether a suitable elaboration model is currently in effect + -- for verifying the SPARK rules of scenario N. Emit a warning if this is + -- not the case. + procedure Check_SPARK_Scenario (N : Node_Id); pragma Inline (Check_SPARK_Scenario); -- Top-level dispatcher for verifying SPARK scenarios which are not always @@ -2696,12 +2707,57 @@ package body Sem_Elab is end if; end Check_SPARK_Instantiation; + --------------------------------- + -- Check_SPARK_Model_In_Effect -- + --------------------------------- + + SPARK_Model_Warning_Posted : Boolean := False; + -- This flag prevents the same SPARK model-related warning from being + -- emitted multiple times. + + procedure Check_SPARK_Model_In_Effect (N : Node_Id) is + begin + -- Do not emit the warning multiple times as this creates useless noise + + if SPARK_Model_Warning_Posted then + null; + + -- SPARK rule verification requires the "strict" static model + + elsif Static_Elaboration_Checks and not Relaxed_Elaboration_Checks then + null; + + -- Any other combination of models does not guarantee the absence of ABE + -- problems for SPARK rule verification purposes. Note that there is no + -- need to check for the legacy ABE mechanism because the legacy code + -- has its own orthogonal processing for SPARK rules. + + else + SPARK_Model_Warning_Posted := True; + + Error_Msg_N + ("??SPARK elaboration checks require static elaboration model", N); + + if Dynamic_Elaboration_Checks then + Error_Msg_N ("\dynamic elaboration model is in effect", N); + else + pragma Assert (Relaxed_Elaboration_Checks); + Error_Msg_N ("\relaxed elaboration model is in effect", N); + end if; + end if; + end Check_SPARK_Model_In_Effect; + -------------------------- -- Check_SPARK_Scenario -- -------------------------- procedure Check_SPARK_Scenario (N : Node_Id) is begin + -- Ensure that a suitable elaboration model is in effect for SPARK rule + -- verification. + + Check_SPARK_Model_In_Effect (N); + -- Add the current scenario to the stack of active scenarios Push_Active_Scenario (N); @@ -9211,6 +9267,11 @@ package body Sem_Elab is Region : Node_Id; begin + -- Ensure that a suitable elaboration model is in effect for SPARK rule + -- verification. + + Check_SPARK_Model_In_Effect (Call); + -- The call and the target body are both in the main unit if Present (Target_Attrs.Body_Decl) @@ -9674,6 +9735,11 @@ package body Sem_Elab is Req_Nam : Name_Id; begin + -- Ensure that a suitable elaboration model is in effect for SPARK rule + -- verification. + + Check_SPARK_Model_In_Effect (Inst); + -- A source instantiation imposes an Elaborate[_All] requirement on the -- context of the main unit. Determine whether the context has a pragma -- strong enough to meet the requirement. The check is orthogonal to the @@ -9807,6 +9873,11 @@ package body Sem_Elab is Spec_Id : constant Entity_Id := Find_Top_Unit (Var_Decl); begin + -- Ensure that a suitable elaboration model is in effect for SPARK rule + -- verification. + + Check_SPARK_Model_In_Effect (Asmt); + -- Emit an error when an initialized variable declared in a package spec -- without pragma Elaborate_Body is further modified by elaboration code -- within the corresponding body. diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 3209df4..43e9ea2 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -23090,17 +23090,7 @@ package body Sem_Util is and then Is_Access_Subprogram_Type (Base_Type (E)) and then Has_Foreign_Convention (E) then - - -- A pragma Convention in an instance may apply to the subtype - -- created for a formal, in which case we have already verified - -- that conventions of actual and formal match and there is nothing - -- to flag on the subtype. - - if In_Instance then - null; - else - Set_Can_Use_Internal_Rep (E, False); - end if; + Set_Can_Use_Internal_Rep (E, False); end if; -- If E is an object, including a component, and the type of E is an diff --git a/gcc/ada/terminals.c b/gcc/ada/terminals.c index 9f30051..1e295af 100644 --- a/gcc/ada/terminals.c +++ b/gcc/ada/terminals.c @@ -1458,7 +1458,7 @@ __gnat_setup_child_communication #ifdef TIOCSCTTY /* make the tty the controlling terminal */ if ((status = ioctl (desc->slave_fd, TIOCSCTTY, 0)) == -1) - return -1; + _exit (1); #endif /* adjust tty settings */ @@ -1480,8 +1480,7 @@ __gnat_setup_child_communication /* launch the program */ execvp (new_argv[0], new_argv); - /* return the pid */ - return pid; + _exit (1); } /* send_signal_via_characters - Send a characters that will trigger a signal -- 2.7.4