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