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 <[email protected]>
* 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
