search

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

From_Universal_Image not present in FSF runtime #31

Closed kanigsson closed 3 years ago

kanigsson commented 3 years ago

As reported by @simonjwright on issue #28, SPARK FSF branch can't be built by latest FSF compiler:

spark_rac.adb:1132:15: "From_Universal_Image" is undefined (more references follow)
kanigsson commented 3 years ago

This is fixed in c7439e4, you can cherry-pick the commit or wait until it hits the fsf branch.

simonjwright commented 3 years ago

Surprise, the extant fsf branch built with gcc-12.0.0, but had other problems, so will try this cherry-pick with gcc 11.2.0.

simonjwright commented 3 years ago

and ...

exp_imgv.adb:58:06: "System.Perfect_Hash_Generators" is not a predefined library unit

(I tried this with -k, that was the only reported error)

kanigsson commented 3 years ago

Hello Simon, I think GCC 11.2.0 is too old now. What is your issue with gcc-12.0.0 (by the way what do you mean by that, is it just the master branch of gcc)?

simonjwright commented 3 years ago

Sorry, not an issue with gcc-12.0.0, rather an issue with gnatprove -- should I post it in this issue, or raise a new one? (I suspect it’s a change in your master that’s not got into fsf, gnat2why complaining about unknown option '--giant-step-rac')

yannickmoy commented 3 years ago

Hi @simonjwright , can you open another issue? Indeed, that seems to be an issue with synchronization between the fsf branch of spark2014 and its why3 submodule.