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 <kirtc...@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.
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