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

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