--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on March 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



Hello,


I have small questions to ask about frama-c with Wp plugin, I'm using 
Neon version.


1 -

-----

//@ lemma lem0 : \forall _Bool x, y;(!x) == y;

-----

This lemma is accepted by frama-c/wp but when I send it
to native Alt-Ergo, I get the following error :

[wp] [Alt-Ergo] Goal typed_lemma_lem0 : Failed
Error: characters 52-67:typing error: undefined symbol bit_testb

It is not a big problem for me since it works with native Coq and Why3 
but
it sounds like a bug.


2 -

-----

//@ predicate test<A>(A x, A y) = x == y;

//@ lemma lem1 : \forall _Bool x, y; test(!x, y);

-----

I get the following error :

-- test.c:6:[kernel] user error: invalid implicit conversion from _Bool 
to ? in annotation.

I found this workaround :

//@ lemma lem1 : \forall _Bool x, y; test(!x, y==1);

Since I did not find any information about _Bool in frama-c/wp 
documentation(maybe I missed it),
I don't know if it is a bug or if there is something more natural to do 
than adding ==1.
For example I tried an explicit cast with (boolean) but I get :

-- test.c:6:[kernel] user error: cannot cast to logic type in 
annotation.


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 ?


4 - When I tried to use Native Coq I had a problem during the 
compilation of Coq wp libraries :

[wp] [Coq] Compiling 'BuiltIn.v'.
[wp] [Coq] Compiling 'Bool.v'.
[wp] [Coq] Compiling 'Int.v'.
[wp] [Coq] Compiling 'Abs.v'.
[wp] [Coq] Compiling 'ComputerDivision.v'.
[wp] [Coq] Compiling 'Real.v'.
[wp] [Coq] Compiling 'RealInfix.v'.
[wp] [Coq] Compiling 'FromInt.v'.
[wp] [Coq] Compiling 'Map.v'.
[wp] [Coq] Compiling 'Qedlib.v'.
[wp] [Coq] Compiling 'Qed.v'.
[wp] [Coq] Compiling 'Cint.v'.
[wp] [Coq] 'Cint.v' compilation failed.
File "/udd/deri/gdavy/.frama-c-wp/coqwp/Cint.v", line 260, characters 
0-21:
Error: Cannot find library Zbits in loadpath
[wp] [Coq] Goal typed_lemma_lem2 : Failed
      Error: Compilation of 'Cint.v' failed.

The problem comes from the order of the compiled files so I modified 
/usr/share/frama-c/wp/wp.driver to have Cint
compiled after Zbits but before Cbits and it seems to work perfectly. I 
don't know if this problem is related to
my installation but the workaround could be useful to someone else.


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 ?


Thanks for reading me,


Guillaume DAVY