--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on May 2014 ---
> 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. It is also my guess. Have also a look to frama-c -print-*-path options, -share and -wp-share options. > 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 ? Of course, this is the nature of inductive types, indeed. You should also consider the following methodology : 1. Declare in Coq your inductive predicate, in a self-consistent Coq module. 2. Declare an *abstract* predicate in ACSL, and state the useful lemmas you want to USE for proving your code. 3. Define a WP-driver (WP ? 2.3.10) that informs WP to link the ACSL predicate to your Coq module. And then, your done in a very sound way. This can be generalized for types and many other interesting things. > I also found what seems to be a bug, I filled a bug report, I hope that it > was the thing to do. Sure. The same for ay feature wish. Regards, L.