--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on December 2019 ---
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.