Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Trouble With Why3 and New Frama-C 20.0
  • From: hirohito at cock.li (Emperor Hirohito)
  • Date: Wed, 18 Dec 2019 12:09:50 -0600
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.