--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on December 2019 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Trouble With Why3 and New Frama-C 20.0



I'm currently using Void Linux x86_64 5.4.2_1, if that's of any help.

I have been messing around with Frama-C and wp for a little bit, but
the transition to Why3 has hit me with something odd that prevents me
from using wp. I've tried reinstalling using an essentially blank
slate (`rm -rf ~/.opam`), unless there are some residual configuration
files somewhere else. Here's the example file I'm using, just for
demonstration purposes:

    /*@
        logic boolean u8_continue_f(unsigned char b) =
            0x80 <= b <= 0xBF;
    */
    /*@
        assigns \nothing;
        ensures \result == (int)u8_continue_f(b);
    */
    int u8_is_continue(const unsigned char b)
    {
        return b >= 0x80 && b <= 0xBF;
    }

Note that if I run Frama-C with `native:alt-ergo`, then this passes fine:

    desktop$ frama-c -wp -wp-prover native:alt-ergo test.c 
    [kernel] Parsing test.c (with preprocessing)
    [wp] Warning: Missing RTE guards
    [wp] Warning: native support for alt-ergo is deprecated, use why3 instead
    [wp] 4 goals scheduled
    [wp] Proved goals:    4 / 4
      Qed:             3  (0.33ms-2ms-6ms)
      Alt-Ergo:        1  (11ms) (88)


The first time I run Frama-C 20.0, I got this message:

    desktop$ frama-c -wp test.c 
    [kernel] Parsing test.c (with preprocessing)
    [wp] Warning: Missing RTE guards
    [wp] User Error: No prover in /home/thz/.why3.conf corresponds to "alt-ergo"
    [kernel] Plug-in wp aborted: invalid user input.

After that I ran `why3 config --detect`, which detects
alt-ergo 2.3.0 and Isabelle 2019 (though it only supports up to 2018).

After generating `~/.why3.conf`, I try running Frama-C again, and I get this:

   desktop$ frama-c -wp test.c 
   [kernel] Parsing test.c (with preprocessing)
   [wp] Warning: Missing RTE guards
   [wp] 4 goals scheduled
   [wp] [Alt-Ergo 2.3.0] Goal typed_u8_is_continue_ensures : Failed
     [Why3 Error] Library file not found: qed
   [wp] Proved goals:    3 / 4
     Qed:               3 
     Alt-Ergo 2.3.0:    0  (failed: 1)


After a few days of poking around, I can get some progress by making this change
to the ~/.why3.conf file:

    [main]
    default_editor = "vis %f"
 +  loadpath = "/home/thz/.opam/4.05.0/share/frama-c/wp/why3/frama_c_wp/"
    loadpath = "/home/thz/.opam/4.05.0/share/why3/stdlib"

Which then gets me here:

    desktop$ frama-c -wp test.c 
    [kernel] Parsing test.c (with preprocessing)
    [wp] Warning: Missing RTE guards
    [wp] 4 goals scheduled
    [wp] [Alt-Ergo 2.0.0] Goal typed_u8_is_continue_ensures : Failed
      [Why3 Error] Ident zleq is not yet declared
    [wp] Proved goals:    3 / 4
      Qed:               3 
      Alt-Ergo 2.0.0:    0  (failed: 1)

At which point I'm stuck. A similar thing happens on my laptop (which also uses
Void Linux). How can I fix this, or at least get some more detailed error messages
so I can poke around and figure out what's wrong? Any help is appreciated.