https://gcc.gnu.org/bugzilla/show_bug.cgi?id=67706
Bug ID: 67706
Summary: Recursive Ghost expression function confuses the
compiler
Product: gcc
Version: 4.9.3
Status: UNCONFIRMED
Severity: normal
Priority: P3
Component: ada
Assignee: unassigned at gcc dot gnu.org
Reporter: phil at sparksure dot com
Target Milestone: ---
Created attachment 36385
--> https://gcc.gnu.org/bugzilla/attachment.cgi?id=36385&action=edit
Miniml spec and body producing the error
D:\SPARK2014\Exercises>gcc -v
Using built-in specs.
COLLECT_GCC=gcc
COLLECT_LTO_WRAPPER=f:/gnat/2015/bin/../libexec/gcc/i686-pc-mingw32/4.9.3/lto-wr
apper.exe
Target: i686-pc-mingw32
Configured with: ../src/configure --enable-languages=ada,c,c++
--enable-threads=
win32 --enable-lto --disable-sjlj-exceptions --enable-frame-pointer
--with-bugur
l=URL:mailto:rep...@adacore.com --disable-nls --without-libiconv-prefix
--disabl
e-libmudflap --disable-libstdcxx-pch --disable-libada --enable-checking=release
--disable-libsanitizer --disable-libcc1 --disable-libcilkrts
--with-mpfr=/gnatma
il/sandbox/gpl-2015/x86-windows/mpfr/install
--with-gmp=/gnatmail/sandbox/gpl-20
15/x86-windows/gmp/install
--with-mpc=/gnatmail/sandbox/gpl-2015/x86-windows/mpc
/install
--with-build-time-tools=/gnatmail/sandbox/gpl-2015/x86-windows/gcc/buil
d/buildtools/bin --prefix=/gnat-prefix-47 --build=i686-pc-mingw32
Thread model: win32
gcc version 4.9.3 20150428 (for GNAT GPL 2015 20150428) (GCC)
Windows 7 Professional
GPS 6.1.1 (20150118) hosted on i686-pc-mingw32
GNAT GPL 2015 (20150428-49)
The attached code should compile without error.
The actual output is:
gprbuild -ws -c -f -u -PD:\SPARK2014\Exercises\exercises.gpr f.adb
gcc -c f.adb
cannot generate code for file f.adb (package spec)
gprbuild: *** compilation phase failed
[2015-09-24 09:19:09] process exited with status 4, elapsed time: 11.65s
If Fact_P is not given the Ghost aspect then the compilation succeeds. It also
succeeds if it is rewritten as a normal function.
Other (non-recursive) Ghost expression functions compile successfully.
