--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on May 2014 ---
Hi, Thanks for your answer. Le 14.05.2014 13:27, Lo?c Correnson a ?crit : >> [wp] [Alt-Ergo] Goal typed_lemma_lem0 : Failed >> Error: characters 52-67:typing error: undefined symbol bit_testb > > I can not reproduce the bug with my Neon. Are you sure you get the > right version ? > > $ frama-c -version > Version: Neon-20140301 Yes I use exactly this version. But I have two versions installed (in different prefix) so maybe there is a conflict between the share folder, I'm going to investigate since it seems dependent of my installation. >> //@ predicate test<A>(A x, A y) = x == y; >> >> //@ lemma lem1 : forall _Bool x, y; test(!x, y); >> >> -- test.c:6:[kernel] user error: invalid implicit conversion from >> _Bool to ? in annotation. > > The type _Bool is defined in ISO/C, it is an alias to a C-integer > (int) regarded as a C-boolean. > Hence, ACSL boolean values are not expected here. Yes the problem is not really the _Bool it is just that the type inference does not behave as I was expecting. It casts !x to ACSL boolean I would have expected that y would have been converted to ACSL boolean automatically too but it seems not the case. >> 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 ? > > Indeed, providing an inversion lemma is very dangerous, especially > when your predicate is recursively defined. > Actually, SMT solvers may instantiate the inversion lemma infinitely. > This is very difficult problem to handle. > If you need so, then simply add it by hand. There are some tricks with > triggers to be explored on this subject. Ok. Just to be sure it can only be added as an axiom, right ? There is no way of proving it with what is exported by wp ? >> 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 ? > > This is automatically done at configure time when compiling Frama-C/WP > when Coq is detected to be installed. > If you don?t want to reconfigure and rebuild frama-c entirely, you > can also type: > # make wp-coq > # [sudo] make wp-cod-install It works perfectly, it will save me a lot of time. I also found what seems to be a bug, I filled a bug report, I hope that it was the thing to do. Guillaume Davy