[Ada] Crash processing SPARK annotate aspect

The compiler blows up writing the ALI file of a package that has a ghost
subprogram with an annotate contract.

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.

From-SVN: r263732

gcc/ada/ChangeLog

+2018-08-21  Javier Miranda  <miranda@adacore.com>
+
+	* lib-writ.adb (Write_Unit_Information): Handle pragmas removed
+	by the expander.
+
 2018-08-21  Ed Schonberg  <schonberg@adacore.com>
 
 	* sem_ch6.adb (Check_Synchronized_Overriding): The conformance

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 (' ');
 

gcc/testsuite/ChangeLog

+2018-08-21  Javier Miranda  <miranda@adacore.com>
+
+	* gnat.dg/spark2.adb, gnat.dg/spark2.ads: New testcase.
+
 2018-08-21  Ed Schonberg  <schonberg@adacore.com>
 
 	* gnat.dg/prot6.adb, gnat.dg/prot6.ads: New testcase.

gcc/testsuite/gnat.dg/spark2.adb

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

gcc/testsuite/gnat.dg/spark2.ads

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