FSF: unknown option '--giant-step-rac'

[simonjwright]

With branch fsf, commit 911e1c4 of 7 Jan, gcc version 12.0.0 20220111, I get

$ /Volumes/Miscellaneous1/spark2014/install/bin/gnatprove -P gdi512 -f
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
+===========================GNAT BUG DETECTED==============================+
| 1.0 (spark) GCC error:                                                   |
| /Volumes/Miscellaneous1/spark2014/install/libexec/spark/bin/gnatwhy3:    |
|    unknown option '--giant-step-rac'.
Usage: gnatwhy3 [options] file
  --version            Print version information and exit
  --sh                                                                     |
| No source file position information available                            |
| Compiling /Users/simon/tmp/so/gdi512.adb                                 |
| Please submit a bug report; see https://gcc.gnu.org/bugs/ .              |
| Use a subject line meaningful to you and us to track the bug.            |
| Include the entire contents of this bug box in the report.               |
| Include the exact command that you entered.                              |
| Also include sources listed below.                                       |
+==========================================================================+

Please include these source files with error report
Note that list may not be accurate in some cases,
so please double check that the problem can still
be reproduced with the set of files listed.
Consider also -gnatd.n switch (see debug.adb).

/Users/simon/tmp/so/gdi512.adb

compilation abandoned
gnatprove: error during flow analysis and proof

A previous build (against 4e09455 of 25 October) didn’t show this problem - that build showed Why3 for gnatprove version 1.4.0+git, this one shows 1.3.3+git - ??

gdi512.zip

[simonjwright]

This is clearly a (very late) response to #31

[simonjwright]

Sorry, finger trouble

[yannickmoy]

Hi @simonjwright, can you check the hash of the why3 submodule? It should be b342316a44b4d19b8bbc13e3e317067966c438bc after you update it with git submodule update. This include support for the new switch --giant-step-rac.

[simonjwright]

The hash is 7d6a684def225f704a00be762ed6aa2d4dbafbcd, it’s stuck at this. I’ve tried submodule update, submodule sync: no difference. The other submodules match.

The repo shows why3 should be a6c3fa0, not b342316a44b4d19b8bbc13e3e317067966c438bc?

On 13 Jan 2022, at 17:53, yannickmoy @.***> wrote:

Hi @simonjwright, can you check the hash of the why3 submodule? It should be b342316a44b4d19b8bbc13e3e317067966c438bc after you update it with git submodule update. This include support for the new switch --giant-step-rac.

— Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android. You are receiving this because you were mentioned.

[yannickmoy]

I gave you the wrong head for the why3 submodule on fsf branch, it should indeed be a6c3fa0 which is more recent than b34231 so also includes the new switch --giant-step-rac. Can you check that you rebuild/install gnatwhy3?

[simonjwright]

I had a lot of problems with git, resolved by (locally!) deleting the fsf branch and checking it out again.

Then, missed make install-all.

Now running successfully with a6c3fa0.

[yannickmoy]

glad that it had a happy conclusion! thanks for letting me know