diff options
| author | Javier Miranda <miranda@adacore.com> | 2018-08-21 14:48:35 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2018-08-21 14:48:35 +0000 |
| commit | 322d87a9b17660f7d04a7320505591538582892a (patch) | |
| tree | f2c5a63f3c954a385252992ef259e7cb05ccc167 | |
| parent | 24241bd0388ec6f730788540b289da12c13a34cc (diff) | |
| download | gcc-322d87a9b17660f7d04a7320505591538582892a.zip gcc-322d87a9b17660f7d04a7320505591538582892a.tar.gz gcc-322d87a9b17660f7d04a7320505591538582892a.tar.bz2 | |
[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
| -rw-r--r-- | gcc/ada/ChangeLog | 5 | ||||
| -rw-r--r-- | gcc/ada/lib-writ.adb | 9 | ||||
| -rw-r--r-- | gcc/testsuite/ChangeLog | 4 | ||||
| -rw-r--r-- | gcc/testsuite/gnat.dg/spark2.adb | 12 | ||||
| -rw-r--r-- | gcc/testsuite/gnat.dg/spark2.ads | 16 |
5 files changed, 45 insertions, 1 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index ff886eb..1d21061 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 9a54fa9..beb9489 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 ddc6e0d..b4f0c41 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 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 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; |