--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on March 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP 0.9 (for Magnesium) Compatible with Coq 8.5?



Hello, all!

As reported in the previous e-mail, I'm having trouble verifying this in 
WP (also attached):

   /*@ lemma ptr_inc:  \forall int n, *v, *p;
         n >= 0 ==> \valid_read(v + (0..n-1)) ==> v <= p < v+n ==>
         v <= p+1;
    */

I would like to use Coq to try out a proof, but running

   frama-c-gui -wp -wp-prover coqide lemma_ptr_inc.c

gives this output:

   [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i 
(no preprocessing)
   [kernel] Parsing lemma_ptr_inc.c (with preprocessing)
   [wp] Running WP plugin...
   [wp] Collecting axiomatic usage
   [wp] 1 goal scheduled
   [wp] [Coq] Compiling 'BuiltIn.v'.
   [wp] [Coq] 'BuiltIn.v' compilation failed.
   Don't know what to do with -as bool -as int -as real -as map
   See -help for the list of supported options
   [wp] [Coq] Goal typed_lemma_ptr_inc : Failed
        Error: Compilation of 'BuiltIn.v' failed.
   [wp] Proved goals:    0 / 1
        Coq:             0  (failed: 1)

Is WP 0.9 (for Magnesium-20151002) compatible with Coq 8.5 (which I'm 
using)? Am I doing something wrong?

Thanks in advance,

-- 
Pablo
http://lia.ufc.br/~pmsf/
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: lemma_ptr_inc.c
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160308/624e8609/attachment.c>