diff mbox

[Ada] Reject the use of volatiles in assertion expressions

Message ID 20140521132144.GA15406@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet May 21, 2014, 1:21 p.m. UTC 
This patch corrects the trigger which determines the proper context of a
volatile object with enabled property Async_Writers or Effective_Reads.

------------
-- Source --
------------

--  assert_exprs.ads

package Assert_Exprs with SPARK_Mode is
   type T is new Integer with Volatile;

   procedure Error (Input : T; Output : out T)
     with Pre  => Input > 1,
          Post => Output = Input * 2;
end Assert_Exprs;

--  assert_exprs.adb

package body Assert_Exprs with SPARK_Mode is
   procedure Error (Input : T; Output : out T) is
   begin
      Output := Input * 2;
   end Error;
end Assert_Exprs;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c -gnata assert_exprs.adb
assert_exprs.adb:4:17: volatile object cannot appear in this context (SPARK RM
  7.1.3(13))
assert_exprs.ads:5:19: volatile object cannot appear in this context (SPARK RM
  7.1.3(13))
assert_exprs.ads:6:19: volatile object cannot appear in this context (SPARK RM
  7.1.3(13))
assert_exprs.ads:6:28: volatile object cannot appear in this context (SPARK RM
  7.1.3(13))

Tested on x86_64-pc-linux-gnu, committed on trunk

2014-05-21  Hristian Kirtchev  <kirtchev@adacore.com>

	* freeze.adb (Freeze_Record_Type): Update the use of
	Is_SPARK_Volatile.
	* sem_ch3.adb (Analyze_Object_Contract): Update the use of
	Is_SPARK_Volatile.
	(Process_Discriminants): Update the use of Is_SPARK_Volatile.
	* sem_ch5.adb (Analyze_Iterator_Specification): Update the use
	of Is_SPARK_Volatile.
	(Analyze_Loop_Parameter_Specification):
	Update the use of Is_SPARK_Volatile.
	* sem_ch6.adb (Process_Formals): Catch an illegal use of an IN
	formal parameter when its type is volatile.
	* sem_prag.adb (Analyze_Global_Item): Update the use of
	Is_SPARK_Volatile.
	* sem_res.adb (Resolve_Entity_Name): Correct the guard which
	determines whether an entity is a volatile source SPARK object.
	* sem_util.adb (Has_Enabled_Property): Accout for external
	properties being set on objects other than abstract states
	and variables. An example would be a formal parameter.
	(Is_SPARK_Volatile): New routine.
	(Is_SPARK_Volatile_Object):
	Remove the entity-specific tests. Call routine Is_SPARK_Volatile
	when checking entities and/or types.
	* sem_util.ads (Is_SPARK_Volatile): New routine.
diff mbox

Patch

Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 210705)
+++ sem_ch3.adb	(working copy)
@@ -2988,7 +2988,7 @@ 
          --  actuals in instantiations (SPARK RM 7.1.3(6)).
 
          if SPARK_Mode = On
-           and then Is_SPARK_Volatile_Object (Obj_Id)
+           and then Is_SPARK_Volatile (Obj_Id)
            and then No (Corresponding_Generic_Association (Parent (Obj_Id)))
          then
             Error_Msg_N ("constant cannot be volatile", Obj_Id);
@@ -3000,7 +3000,7 @@ 
          --  they are not standard Ada legality rules.
 
          if SPARK_Mode = On then
-            if Is_SPARK_Volatile_Object (Obj_Id) then
+            if Is_SPARK_Volatile (Obj_Id) then
 
                --  The declaration of a volatile object must appear at the
                --  library level (SPARK RM 7.1.3(7), C.6(6)).
@@ -3030,7 +3030,7 @@ 
                --  A non-volatile object cannot have volatile components
                --  (SPARK RM 7.1.3(7)).
 
-               if not Is_SPARK_Volatile_Object (Obj_Id)
+               if not Is_SPARK_Volatile (Obj_Id)
                  and then Has_Volatile_Component (Obj_Typ)
                then
                   Error_Msg_N
@@ -18051,7 +18051,7 @@ 
          --  (SPARK RM 7.1.3(6)).
 
          if SPARK_Mode = On
