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] Questions on wp about _Bool, inductive predicates and Coq
- Subject: [Frama-c-discuss] Questions on wp about _Bool, inductive predicates and Coq
- From: Guillaume.Davy at onera.fr (Guillaume Davy)
- Date: Mon, 31 Mar 2014 10:53:17 +0200
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