The compiler blows up writing the ALI file of a package that has a ghost
subprogram with an annotate contract.
Tested on x86_64-pc-linux-gnu, committed on trunk
2018-08-21 Javier Miranda <mira...@adacore.com>
gcc/ada/
* lib-writ.adb (Write_Unit_Information): Handle pragmas removed
by the expander.
gcc/testsuite/
* gnat.dg/spark2.adb, gnat.dg/spark2.ads: New testcase.--- gcc/ada/lib-writ.adb
+++ gcc/ada/lib-writ.adb
@@ -744,7 +744,14 @@ package body Lib.Writ is
Note_Unit := U;
end if;
- if Note_Unit = Unit_Num then
+ -- No action needed for pragmas removed by the expander (for
+ -- example, pragmas of ignored ghost entities).
+
+ if Nkind (N) = N_Null_Statement then
+ pragma Assert (Nkind (Original_Node (N)) = N_Pragma);
+ null;
+
+ elsif Note_Unit = Unit_Num then
Write_Info_Initiate ('N');
Write_Info_Char (' ');
--- /dev/null
new file mode 100644
+++ gcc/testsuite/gnat.dg/spark2.adb
@@ -0,0 +1,12 @@
+-- { dg-do compile }
+
+package body SPARK2 with SPARK_Mode is
+ function Factorial (N : Natural) return Natural is
+ begin
+ if N = 0 then
+ return 1;
+ else
+ return N * Factorial (N - 1);
+ end if;
+ end Factorial;
+end SPARK2;
--- /dev/null
new file mode 100644
+++ gcc/testsuite/gnat.dg/spark2.ads
@@ -0,0 +1,16 @@
+package SPARK2 with SPARK_Mode is
+
+ function Expon (Value, Exp : Natural) return Natural is
+ (if Exp = 0 then 1
+ else Value * Expon (Value, Exp - 1))
+ with Ghost,
+ Pre => Value <= Max_Factorial_Number and Exp <= Max_Factorial_Number,
+ Annotate => (GNATprove, Terminating); -- CRASH!
+
+ Max_Factorial_Number : constant := 6;
+
+ function Factorial (N : Natural) return Natural with
+ Pre => N < Max_Factorial_Number,
+ Post => Factorial'Result <= Expon (Max_Factorial_Number, N);
+
+end SPARK2;
