[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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index ff886ebd7893a76a1109f2943f6ad14bc0b3588d..1d21061cd28b38d8d9debc9b09767dc8752c1846 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+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

diff --git a/gcc/ada/lib-writ.adb b/gcc/ada/lib-writ.adb
index 9a54fa9dbcd9a6626d30fc429b2099f20bc18e2d..beb9489ef0931e3f3b33d0e57cc2f86504b6ac43 100644 (file)
--- a/gcc/ada/lib-writ.adb
+++ b/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 (' ');
 

diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog
index ddc6e0dc13bd30ed0f941bb9d285b76988659598..b4f0c41116db501d5fa16e24c8a8debb504d5aa6 100644 (file)
--- a/gcc/testsuite/ChangeLog
+++ b/gcc/testsuite/ChangeLog
@@ -1,3 +1,7 @@
+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.

diff --git a/gcc/testsuite/gnat.dg/spark2.adb b/gcc/testsuite/gnat.dg/spark2.adb
new file mode 100644 (file)
index 0000000..cb6c3b8
--- /dev/null
+++ b/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;

diff --git a/gcc/testsuite/gnat.dg/spark2.ads b/gcc/testsuite/gnat.dg/spark2.ads
new file mode 100644 (file)
index 0000000..c60b1e2
--- /dev/null
+++ b/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;