* [Ada] Missing detection of elaboration dependency
@ 2015-11-12 11:35 Arnaud Charlet
0 siblings, 0 replies; only message in thread
From: Arnaud Charlet @ 2015-11-12 11:35 UTC (permalink / raw)
To: gcc-patches; +Cc: Hristian Kirtchev
[-- Attachment #1: Type: text/plain, Size: 1998 bytes --]
This patch modifies the elaboration circuitry to detect an issue in SPARK
where an object in package P of a private type in package T subject to
pragma Default_Initial_Condition is default initialized and package P
lacks Elaborate_All (T).
------------
-- Source --
------------
-- pack.ads
package Pack with SPARK_Mode is
type Elab_Typ is private
with Default_Initial_Condition => Get_Val (Elab_Typ) = Expect_Val;
type False_Typ is private
with Default_Initial_Condition => False;
type True_Typ is private
with Default_Initial_Condition => True;
function Expect_Val return Integer;
function Get_Val (Obj : Elab_Typ) return Integer;
private
type Elab_Typ is record
Comp : Integer;
end record;
type False_Typ is null record;
type True_Typ is null record;
end Pack;
-- pack.adb
package body Pack with SPARK_Mode is
function Expect_Val return Integer is
begin
return 1234;
end Expect_Val;
function Get_Val (Obj : Elab_Typ) return Integer is
begin
return Obj.Comp;
end Get_Val;
end Pack;
-- main_pack.ads
with Pack; use Pack;
package Main_Pack with SPARK_Mode is
Obj_1 : Elab_Typ;
Obj_2 : False_Typ;
Obj_3 : True_Typ;
end Main_Pack;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c -gnata main_pack.ads
main_pack.ads:4:04: call to Default_Initial_Condition during elaboration in
SPARK
main_pack.ads:4:04: Elaborate_All pragma required for "Pack"
Tested on x86_64-pc-linux-gnu, committed on trunk
2015-11-12 Hristian Kirtchev <kirtchev@adacore.com>
* sem_elab.adb (Check_A_Call): Add new variable
Is_DIC_Proc. Report elaboration issue in SPARK concerning calls
to source subprograms or nontrivial Default_Initial_Condition
procedures. Add specialized error message to avoid outputting
the internal name of the Default_Initial_Condition procedure.
* sem_util.ads, sem_util.adb
(Is_Non_Trivial_Default_Init_Cond_Procedure): New routine.
[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 5116 bytes --]
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 230235)
+++ sem_util.adb (working copy)
@@ -12362,12 +12362,50 @@
end if;
end Is_Local_Variable_Reference;
+ ------------------------------------------------
+ -- Is_Non_Trivial_Default_Init_Cond_Procedure --
+ ------------------------------------------------
+
+ function Is_Non_Trivial_Default_Init_Cond_Procedure
+ (Id : Entity_Id) return Boolean
+ is
+ Body_Decl : Node_Id;
+ Stmt : Node_Id;
+
+ begin
+ if Ekind (Id) = E_Procedure
+ and then Is_Default_Init_Cond_Procedure (Id)
+ then
+ Body_Decl :=
+ Unit_Declaration_Node
+ (Corresponding_Body (Unit_Declaration_Node (Id)));
+
+ -- The body of the Default_Initial_Condition procedure must contain
+ -- at least one statement, otherwise the generation of the subprogram
+ -- body failed.
+
+ pragma Assert (Present (Handled_Statement_Sequence (Body_Decl)));
+
+ -- To qualify as non-trivial, the first statement of the procedure
+ -- must be a check in the form of an if statement. If the original
+ -- Default_Initial_Condition expression was folded, then the first
+ -- statement is not a check.
+
+ Stmt := First (Statements (Handled_Statement_Sequence (Body_Decl)));
+
+ return
+ Nkind (Stmt) = N_If_Statement
+ and then Nkind (Original_Node (Stmt)) = N_Pragma;
+ end if;
+
+ return False;
+ end Is_Non_Trivial_Default_Init_Cond_Procedure;
+
-------------------------
-- Is_Object_Reference --
-------------------------
function Is_Object_Reference (N : Node_Id) return Boolean is
-
function Is_Internally_Generated_Renaming (N : Node_Id) return Boolean;
-- Determine whether N is the name of an internally-generated renaming
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 230223)
+++ sem_util.ads (working copy)
@@ -1433,6 +1433,12 @@
-- parameter of the current enclosing subprogram.
-- Why are OUT parameters not considered here ???
+ function Is_Non_Trivial_Default_Init_Cond_Procedure
+ (Id : Entity_Id) return Boolean;
+ -- Determine whether entity Id denotes the procedure which verifies the
+ -- assertion expression of pragma Default_Initial_Condition and if it does,
+ -- the encapsulated expression is non-trivial.
+
function Is_Object_Reference (N : Node_Id) return Boolean;
-- Determines if the tree referenced by N represents an object. Both
-- variable and constant objects return True (compare Is_Variable).
Index: sem_elab.adb
===================================================================
--- sem_elab.adb (revision 230223)
+++ sem_elab.adb (working copy)
@@ -597,6 +597,11 @@
-- non-visible unit. This is the scope that is to be investigated to
-- see whether an elaboration check is required.
+ Is_DIC_Proc : Boolean := False;
+ -- Flag set when the call denotes the Default_Initial_Condition
+ -- procedure of a private type which wraps a non-trivila assertion
+ -- expression.
+
Issue_In_SPARK : Boolean;
-- Flag set when a source entity is called during elaboration in SPARK
@@ -966,8 +971,17 @@
return;
end if;
- Issue_In_SPARK := SPARK_Mode = On and Comes_From_Source (Ent);
+ Is_DIC_Proc := Is_Non_Trivial_Default_Init_Cond_Procedure (Ent);
+ -- Elaboration issues in SPARK are reported only for source constructs
+ -- and for non-trivial Default_Initial_Condition procedures. The latter
+ -- must be checked because the default initialization of an object of a
+ -- private type triggers the evaluation of the Default_Initial_Condition
+ -- expression which in turn may have side effects.
+
+ Issue_In_SPARK :=
+ SPARK_Mode = On and (Comes_From_Source (Ent) or Is_DIC_Proc);
+
-- Now check if an Elaborate_All (or dynamic check) is needed
if not Suppress_Elaboration_Warnings (Ent)
@@ -1016,8 +1030,21 @@
Ent);
elsif Issue_In_SPARK then
- Error_Msg_NE ("call to & during elaboration in SPARK", N, Ent);
+ -- Emit a specialized error message when the elaboration of an
+ -- object of a private type evaluates the expression of pragma
+ -- Default_Initial_Condition. This prevents the internal name
+ -- of the procedure from appearing in the error message.
+
+ if Is_DIC_Proc then
+ Error_Msg_N
+ ("call to Default_Initial_Condition during elaboration in "
+ & "SPARK", N);
+ else
+ Error_Msg_NE
+ ("call to & during elaboration in SPARK", N, Ent);
+ end if;
+
else
Elab_Warning
("call to & may raise Program_Error?l?",
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2015-11-12 11:35 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2015-11-12 11:35 [Ada] Missing detection of elaboration dependency Arnaud Charlet
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).