===================================================================
@@ -25408,6 +25408,14 @@
SPARK_Msg_N
("\all constituents must be declared before body #",
N);
+
+ -- A misplaced constituent is a critical error because
+ -- pragma Refined_Depends or Refined_Global depends on
+ -- the proper link between a state and a constituent.
+ -- Stop the compilation, as this leads to a multitude
+ -- of misleading cascaded errors.
+
+ raise Program_Error;
end if;
-- The constituent is a valid state or object
This patch classifies a misplaced constituent as a critical error and stops the compilation. This ensures that the missing link between a constituent and state will not cause obscure cascaded errors. ------------ -- Source -- ------------ -- pack.ads package Pack with Spark_Mode => On, Abstract_State => Top_State, Initializes => Top_State is procedure Do_Something (Value : in out Natural; Success : out Boolean) with Global => (In_Out => Top_State), Depends => (Value =>+ Top_State, Success => (Value, Top_State), Top_State =>+ Value); end Pack; -- pack.adb package body Pack with SPARK_Mode => On, Refined_State => (Top_State => (Count, A_Pack.State)) is package A_Pack with Abstract_State => State, Initializes => State is procedure A_Proc (Test : in out Natural) with Global => (In_Out => State), Depends => (Test =>+ State, State =>+ Test); end A_Pack; package body A_Pack with Refined_State => (State => Total) is Total : Natural := 0; procedure A_Proc (Test : in out Natural) with Refined_Global => (In_Out => Total), Refined_Depends => ((Test =>+ Total, Total =>+ Test)) is begin if Total > Natural'Last - Test then Total := abs (Total - Test); else Total := Total + Test; end if; Test := Total; end A_Proc; end A_Pack; Count : Natural := 0; procedure Do_Something (Value : in out Natural; Success : out Boolean) with Refined_Global => (In_Out => (Count, A_Pack.State)), Refined_Depends => (Value =>+ (Count, A_Pack.State), Success => (Value, Count, A_Pack.State), Count =>+ null, A_Pack.State =>+ (Count, Value)) is begin Count := Count rem 128; if Count <= Value then Value := Count + (Value - Count) / 2; else Value := Value + (Count - Value) / 2; end if; A_Pack.A_Proc (Value); Success := Value /= 0; end Do_Something; end Pack; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c pack.adb pack.adb:3:09: body "A_Pack" declared at line 15 freezes the contract of "Pack" pack.adb:3:09: all constituents must be declared before body at line 15 pack.adb:3:41: "Count" is undefined compilation abandoned due to previous error Tested on x86_64-pc-linux-gnu, committed on trunk 2015-11-12 Hristian Kirtchev <kirtchev@adacore.com> * sem_prag.adb (Analyze_Constituent): Stop the analysis after detecting a misplaced constituent as this is a critical error.