[Ada] Accept a constituent in a null dependency clause

[Ada] Accept a constituent in a null dependency clause

[Arnaud Charlet]

[-- Attachment #1: Type: text/plain, Size: 1678 bytes --]

This patch implements the following SPARK RM rule from 7.2.5 (3g):

   at least one of its constituents shall be denoted in the input_list of a
   null_dependency_clause; or

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

--  null_dependency.ads

package Null_Dependency
  with Abstract_State => (Input_State, Output_State)
is
   procedure OK_1
     with Global  => (Input => Input_State),
          Depends => (null  => Input_State);

   procedure OK_2
     with Global  => (Input  => Input_State,
                      Output => Output_State),
          Depends => (Output_State => Input_State);
end Null_Dependency;

--  null_dependency.adb

package body Null_Dependency
  with Refined_State => (Input_State  => (C1, C2),
                         Output_State => (C3, C4))
is
   C1, C2, C3, C4 : Integer := 0;

   procedure OK_1
     with Refined_Global  => (Input => C1),
          Refined_Depends => (null  => C1)
   is begin null; end OK_1;

   procedure OK_2
     with Refined_Global  => (Input  => (C1, C2),
                              Output => (C3, C4)),
          Refined_Depends => ((C3, C4) => C1,
                               null    => C2)
   is begin null; end OK_2;
end Null_Dependency;

-----------------
-- Compilation --
-----------------

$ gcc -c null_dependency.adb

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

2014-02-19  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Check_Dependency_Clause): Account
	for the case where a state with a non-null refinement matches a
	null output list. Comment reformatting.
	(Inputs_Match): Copy a solitary input to avoid an assertion failure
	when trying to match the same input in multiple clauses.


[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 3816 bytes --]

Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 207879)
+++ sem_prag.adb	(working copy)
@@ -21434,16 +21434,38 @@
                   elsif Has_Non_Null_Refinement (Dep_Id) then
                      Has_Refined_State := True;
 
-                     if Is_Entity_Name (Ref_Output) then
+                     --  Account for the case where a state with a non-null
+                     --  refinement matches a null output list:
+
+                     --    Refined_State   => (State_1 => (C1, C2),
+                     --                        State_2 => (C3, C4))
+                     --    Depends         => (State_1 => State_2)
+                     --    Refined_Depends => (null    => C3)
+
+                     if Nkind (Ref_Output) = N_Null
+                       and then Inputs_Match
+                                  (Dep_Clause  => Dep_Clause,
+                                   Ref_Clause  => Ref_Clause,
+                                   Post_Errors => False)
+                     then
+                        Has_Constituent := True;
+
+                        --  Note that the search continues after the clause is
+                        --  removed from the pool of candidates because it may
+                        --  have been normalized into multiple simple clauses.
+
+                        Remove (Ref_Clause);
+
+                     --  Otherwise the output of the refinement clause must be
+                     --  a valid constituent of the state:
+
+                     --    Refined_State   => (State => (C1, C2))
+                     --    Depends         => (State => <input>)
+                     --    Refined_Depends => (C1    => <input>)
+
+                     elsif Is_Entity_Name (Ref_Output) then
                         Ref_Id := Entity_Of (Ref_Output);
 
-                        --  The output of the refinement clause is a valid
-                        --  constituent of the state. Remove the clause from
-                        --  the pool of candidates if both input lists match.
-                        --  Note that the search continues because one clause
-                        --  may have been normalized into multiple clauses as
-                        --  per the example above.
-
                         if Ekind_In (Ref_Id, E_Abstract_State, E_Variable)
                           and then Present (Encapsulating_State (Ref_Id))
                           and then Encapsulating_State (Ref_Id) = Dep_Id
@@ -21453,6 +21475,12 @@
                                       Post_Errors => False)
                         then
                            Has_Constituent := True;
+
+                           --  Note that the search continues after the clause
+                           --  is removed from the pool of candidates because
+                           --  it may have been normalized into multiple simple
+                           --  clauses.
+
                            Remove (Ref_Clause);
                         end if;
                      end if;
@@ -21819,12 +21847,13 @@
       begin
          --  Construct a list of all refinement inputs. Note that the input
          --  list is copied because the algorithm modifies its contents and
-         --  this should not be visible in Refined_Depends.
+         --  this should not be visible in Refined_Depends. The same applies
+         --  for a solitary input.
 
          if Nkind (Inputs) = N_Aggregate then
             Ref_Inputs := New_Copy_List (Expressions (Inputs));
          else
-            Ref_Inputs := New_List (Inputs);
+            Ref_Inputs := New_List (New_Copy (Inputs));
          end if;
 
          --  Depending on whether the original dependency clause mentions