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: loic.correnson at cea.fr (Loïc Correnson)
  • Date: Wed, 14 May 2014 13:27:09 +0200
  • In-reply-to: <eaf36764a5f64d963aaaa78117316a9b@sybille.onecert.fr>
  • References: <eaf36764a5f64d963aaaa78117316a9b@sybille.onecert.fr>
Hello,
Sorry for the late answer.

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

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

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

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

Seems to be the same problem than your first question, but I can not reproduce it on my side.

> 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

	L.




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140514/bf9615bf/attachment.html>