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