diff mbox series

[Ada] Crash processing SPARK annotate aspect

Message ID 20180821150509.GA57233@adacore.com
State New
Headers show
Series [Ada] Crash processing SPARK annotate aspect | expand

Commit Message

Pierre-Marie de Rodat Aug. 21, 2018, 3:05 p.m. UTC 
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  <miranda@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.
diff mbox series

Patch

--- 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;