-           and then Is_SPARK_Volatile_Object (Defining_Identifier (Discr))
+           and then Is_SPARK_Volatile (Defining_Identifier (Discr))
          then
             Error_Msg_N ("discriminant cannot be volatile", Discr);
          end if;
Index: sem_ch5.adb
===================================================================
--- sem_ch5.adb	(revision 210707)
+++ sem_ch5.adb	(working copy)
@@ -1986,7 +1986,7 @@ 
 
       if SPARK_Mode = On
         and then not Of_Present (N)
-        and then Is_SPARK_Volatile_Object (Ent)
+        and then Is_SPARK_Volatile (Ent)
       then
          Error_Msg_N ("loop parameter cannot be volatile", Ent);
       end if;
@@ -2706,7 +2706,7 @@ 
       --  when SPARK_Mode is on as it is not a standard Ada legality check
       --  (SPARK RM 7.1.3(6)).
 
-      if SPARK_Mode = On and then Is_SPARK_Volatile_Object (Id) then
+      if SPARK_Mode = On and then Is_SPARK_Volatile (Id) then
          Error_Msg_N ("loop parameter cannot be volatile", Id);
       end if;
    end Analyze_Loop_Parameter_Specification;
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 210702)
+++ sem_prag.adb	(working copy)
@@ -2038,9 +2038,8 @@ 
                --  SPARK_Mode is on as they are not standard Ada legality
                --  rules.
 
-               elsif SPARK_Mode = On
-                 and then Is_SPARK_Volatile_Object (Item_Id)
-               then
+               elsif SPARK_Mode = On and then Is_SPARK_Volatile (Item_Id) then
+
                   --  A volatile object cannot appear as a global item of a
                   --  function (SPARK RM 7.1.3(9)).
 
Index: freeze.adb
===================================================================
--- freeze.adb	(revision 210697)
+++ freeze.adb	(working copy)
@@ -3318,7 +3318,7 @@ 
          --  they are not standard Ada legality rules.
 
          if SPARK_Mode = On then
-            if Is_SPARK_Volatile_Object (Rec) then
+            if Is_SPARK_Volatile (Rec) then
 
                --  A discriminated type cannot be volatile (SPARK RM C.6(4))
 
@@ -3340,7 +3340,7 @@ 
                Comp := First_Component (Rec);
                while Present (Comp) loop
                   if Comes_From_Source (Comp)
-                    and then Is_SPARK_Volatile_Object (Comp)
+                    and then Is_SPARK_Volatile (Comp)
                   then
                      Error_Msg_Name_1 := Chars (Rec);
                      Error_Msg_N
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 210701)
+++ sem_util.adb	(working copy)
@@ -7466,7 +7466,7 @@ 
       begin
          --  A non-volatile object can never possess external properties
 
-         if not Is_SPARK_Volatile_Object (Item_Id) then
+         if not Is_SPARK_Volatile (Item_Id) then
             return False;
 
          --  External properties related to variables come in two flavors -
@@ -7514,11 +7514,19 @@ 
    --  Start of processing for Has_Enabled_Property
 
    begin
+      --  Abstract states and variables have a flexible scheme of specifying
+      --  external properties.
+
       if Ekind (Item_Id) = E_Abstract_State then
          return State_Has_Enabled_Property;
 
-      else pragma Assert (Ekind (Item_Id) = E_Variable);
+      elsif Ekind (Item_Id) = E_Variable then
          return Variable_Has_Enabled_Property;
+
+      --  Otherwise a property is enabled when the related object is volatile
+
+      else
+         return Is_SPARK_Volatile (Item_Id);
       end if;
    end Has_Enabled_Property;
 
@@ -11413,22 +11421,26 @@ 
       end if;
    end Is_SPARK_Object_Reference;
 
+   -----------------------
+   -- Is_SPARK_Volatile --
+   -----------------------
+
+   function Is_SPARK_Volatile (Id : Entity_Id) return Boolean is
+   begin
+      return Is_Volatile (Id) or else Is_Volatile (Etype (Id));
+   end Is_SPARK_Volatile;
+
    ------------------------------
    -- Is_SPARK_Volatile_Object --
    ------------------------------
 
    function Is_SPARK_Volatile_Object (N : Node_Id) return Boolean is
    begin
