search

Frama-C / Frama-C-snapshot

Release snapshots of the Frama-C platform for source code analysis
http://frama-c.com
165 stars 38 forks source link

Prover 'alt-ergo' not found in why3.conf #49

Closed BehnazR closed 6 months ago

BehnazR commented 6 months ago

Hello,

I know I should have asked on GitLab (I am waiting for approval), but I was hoping someone could help me here.

I am facing this issue using the latest version of Frama-C using opam. Below are the methods I tried to solve this issue: -- why3 config detect: finds alt-ergo and the why3.conf contains the correct address -- Manually add the alt-ergo to why3.conf using the add-prover command -- The PATH is also updated and shows the correct directory of alt-ergo -- Reinstall alt-ergo and why3 -- Check the execution permission for alt-ergo

I installed Frama-C on my Windows using WSL2 and Mint system followed the Frama-C website's instructions and got the same error.

Here are the current versions: opam 2.1.2 ocaml 4.13.1 why3 1.7.1 alt-ergo 2.5.2

Below is what I get after trying running -wp: [kernel] Parsing max.c (with preprocessing) [wp] Warning: Missing RTE guards [wp] User Error: Prover 'alt-ergo' not found in why3.conf [wp] Goal typed_max_ensures : not tried [wp] Goal typed_max_ensures_2 : not tried [wp:pedantic-assigns] max.c:6: Warning: No 'assigns' specification for function 'max'. Callers assumptions might be imprecise. [wp] User Error: Deferred error message was emitted during execution. See above messages for more information. [kernel] Plug-in wp aborted: invalid user input.

maroneze commented 6 months ago

I'm not sure what you mean by "waiting for approval"; normally our Gitlab registration is automatic, based on your Github account: choose the "sign in with GitHub" button, then login to Github and authorize our Gitlab OAuth:

Screenshot_20240301_110034

Screenshot_20240301_110048

Screenshot_20240301_110457

Did you try it and got the "waiting for approval"? Or did you do something else?

Concerning the issue with why3, I'm not entirely sure of what's happening, but you might want to consider following the reference configuration to ensure the versions you are using have been tested by us. In particular, our file currently lists why3.1.6.0 and alt-ergo.2.4.2. It does happen that new why3 or alt-ergo releases are initially incompatible, and then we have to adapt Frama-C (or blacklist versions) to ensure it works.

(But I'm not a WP developer, so take my advice with a grain of salt.)

vprevosto commented 6 months ago

Indeed, as indicated by this thread Frama-C 28.0 cannot use Why3 1.7.0 together with Alt-Ergo 2.5.2. This is probably also the case for Why3 1.7.1, as the observed behavior is not considered a bug on Why3's part. Upcoming Frama-C 28.1 will fix that, as well as reverting to why3 1.6.0.

BehnazR commented 6 months ago

@maroneze Yes, I followed the same steps and got "pending approval" so I thought there should be some permission grant. Thank you so much for your advice, it is working now! I thought frama-c would take care of the supported dependencies as it did not mention anything regarding this on the website.

@vprevosto Thank you for your response! Yes, using the supported versions makes it work.