6

I am trying to test a function with Frama-c:

/*@
    ensures \result >= x && \result >= y;
    ensures \result == x || \result == y;
*/

int max( int x, int y){
    return (x>y) ? x : y;
}

After I installed all the requirements: OPAM, why3, alt-ergo Whenever I execute frama-c -wp fct.c I receive:

[kernel] Parsing fct.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] User Error: Deferred error message was emitted during execution. 
See above messages for more information.
[kernel] Plug-in wp aborted: invalid user input.
I. Ali
  • 171
  • 2
  • 5

1 Answers1

11

As mentioned in Frama-C's installation instructions, why3 must be explicitely configured to check for available provers, through the why3 config --detect command (Note that, depending on the exact version of Why3 that you have installed, you might also use why3 config --full-config instead). You should see an output like:

Found prover Alt-Ergo version 2.0.0, OK.
... possibly other provers if you have installed them
Save config to /PATH/TO/HOME/.why3.conf

After that, you will be able to use the provers in Frama-C/WP

Virgile
  • 9,724
  • 18
  • 42
  • 1
    I tried the two commands but this is what I get: `Found prover Coq version 8.12.0, but no Why3 libraries were compiled for it Prover Alt-Ergo version 2.3.3 is not known to be supported. Known versions for this prover: 2.3.1, 2.3.0. Known old versions for this prover: . 1 prover(s) added (including 1 prover(s) with an unrecognized version) Generating strategies: Save config to /Users/aliissaoui/.why3.conf` – I. Ali Oct 02 '20 at 14:37
  • If you don't plan to use coq to terminate Frama-C or Why3 proofs, the first point shouldn't be a problem (but you might want to install the opam package `why3-coq`). The second point is simply an indication that your version of Why3 has not been tested againt your version of Alt-Ergo. Given the proximity with fully supported versions (2.3.3. vs 2.3.1), this shouldn't be a problem, but if you experience Alt-Ergo failures when doing proofs, you might consider downgrading to 2.3.1. – Virgile Oct 05 '20 at 06:06
  • 2
    It seems like the command line has changed? I need `why3 config detect`, I have why3 v1.4.0. It looks like the `opam install why3` tries to tell you this. The final message is *=> Why3 provers setup: rm -f ~/.why3.conf ; why3 config detect*, but if you have never used opam it is not clear this is instructions for the user. I thought it was a command that was performed by opam. – artless noise Aug 20 '21 at 14:23
  • @artlessnoise yes, why3 has changed its command line syntax for detecting provers three times in the last three releases (but a developer -speaking on strict condition of anonymity - promised me that 1.4.0 was the last time). Normally, each Frama-C installation instructions contains the appropriate command line for the corresponding Why3 version. – Virgile Aug 23 '21 at 13:28