From: pmderodat <pmderodat@138bc75d-0d04-0410-961f-82ee72b054a4>
Date: Tue, 21 Aug 2018 14:48:35 +0000 (+0000)
Subject: [Ada] Crash processing SPARK annotate aspect
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=36bf51692bb3710f921fb4c1be7349db1e95cf26;p=thirdparty%2Fgcc.git

[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.

git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@263732 138bc75d-0d04-0410-961f-82ee72b054a4
---

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index ff886ebd7893..1d21061cd28b 100644
--- 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 9a54fa9dbcd9..beb9489ef093 100644
--- 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 ddc6e0dc13bd..b4f0c41116db 100644
--- 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
index 000000000000..cb6c3b842e21
--- /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
index 000000000000..c60b1e27501c
--- /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;