--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on May 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Questions on wp about _Bool, inductive predicates and Coq



> 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.