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

  • Subject: [Frama-c-discuss] Questions on wp about _Bool, inductive predicates and Coq
  • From: Guillaume.Davy at onera.fr (Guillaume Davy)
  • Date: Mon, 31 Mar 2014 10:53:17 +0200
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