Commit ed37f25a by Arnaud Charlet

[multiple changes]

2015-10-23  Gary Dismukes  <dismukes@adacore.com>

	* bindgen.adb, restrict.adb: Minor spelling/grammar fixes.

2015-10-23  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_res.adb (Resolve_Entity_Name): Code cleanup. Check for possible
	elaboration issues in SPARK when the name denotes a source variable.

From-SVN: r229228
parent 6e840989
2015-10-23 Gary Dismukes <dismukes@adacore.com>
* bindgen.adb, restrict.adb: Minor spelling/grammar fixes.
2015-10-23 Hristian Kirtchev <kirtchev@adacore.com>
* sem_res.adb (Resolve_Entity_Name): Code cleanup. Check for possible
elaboration issues in SPARK when the name denotes a source variable.
2015-10-23 Hristian Kirtchev <kirtchev@adacore.com> 2015-10-23 Hristian Kirtchev <kirtchev@adacore.com>
* exp_ch7.adb (Process_Transient_Objects): Reimplement to properly * exp_ch7.adb (Process_Transient_Objects): Reimplement to properly
......
...@@ -2810,8 +2810,8 @@ package body Bindgen is ...@@ -2810,8 +2810,8 @@ package body Bindgen is
procedure Check_Package (Var : in out Boolean; Name : String); procedure Check_Package (Var : in out Boolean; Name : String);
-- Set Var to true iff the current identifier in Namet is Name. Do -- Set Var to true iff the current identifier in Namet is Name. Do
-- nothing if it doesn't match. This procedure is just an helper to -- nothing if it doesn't match. This procedure is just a helper to
-- avoid to explicitely deal with length. -- avoid explicitly dealing with length.
------------------- -------------------
-- Check_Package -- -- Check_Package --
......
...@@ -503,7 +503,7 @@ package body Restrict is ...@@ -503,7 +503,7 @@ package body Restrict is
-- so that we have consistency between each compilation. -- so that we have consistency between each compilation.
-- In GNATprove mode restrictions are checked, except for -- In GNATprove mode restrictions are checked, except for
-- No_Initialize_Scalars, which is implicitely set in gnat1drv.adb. -- No_Initialize_Scalars, which is implicitly set in gnat1drv.adb.
-- Just checking, SPARK does not allow restrictions to be set ??? -- Just checking, SPARK does not allow restrictions to be set ???
......
...@@ -7179,44 +7179,40 @@ package body Sem_Res is ...@@ -7179,44 +7179,40 @@ package body Sem_Res is
Par := Parent (Par); Par := Parent (Par);
end if; end if;
-- The following checks are only relevant when SPARK_Mode is on as they if Comes_From_Source (N) then
-- are not standard Ada legality rules. An effectively volatile object
-- subject to enabled properties Async_Writers or Effective_Reads must
-- appear in a specific context.
if SPARK_Mode = On
and then Is_Object (E)
and then Is_Effectively_Volatile (E)
and then (Async_Writers_Enabled (E)
or else Effective_Reads_Enabled (E))
and then Comes_From_Source (N)
then
-- The effectively volatile objects appears in a "non-interfering
-- context" as defined in SPARK RM 7.1.3(12).
if Is_OK_Volatile_Context (Par, N) then -- The following checks are only relevant when SPARK_Mode is on as
null; -- they are not standard Ada legality rules.
-- Otherwise the context causes a side effect with respect to the if SPARK_Mode = On then
-- effectively volatile object.
else -- An effectively volatile object subject to enabled properties
SPARK_Msg_N -- Async_Writers or Effective_Reads must appear in non-interfering
("volatile object cannot appear in this context " -- context (SPARK RM 7.1.3(12)).
& "(SPARK RM 7.1.3(12))", N);
end if;
end if;
-- A Ghost entity must appear in a specific context if Is_Object (E)
and then Is_Effectively_Volatile (E)
and then (Async_Writers_Enabled (E)
or else Effective_Reads_Enabled (E))
and then not Is_OK_Volatile_Context (Par, N)
then
SPARK_Msg_N
("volatile object cannot appear in this context "
& "(SPARK RM 7.1.3(12))", N);
end if;
if Is_Ghost_Entity (E) and then Comes_From_Source (N) then -- Check possible elaboration issues with respect to variables
Check_Ghost_Context (E, N);
end if; if Ekind (E) = E_Variable then
Check_Elab_Call (N);
end if;
end if;
-- In SPARK mode, need to check possible elaboration issues -- A Ghost entity must appear in a specific context
if SPARK_Mode = On and then Ekind (E) = E_Variable then if Is_Ghost_Entity (E) then
Check_Elab_Call (N); Check_Ghost_Context (E, N);
end if;
end if; end if;
end Resolve_Entity_Name; end Resolve_Entity_Name;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment