===================================================================
@@ -117,6 +117,9 @@
-- 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 @@
-- 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 @@
-- 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 @@
-- 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 @@
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 @@
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 @@
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 @@
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.
This patch introduces a check which ensures that SPARK elaboration code is processed using the static elaboration model as it guarantees the highest degree of safety. ------------ -- Source -- ------------ -- spark_pack.ads package SPARK_Pack with SPARK_Mode is pragma Elaborate_Body; type Root is tagged null record; procedure Prim (Obj : Root); type Child is new Root with null record; procedure Prim (Obj : Child); end SPARK_Pack; -- spark_pack.adb with Ada.Text_IO; use Ada.Text_IO; package body SPARK_Pack with SPARK_Mode is procedure Prim (Obj : Root) is begin Put_Line ("Root.Prim"); end Prim; procedure Prim (Obj : Child) is begin Put_Line ("Child.Prim"); end Prim; end SPARK_Pack; ---------------------------- -- Compilation and output -- ---------------------------- $ echo "Static model" $ gcc -c spark_pack.adb $ echo "Relaxed static model" $ gcc -c spark_pack.adb -gnatJ $ echo "Dynamic model" $ gcc -c spark_pack.adb -gnatE $ echo "Relaxed dynamic model" $ gcc -c spark_pack.adb -gnatE -gnatJ Static model Relaxed static model spark_pack.ads:7:04: warning: SPARK elaboration checks require static elaboration model spark_pack.ads:7:04: warning: relaxed elaboration model is in effect Dynamic model spark_pack.ads:4:09: warning: SPARK elaboration checks require static elaboration model spark_pack.ads:4:09: warning: dynamic elaboration model is in effect Relaxed dynamic model spark_pack.ads:4:09: warning: SPARK elaboration checks require static elaboration model spark_pack.ads:4:09: warning: dynamic elaboration model is in effect Tested on x86_64-pc-linux-gnu, committed on trunk 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.