search

AdaCore / RecordFlux

Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
Apache License 2.0
105 stars 6 forks source link

`make prove` fails with `gnatprove: unrecognized option '--checks-as-errors=on'` #1303

Closed mgrojo closed 3 weeks ago

mgrojo commented 4 weeks ago

Invocations to gnatprove seem to require a newer version compared to the one available in Alire.

When running make prove

/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/.venv.poetry/bin/poetry run make -C tests/spark prove
make[1]: se entra en el directorio '/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/tests/spark'
/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/tools/gnatprove -Ptest -Xtest=
gnatprove: unrecognized option '--checks-as-errors=on'
try "gnatprove --help" for more information.
make[1]: *** [Makefile:32: prove] Error 1
make[1]: se sale del directorio '/home/mgr/src/github/mgrojo/coap_spark/tools/RecordFlux/tests/spark'
make: *** [Makefile:494: prove_tests] Error 2

After looking at https://github.com/AdaCore/spark2014/commit/3e33794eb73f0fca408dccb48148e6f1492f8bbd I changed --checks-as-errors=on to --checks-as-errors. But there are more incompatibilities:

gnatprove: unrecognized option '--function-sandboxing=off'

gnatprove on PATH is version 14.1.1 as installed by Alire. RecordFlux is v0.24.0.

senier commented 3 weeks ago

Hi @mgrojo,

thank you for your report!

As you have noticed, we do not officially support the Alire version of gnatprove for developing RecordFlux. SPARK Pro is a prerequisite for that. Consequently, the internal testsuite is run only with the Pro tools.

That being said, you may still be able to verify most of the code you generate with RecordFlux using the toolchain from Alire. Are you sure you're really using the most recent version? When adding gnatprove to the install_gnat target, removing "colibri" from the list of provers in tests/spark/test.gpr and then using $ eval make_printenv_gnat to setup your environment you should be able to get the proofs started without fatal errors. Note, that there may be a few unproven verification conditions, though.

mgrojo commented 3 weeks ago

Are you sure you're really using the most recent version?

No, it seems I wasn't. Thanks.

✓ Installation targets fully solved
error: Release gnatprove=14.1.1 has another version already installed:
error:    gnatprove=12.1.1:
error:    Releases installing executables can be installed only once:
error:    Forcing this install will overwrite the release already installed. (This error can be overridden with --force.)

After forcing the update and removing "colibri", I got what I think you expected.


------------------------------------------------------------------------------------------------------------------------
SPARK Analysis results        Total        Flow                                           Provers   Justified   Unproved
------------------------------------------------------------------------------------------------------------------------
Data Dependencies                 1           1                                                 .           .          .
Flow Dependencies                 3           3                                                 .           .          .
Initialization                  197         197                                                 .           .          .
Non-Aliasing                      .           .                                                 .           .          .
Run-time Checks                1991           .    1989 (CVC5 1%, Trivial 5%, Z3 94%, altergo 0%)           .          2
Assertions                      105           .              104 (Trivial 1%, Z3 97%, altergo 2%)           .          1
Functional Contracts           1332           .    1332 (CVC5 0%, Trivial 1%, Z3 99%, altergo 0%)           .          .
LSP Verification                  .           .                                                 .           .          .
Termination                     126         126                                                 .           .          .
Concurrency                       .           .                                                 .           .          .
------------------------------------------------------------------------------------------------------------------------
Total                          3755    327 (9%)                                        3425 (91%)           .     3 (0%)

I'll close this as it has been clarified. Thanks.