--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on March 2014 ---
Hello, I have small questions to ask about frama-c with Wp plugin, I'm using Neon version. 1 - ----- //@ lemma lem0 : \forall _Bool x, y;(!x) == y; ----- This lemma is accepted by frama-c/wp but when I send it to native Alt-Ergo, I get the following error : [wp] [Alt-Ergo] Goal typed_lemma_lem0 : Failed Error: characters 52-67:typing error: undefined symbol bit_testb It is not a big problem for me since it works with native Coq and Why3 but it sounds like a bug. 2 - ----- //@ predicate test<A>(A x, A y) = x == y; //@ lemma lem1 : \forall _Bool x, y; test(!x, y); ----- I get the following error : -- test.c:6:[kernel] user error: invalid implicit conversion from _Bool to ? in annotation. I found this workaround : //@ lemma lem1 : \forall _Bool x, y; test(!x, y==1); Since I did not find any information about _Bool in frama-c/wp documentation(maybe I missed it), I don't know if it is a bug or if there is something more natural to do than adding ==1. For example I tried an explicit cast with (boolean) but I get : -- test.c:6:[kernel] user error: cannot cast to logic type in annotation. 3 - I was trying to use inductive predicates, It seems that in wp, no inversion Lemma is given to provers (Whereas in Jessie there is one). Is it a feature that will be implemented in the future or is there a deep reason for not having inversion lemma given to smt/Coq ? 4 - When I tried to use Native Coq I had a problem during the compilation of Coq wp libraries : [wp] [Coq] Compiling 'BuiltIn.v'. [wp] [Coq] Compiling 'Bool.v'. [wp] [Coq] Compiling 'Int.v'. [wp] [Coq] Compiling 'Abs.v'. [wp] [Coq] Compiling 'ComputerDivision.v'. [wp] [Coq] Compiling 'Real.v'. [wp] [Coq] Compiling 'RealInfix.v'. [wp] [Coq] Compiling 'FromInt.v'. [wp] [Coq] Compiling 'Map.v'. [wp] [Coq] Compiling 'Qedlib.v'. [wp] [Coq] Compiling 'Qed.v'. [wp] [Coq] Compiling 'Cint.v'. [wp] [Coq] 'Cint.v' compilation failed. File "/udd/deri/gdavy/.frama-c-wp/coqwp/Cint.v", line 260, characters 0-21: Error: Cannot find library Zbits in loadpath [wp] [Coq] Goal typed_lemma_lem2 : Failed Error: Compilation of 'Cint.v' failed. The problem comes from the order of the compiled files so I modified /usr/share/frama-c/wp/wp.driver to have Cint compiled after Zbits but before Cbits and it seems to work perfectly. I don't know if this problem is related to my installation but the workaround could be useful to someone else. 5- By the way is it possible to tell wp to save the previous Coq compilation to not have coq files recompile each time you restart frama-c ? Thanks for reading me, Guillaume DAVY