* [Ada] Warn on weal elaboration model for SPARK
@ 2017-12-05 12:24 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2017-12-05 12:24 UTC (permalink / raw)
To: gcc-patches; +Cc: Hristian Kirtchev
[-- Attachment #1: Type: text/plain, Size: 2154 bytes --]
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.
[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 5055 bytes --]
Index: sem_elab.adb
===================================================================
--- sem_elab.adb (revision 255412)
+++ sem_elab.adb (working copy)
@@ -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.
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2017-12-05 12:24 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2017-12-05 12:24 [Ada] Warn on weal elaboration model for SPARK Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).