--- layout: fc_discuss_archives title: Message 8 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



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