AdaCore / spark2014

SPARK 2014 is the new version of SPARK, a software development technology specifically designed for engineering high-reliability applications.
GNU General Public License v3.0
249 stars 33 forks source link

fsf branch not building gnat2why #28

Closed simonjwright closed 3 years ago

simonjwright commented 3 years ago

spark2014 commit: 5da8c83 gcc commit: f19c70a of 2021-08-11 macOS Big Sur 11.5 (darwin-20.6.0, x86_64) base compiler GCC 11.1.0

First,

gprbuild  -Pgnat2why -j0 -cargs  -largs 
Compile
   [Ada]          gnat1drv.adb
   [C]            smissing.c
restrict.ads:117:07: "No_Dynamic_Accessibility_Checks" is undefined

I worked round this by adding "gnat_src/libgnat" to GNAT2Why_GNAT’Source_Dirs.

Next,

gprbuild  -Pgnat2why -j0 -cargs  -largs 
Compile
   [Ada]          gnat1drv.adb
types.ads:149:04: run-time configuration error
types.ads:149:04: entity "System.Scalar_Values.Is_Is16" not defined

which looks to me as though my setup requires the 128-bit version, s-scaval__128.ad? (and indeed that’s the version in the compiler’s adainclude/).

pmderodat commented 3 years ago

Hello @simonjwright,

Thanks for reporting this issue, sorry for the delay. The fsf branch now contains a fix for the first issue (thanks to commit 869d8b7c424c80c817ff0d50822675d37b86c515). However I’m not able to reproduce the second error with today’s sources and compiling spark2014 with a freshly built GCC from the development branch: please re-open this if you still have problems.

simonjwright commented 3 years ago

I’m afraid that commit 869d8b7 doesn’t fix the problem with older compilers: the trouble is that building restrict.adb is done using gnat2why_gnat.gpr, which doesn’t see the new source copy in obj-gnat/ (btw, what kind of a misleading name is that! since it only contains Ada), and so uses the host compiler’s version of s-rident.ads.

$ gprbuild  -Pgnat2why -v -c -f restrict.adb
Changing to object directory of "GNAT2Why_GNAT": 
[...]
/Volumes/Miscellaneous1/spark2014/gnat2why/gnat_src/restrict.adb
restrict.ads:117:07: "No_Dynamic_Accessibility_Checks" is undefined (more references follow)
gprbuild: *** compilation phase failed

If I compile s-rident.ads, it’s done using gnat2why.gpr, which does see the source copy.

$ gprbuild  -Pgnat2why -v -c -f s-rident.ads
Changing to object directory of "GNAT2Why": 
[...]
/Volumes/Miscellaneous1/spark2014/gnat2why/obj-gnat/s-rident.ads
pmderodat commented 3 years ago

Arg yes, I misunderstood spark2014 engineers and thought a freshly built development branch of GCC FSF was necessary to build gnat2why, sorry about that. We’ll fix.

kanigsson commented 3 years ago

Hello @simonjwright , to our knowledge the issue is fixed now, can you please try again?

simonjwright commented 3 years ago

I think my original problem has probably been fixed, but

spark_rac.adb:1132:15: "From_Universal_Image" is undefined (more references follow)

This is macOS Big Sur 11.6 GCC 11.2.0 gcc-mirror commit 5f7976f of Oct 21 spark2014 commit 4e09455 GNATColl 21.0.0

kanigsson commented 3 years ago

I opened #31 for this new issue.