[Ada] Illegal use of SPARK volatile object not detected
Arnaud Charlet
charlet@adacore.com
Tue Feb 25 14:56:00 GMT 2014
This patch simplifies the entity resolution machinery which detects an illegaly
used SPARK volatile object with enabled external properties Async_Writers or
Effective_Reads. The mechanism no longer traverses the parent chain as this is
not needed.
------------
-- Source --
------------
-- volatile_use.ads
package Volatile_Use with SPARK_Mode => On is
V1 : Integer
with Volatile,
Async_Writers => True;
procedure Test_Eval_Order_OK (X : out Boolean)
with Global => (Input => V1),
Depends => (X => V1);
procedure Test_Eval_Order_Bad1 (X : out Boolean)
with Global => (Input => V1),
Depends => (X => V1);
procedure Test_Eval_Order_Bad2 (X : out Boolean)
with Global => (Input => V1),
Depends => (X => V1);
end Volatile_Use;
-- volatile_use.adb
package body Volatile_Use with SPARK_Mode => On is
procedure Test_Eval_Order_OK (X : out Boolean) is
T1 : Integer;
T2 : Integer;
begin
T1 := V1;
T2 := V1;
X := (T1 <= T2);
end Test_Eval_Order_OK;
procedure Test_Eval_Order_Bad1 (X : out Boolean) is
T1 : Integer;
begin
T1 := V1;
X := (T1 <= V1);
end Test_Eval_Order_Bad1;
procedure Test_Eval_Order_Bad2 (X : out Boolean) is
begin
X := (V1 <= V1);
end Test_Eval_Order_Bad2;
end Volatile_Use;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c volatile_use.adb
volatile_use.adb:15:19: volatile object cannot appear in this context (SPARK RM
7.1.3(13))
volatile_use.adb:20:13: volatile object cannot appear in this context (SPARK RM
7.1.3(13))
volatile_use.adb:20:19: volatile object cannot appear in this context (SPARK RM
7.1.3(13))
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-02-25 Hristian Kirtchev <kirtchev@adacore.com>
* sem_res.adb (Appears_In_Check): New routine.
(Resolve_Entity_Name): Remove local variables Prev and
Usage_OK. Par is now a constant. Remove the parent chain traversal
as the placement of a volatile object with enabled property
Async_Writers and/or Effective_Reads must appear immediately
within a legal construct.
-------------- next part --------------
Index: sem_res.adb
===================================================================
--- sem_res.adb (revision 208076)
+++ sem_res.adb (working copy)
@@ -6434,13 +6434,43 @@
-- Used to resolve identifiers and expanded names
procedure Resolve_Entity_Name (N : Node_Id; Typ : Entity_Id) is
- E : constant Entity_Id := Entity (N);
- Par : Node_Id;
- Prev : Node_Id;
+ function Appears_In_Check (Nod : Node_Id) return Boolean;
+ -- Denote whether an arbitrary node Nod appears in a check node
- Usage_OK : Boolean := False;
- -- Flag set when the use of a volatile object agrees with its context
+ ----------------------
+ -- Appears_In_Check --
+ ----------------------
+ function Appears_In_Check (Nod : Node_Id) return Boolean is
+ Par : Node_Id;
+
+ begin
+ -- Climb the parent chain looking for a check node
+
+ Par := Nod;
+ while Present (Par) loop
+ if Nkind (Par) in N_Raise_xxx_Error then
+ return True;
+
+ -- Prevent the search from going too far
+
+ elsif Is_Body_Or_Package_Declaration (Par) then
+ exit;
+ end if;
+
+ Par := Parent (Par);
+ end loop;
+
+ return False;
+ end Appears_In_Check;
+
+ -- Local variables
+
+ E : constant Entity_Id := Entity (N);
+ Par : constant Node_Id := Parent (N);
+
+ -- Start of processing for Resolve_Entity_Name
+
begin
-- If garbage from errors, set to Any_Type and return
@@ -6555,62 +6585,43 @@
(Async_Writers_Enabled (E)
or else Effective_Reads_Enabled (E))
then
- Par := Parent (N);
- Prev := N;
- while Present (Par) loop
+ -- The volatile object can appear on either side of an assignment
- -- The volatile object can appear on either side of an assignment
+ if Nkind (Par) = N_Assignment_Statement then
+ null;
- if Nkind (Par) = N_Assignment_Statement then
- Usage_OK := True;
- exit;
+ -- The volatile object is part of the initialization expression of
+ -- another object. Ensure that the climb of the parent chain came
+ -- from the expression side and not from the name side.
- -- The volatile object is part of the initialization expression of
- -- another object. Ensure that the climb of the parent chain came
- -- from the expression side and not from the name side.
+ elsif Nkind (Par) = N_Object_Declaration
+ and then Present (Expression (Par))
+ and then N = Expression (Par)
+ then
+ null;
- elsif Nkind (Par) = N_Object_Declaration
- and then Present (Expression (Par))
- and then Prev = Expression (Par)
- then
- Usage_OK := True;
- exit;
+ -- The volatile object appears as an actual parameter in a call to an
+ -- instance of Unchecked_Conversion whose result is renamed.
- -- The volatile object appears as an actual parameter in a call to
- -- an instance of Unchecked_Conversion whose result is renamed.
+ elsif Nkind (Par) = N_Function_Call
+ and then Is_Unchecked_Conversion_Instance (Entity (Name (Par)))
+ and then Nkind (Parent (Par)) = N_Object_Renaming_Declaration
+ then
+ null;
- elsif Nkind (Par) = N_Function_Call
- and then Is_Unchecked_Conversion_Instance (Entity (Name (Par)))
- and then Nkind (Parent (Par)) = N_Object_Renaming_Declaration
- then
- Usage_OK := True;
- exit;
+ -- Assume that references to volatile objects that appear as actual
+ -- parameters in a procedure call are always legal. The full legality
+ -- check is done when the actuals are resolved.
- -- Assume that references to volatile objects that appear as
- -- actual parameters in a procedure call are always legal. The
- -- full legality check is done when the actuals are resolved.
+ elsif Nkind (Par) = N_Procedure_Call_Statement then
+ null;
- elsif Nkind (Par) = N_Procedure_Call_Statement then
- Usage_OK := True;
- exit;
+ -- Allow references to volatile objects in various checks
- -- Allow references to volatile objects in various checks
+ elsif Appears_In_Check (Par) then
+ null;
- elsif Nkind (Par) in N_Raise_xxx_Error then
- Usage_OK := True;
- exit;
-
- -- Prevent the search from going too far
-
- elsif Is_Body_Or_Package_Declaration (Par) then
- exit;
- end if;
-
- Prev := Par;
- Par := Parent (Par);
- end loop;
-
- if not Usage_OK then
+ else
Error_Msg_N
("volatile object cannot appear in this context "
& "(SPARK RM 7.1.3(13))", N);
More information about the Gcc-patches
mailing list