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 <troja...@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.
Index: sem_res.adb =================================================================== --- sem_res.adb (revision 253559) +++ sem_res.adb (working copy) @@ -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;