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

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