+2017-12-05 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * 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 <setton@adacore.com>
+
+ * 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 <hainque@adacore.com>
+
+ * libgnat/s-tsmona.adb: Fix for oversight in the tsmona interface
+ update.
+
+2017-12-05 Gary Dismukes <dismukes@adacore.com>
+
+ * doc/gnat_ugn/elaboration_order_handling_in_gnat.rst: Minor typo fix
+ and reformatting.
+ * gnat_ugn.texi: Regenerate.
+
+2017-12-05 Olivier Hainque <hainque@adacore.com>
+
+ * sem_util.adb (Set_Convention): Always clear Can_Use_Internal_Rep
+ on access to subprogram types with foreign convention.
+
+2017-12-05 Yannick Moy <moy@adacore.com>
+
+ * doc/gnat_ugn/building_executable_programs_with_gnat.rst: Fix User's
+ Guide description of default settings of warnings.
+
2017-12-05 Olivier Hainque <hainque@adacore.com>
* s-dwalin.adb (Read_And_Execute_Isn): Adjust test checking for the end
* :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`
* :switch:`-gnatwn`
+ * :switch:`-gnatw.N`
+
* :switch:`-gnatwo`
* :switch:`-gnatw.O`
* :switch:`-gnatwT`
- * :switch:`-gnatw.T`
+ * :switch:`-gnatw.t`
* :switch:`-gnatwU`
+ * :switch:`-gnatw.U`
+
* :switch:`-gnatwv`
+ * :switch:`-gnatw.v`
+
* :switch:`-gnatww`
* :switch:`-gnatw.W`
* :switch:`-gnatwy`
+ * :switch:`-gnatw.Y`
+
* :switch:`-gnatwz`
+ * :switch:`-gnatw.z`
+
.. _Debugging_and_Assertion_Control:
Debugging and Assertion Control
* *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`.
: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.
@item
@code{-gnatwD}
+@item
+@code{-gnatw.D}
+
@item
@code{-gnatwF}
+@item
+@code{-gnatw.F}
+
@item
@code{-gnatwg}
@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
@code{-gnatwn}
+@item
+@code{-gnatw.N}
+
@item
@code{-gnatwo}
@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
@code{-gnatwy}
+@item
+@code{-gnatw.Y}
+
@item
@code{-gnatwz}
+
+@item
+@code{-gnatw.z}
@end itemize
@end quotation
@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
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
-- 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 "";
-- 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.
-- calls to subprograms which verify the run-time semantics of
-- the following assertion pragmas:
--
+ -- Default_Initial_Condition
+ -- Initial_Condition
-- Invariant
-- Invariant'Class
-- Post
-- 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
--
-- 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
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);
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)
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
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.
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
#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 */
/* 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
projects / gcc.git / commitdiff