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 <kirtc...@adacore.com>
* sem_prag.adb (Analyze_Constituent): Stop the
analysis after detecting a misplaced constituent as this is a
critical error.
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 230236)
+++ sem_prag.adb (working copy)
@@ -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
