From 322d87a9b17660f7d04a7320505591538582892a Mon Sep 17 00:00:00 2001 From: Javier Miranda Date: Tue, 21 Aug 2018 14:48:35 +0000 Subject: [PATCH] [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 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 | 5 +++++ gcc/ada/lib-writ.adb | 9 ++++++++- gcc/testsuite/ChangeLog | 4 ++++ gcc/testsuite/gnat.dg/spark2.adb | 12 ++++++++++++ gcc/testsuite/gnat.dg/spark2.ads | 16 ++++++++++++++++ 5 files changed, 45 insertions(+), 1 deletion(-) create mode 100644 gcc/testsuite/gnat.dg/spark2.adb create mode 100644 gcc/testsuite/gnat.dg/spark2.ads 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 + + * lib-writ.adb (Write_Unit_Information): Handle pragmas removed + by the expander. + 2018-08-21 Ed Schonberg * 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 + + * gnat.dg/spark2.adb, gnat.dg/spark2.ads: New testcase. + 2018-08-21 Ed Schonberg * 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; -- 2.47.2