-      if Nkind (N) = N_Defining_Identifier then
-         return Is_Volatile (N) or else Is_Volatile (Etype (N));
+      if Is_Entity_Name (N) then
+         return Is_SPARK_Volatile (Entity (N));
 
-      elsif Is_Entity_Name (N) then
-         return
-           Is_SPARK_Volatile_Object (Entity (N))
-             or else Is_Volatile (Etype (N));
-
       elsif Nkind (N) = N_Expanded_Name then
-         return Is_SPARK_Volatile_Object (Entity (N));
+         return Is_SPARK_Volatile (Entity (N));
 
       elsif Nkind (N) = N_Indexed_Component then
          return Is_SPARK_Volatile_Object (Prefix (N));
Index: sem_util.ads
===================================================================
--- sem_util.ads	(revision 210697)
+++ sem_util.ads	(working copy)
@@ -1302,10 +1302,15 @@ 
    function Is_SPARK_Object_Reference (N : Node_Id) return Boolean;
    --  Determines if the tree referenced by N represents an object in SPARK
 
+   function Is_SPARK_Volatile (Id : Entity_Id) return Boolean;
+   --  This routine is similar to predicate Is_Volatile, but it takes SPARK
+   --  semantics into account. In SPARK volatile components to not render a
+   --  type volatile.
+
    function Is_SPARK_Volatile_Object (N : Node_Id) return Boolean;
    --  Determine whether an arbitrary node denotes a volatile object reference
    --  according to the semantics of SPARK. To qualify as volatile, an object
-   --  must be subject to aspect/pragma Volatile or Atomic or have a [sub]type
+   --  must be subject to aspect/pragma Volatile or Atomic, or have a [sub]type
    --  subject to the same attributes. Note that volatile components do not
    --  render an object volatile.
 
Index: sem_res.adb
===================================================================
--- sem_res.adb	(revision 210697)
+++ sem_res.adb	(working copy)
@@ -6579,8 +6579,9 @@ 
       --  standard Ada legality rules.
 
       if SPARK_Mode = On
-        and then Ekind_In (E, E_Abstract_State, E_Variable)
-        and then Is_SPARK_Volatile_Object (E)
+        and then Is_Object (E)
+        and then Is_SPARK_Volatile (E)
+        and then Comes_From_Source (E)
         and then
           (Async_Writers_Enabled (E)
              or else Effective_Reads_Enabled (E))
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 210705)
+++ sem_ch6.adb	(working copy)
@@ -11511,23 +11511,35 @@ 
          --  The following checks are relevant when SPARK_Mode is on as these
          --  are not standard Ada legality rules.
 
-         if SPARK_Mode = On
-           and then Ekind_In (Scope (Formal), E_Function, E_Generic_Function)
-         then
-            --  A function cannot have a parameter of mode IN OUT or OUT
-            --  (SPARK RM 6.1).
+         if SPARK_Mode = On then
+            if Ekind_In (Scope (Formal), E_Function, E_Generic_Function) then
 
-            if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then
-               Error_Msg_N
-                 ("function cannot have parameter of mode `OUT` or `IN OUT`",
-                  Formal);
+               --  A function cannot have a parameter of mode IN OUT or OUT
+               --  (SPARK RM 6.1).
 
-            --  A function cannot have a volatile formal parameter
-            --  (SPARK RM 7.1.3(10)).
+               if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then
+                  Error_Msg_N
+                    ("function cannot have parameter of mode `OUT` or "
+                     & "`IN OUT`", Formal);
 
-            elsif Is_SPARK_Volatile_Object (Formal) then
+               --  A function cannot have a volatile formal parameter
+               --  (SPARK RM 7.1.3(10)).
+
+               elsif Is_SPARK_Volatile (Formal) then
+                  Error_Msg_N
+                    ("function cannot have a volatile formal parameter",
+                     Formal);
+               end if;
+
+            --  A procedure cannot have a formal parameter of mode IN because
+            --  it behaves as a constant (SPARK RM 7.1.3(6)).
+
+            elsif Ekind (Scope (Formal)) = E_Procedure
+              and then Ekind (Formal) = E_In_Parameter
+              and then Is_SPARK_Volatile (Formal)
+            then
                Error_Msg_N
-                 ("function cannot have a volatile formal parameter", Formal);
+                 ("formal parameter of mode `IN` cannot be volatile", Formal);
             end if;
          end if;