[Ada] Rewrite check for SPARK RM 7.1.3(10)

Message ID 20171009200030.GA44133@adacore.com
State New
Headers show
Series
  • [Ada] Rewrite check for SPARK RM 7.1.3(10)
Related show

Commit Message

Pierre-Marie de Rodat Oct. 9, 2017, 8 p.m.
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.

Patch

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;