fmap.adb:304:18: "Null_FD" is undefined

[Earnestly]

• Linux
• gcc 7.2.1
• GNATMAKE 7.2.1 20171128
• GPRBUILD Pro 18.0w (19940713) (x86_64-pc-linux-gnu)

Using https://github.com/AdaCore/spark2014/tree/gpl-2017

% make setup
...
% make
make -C gnat2why
make[1]: Entering directory '/.../gnat2why'
make -C why/xgen
make[2]: Entering directory '/.../gnat2why/why/xgen'
gprbuild -j0 -p -Phelpers xtree
Link
   [link]         xtree.adb
./xtree
cp why-classes.ads why-atree.ads why-atree-accessors.ads why-atree-builders.ads why-atree-builders.adb why-atree-mutators.ads why-atree-mutators.adb why-atree-traversal.ads why-atree-traversal.adb why-atree-traversal_stub.ads why-atree-traversal_stub.adb why-atree-treepr.ads why-atree-treepr.adb why-atree-validity.ads why-conversions.ads why-ids.ads why-kind_validity.ads why-opaque_ids.ads why-unchecked_ids.ads ../
make[2]: Leaving directory '/.../gnat2why/why/xgen'
mkdir -p obj obj-tools ../install/bin
sed -e "s^@ADAINCLUDE@^/usr/lib/gcc/x86_64-pc-linux-gnu/7.2.1/adainclude^" \
    -e "s^@ADALIB@^/usr/lib/gcc/x86_64-pc-linux-gnu/7.2.1/adalib^" \
    -e "s^@PREFIX@^@NOPREFIX@^" \
    -e "s^@GNAT1DIR@^/usr/lib/gcc/x86_64-pc-linux-gnu/7.2.1/^" \
    sdefault.adb.in > obj/sdefault.adb
for f in `cd gnat_src; ls xtreeprs.adb xnmake.adb xutil.ad? *-tmpl sinfo.ads treeprs.adt nmake.adt xsnamest.adb`; \
do \
  cp -p gnat_src/$f obj-tools; \
done
cd obj-tools && gnatmake -q xtreeprs xnmake xsnamest && \
./xtreeprs && ./xnmake && mv nmake.ads nmake.adb treeprs.ads ../obj && \
./xsnamest && mv snames.ns ../obj/snames.ads && mv snames.nb ../obj/snames.adb
cd obj && ln -sf ../gnat_src/*.ad[sb] .
cd obj && rm -rf x*.ad? system* mlib* back_end.adb \
  ada.ads gnat.ads interfac.ads unch*.ads text_io.ads && \
rm -rf ?-*.ad? && \
mv -f ada_get_targ.adb get_targ.adb
gprbuild  -Pgnat2why -j0 -cargs  -largs 
Compile
   [Ada]          gnat1drv.adb
   [C]            smissing.c
/.../gnat2why/smissing.c:67:1: warning: control reaches end of non-void function [-Wreturn-type]
}
^
1 warning generated.
   [Ada]          atree.adb
   [Ada]          back_end.adb
   [Ada]          checks.adb
   [Ada]          comperr.adb
   [Ada]          csets.adb
   [Ada]          debug.adb
   [Ada]          elists.adb
   [Ada]          errout.adb
   [Ada]          exp_cg.adb
   [Ada]          fmap.adb
fmap.adb:304:18: "Null_FD" is undefined

   compilation of fmap.adb failed

gprbuild: *** compilation phase failed
make[1]: *** [Makefile;66: build] Error 4
make[1]: Leaving directory '/.../gnat2why'
make: *** [Makefile;142: gnat2why] Error 2

[Earnestly]

My mistake. I was using the latest gcc code for the gnat2why/gnat_src symlink. I corrected this and switched to using the same gcc commit (bce1ab0478f96724828df51ccfd43197d917c572) my machine is using.

However next error:

[...]
   [Ada]          atree.adb
   [Ada]          back_end.adb
   [Ada]          checks.adb
   [Ada]          comperr.adb
   [Ada]          csets.adb
   [Ada]          debug.adb
   [Ada]          elists.adb
   [Ada]          errout.adb
spark_util.ads:489:16: "Within_Protected_Type" is undefined (more references follow)

   compilation of back_end.adb failed

gprbuild: *** compilation phase failed
make[1]: *** [Makefile;66: build] Error 4
make[1]: Leaving directory '/.../spark2014/gnat2why'
make: *** [Makefile;142: gnat2why] Error 2

It appears my version of gcc is ever so slightly too old for this codebase.

[yannickmoy]

Indeed, we do not have a suitable mechanism for synching the latest versions of GNAT and SPARK, due to the fact that the GNAT repo at AdaCore is not public, only the repo at the FSF is public and it is lagging a few days behind the GNAT repo. What we recommend if you want to rebuild SPARK is to rebuild the latest GPL release, following these instructions: https://github.com/AdaCore/spark2014#6-building-spark-with-a-gnat-gpl-compiler

[Earnestly]

Thank you, but I won't be using the "community" edition.