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



Just to say that the compatibility between WP 0.9 and Coq 8.5 is not 
urgent for me anymore: I created a fresh opam environment with Coq 
8.4pl6 + Why3 + Frama-C. (I still cannot verify the lemma, though.)

---
Pablo
http://lia.ufc.br/~pmsf/

Em 2016-03-08 13:22, Pablo M. S. Farias escreveu:
> 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/