===================================================================
@@ -3178,14 +3178,6 @@
-- an instance of the default expression. The insertion is always
-- a named association.
- procedure Property_Error
- (Var : Node_Id;
- Var_Id : Entity_Id;
- Prop_Nam : Name_Id);
- -- Emit an error concerning variable Var with entity Var_Id that has
- -- enabled property Prop_Nam when it acts as an actual parameter in a
- -- call and the corresponding formal parameter is of mode IN.
-
function Same_Ancestor (T1, T2 : Entity_Id) return Boolean;
-- Check whether T1 and T2, or their full views, are derived from a
-- common type. Used to enforce the restrictions on array conversions
@@ -3634,23 +3626,6 @@
Prev := Actval;
end Insert_Default;
- --------------------
- -- Property_Error --
- --------------------
-
- procedure Property_Error
- (Var : Node_Id;
- Var_Id : Entity_Id;
- Prop_Nam : Name_Id)
- is
- begin
- Error_Msg_Name_1 := Prop_Nam;
- Error_Msg_NE
- ("external variable & with enabled property % cannot appear as "
- & "actual in procedure call (SPARK RM 7.1.3(10))", Var, Var_Id);
- Error_Msg_N ("\\corresponding formal parameter has mode In", Var);
- end Property_Error;
-
-------------------
-- Same_Ancestor --
-------------------
@@ -4659,26 +4634,28 @@
Flag_Effectively_Volatile_Objects (A);
end if;
- -- Detect an external variable with an enabled property that
- -- does not match the mode of the corresponding formal in a
- -- procedure call. Functions are not considered because they
- -- cannot have effectively volatile formal parameters in the
- -- first place.
+ -- An effectively volatile variable cannot act as an actual
+ -- parameter in a procedure call when the variable has enabled
+ -- property Effective_Reads and the corresponding formal is of
+ -- mode IN (SPARK RM 7.1.3(10)).
if Ekind (Nam) = E_Procedure
and then Ekind (F) = E_In_Parameter
and then Is_Entity_Name (A)
- and then Present (Entity (A))
- and then Ekind (Entity (A)) = E_Variable
then
A_Id := Entity (A);
- if Async_Readers_Enabled (A_Id) then
- Property_Error (A, A_Id, Name_Async_Readers);
- elsif Effective_Reads_Enabled (A_Id) then
- Property_Error (A, A_Id, Name_Effective_Reads);
- elsif Effective_Writes_Enabled (A_Id) then
- Property_Error (A, A_Id, Name_Effective_Writes);
+ if Ekind (A_Id) = E_Variable
+ and then Is_Effectively_Volatile (Etype (A_Id))
+ and then Effective_Reads_Enabled (A_Id)
+ then
+ Error_Msg_NE
+ ("effectively volatile variable & cannot appear as "
+ & "actual in procedure call", A, A_Id);
+
+ Error_Msg_Name_1 := Name_Effective_Reads;
+ Error_Msg_N ("\\variable has enabled property %", A);
+ Error_Msg_N ("\\corresponding formal has mode IN", A);
end if;
end if;
end if;
The evolution of SPARK RM 7.1.3(10) rule was not followed by code that implements it. The current wording is: "If a procedure has an in mode parameter of an effectively volatile type, then the Effective_Reads aspect of any corresponding actual parameter shall be False." and the current code checks exactly that. ------------ -- Source -- ------------ -- ineffective_actual.ads with System; package Ineffective_Actual with SPARK_Mode is type VT is record Int : Integer; end record with Volatile; The_Volatile_Data : VT with Volatile, Async_Readers => True, Async_Writers => True, Effective_Reads => False, Effective_Writes => False, Address => System'To_Address (16#1234_5678#); procedure Harmless_Reader (Data : in VT); procedure Do_Something; end Ineffective_Actual; -- ineffective_actual.adb package body Ineffective_Actual with SPARK_Mode is procedure Harmless_Reader (Data : in VT) with SPARK_Mode => Off is I : Integer; begin I := Data.Int; end Harmless_Reader; procedure Do_Something is begin Harmless_Reader (The_Volatile_Data); end Do_Something; end Ineffective_Actual; ---------------------------- -- Compilation and output -- ---------------------------- & gcc -c ineffective_actual.adb & gcc -c -gnatd.F ineffective_actual.adb Tested on x86_64-pc-linux-gnu, committed on trunk 2017-10-09 Piotr Trojanek <trojanek@adacore.com> * sem_res.adb (Property_Error): Remove. (Resolve_Actuals): check for SPARK RM 7.1.3(10) rewritten to match the current wording of the rule.