This patch updates the analysis of Refined_State triggered by contract freezing to raise a more suitable exception when compilation has to be halted.
------------ -- Source -- ------------ -- pack.ads package Pack with Abstract_State => State is function F return Boolean with Global => State; generic package Gen_Pack with Abstract_State => Gen_State, Initial_Condition => F is procedure Proc (X : in out Integer); end Gen_Pack; private A : Integer with Part_Of => State; end Pack; -- pack.adb package body Pack with Refined_State => (State => (A, B, Inst_Pack.Gen_State)) is B : Integer := 6; function F return Boolean is (B > 0); package body Gen_Pack with Refined_State => (Gen_State => C) is C : Integer; procedure Proc (X : in out Integer) is begin if C = X and A = X then X := C; end if; end Proc; begin Proc (C); end Gen_Pack; package Inst_Pack is new Gen_Pack; begin Inst_Pack.Proc (B); end Pack; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c pack.adb pack.adb:2:08: body "F" declared at line 6 freezes the contract of "Pack" pack.adb:2:08: all constituents must be declared before body at line 6 pack.adb:2:42: "Inst_Pack" is undefined compilation abandoned Tested on x86_64-pc-linux-gnu, committed on trunk 2017-09-25 Hristian Kirtchev <kirtc...@adacore.com> * sem_prag.adb (Analyze_Constituent): Raise Unrecoverable_Error rather than Program_Error because U_E is more in line with respect to the intended behavior.
Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 253134) +++ sem_prag.adb (working copy) @@ -13219,7 +13219,7 @@ Analyze (N); raise Pragma_Exit; - -- No other possibilities + -- No other possibilities when others => raise Program_Error; @@ -27448,7 +27448,7 @@ -- Stop the compilation, as this leads to a multitude -- of misleading cascaded errors. - raise Program_Error; + raise Unrecoverable_Error; end if; -- The constituent is a valid state or object