--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on March 2016 ---
Hello, WP 0.9 (for Magnesium-20151002) is compatible with > coqc -v The Coq Proof Assistant, version 8.4pl5 (March 2016) > why3 --version Why3 platform, version 0.85 > alt-ergo -version 0.99.1 > frama-c -wp-help Plug-in name: WP Plug-in shortname: wp Description: Weakest Precondition Calculus WP 0.9 for Magnesium-20151002 ... > frama-c -wp -wp-prover coq lemma_ptr_inc.c [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing lemma_ptr_inc.c (with preprocessing) [wp] 1 goal scheduled [wp] [Coq] Compiling 'Compound.v'. [wp] [Coq] Goal typed_lemma_ptr_inc : Unknown [wp] Proved goals: 0 / 1 Coq: 0 (unknown: 1) -- Patrick. Le 08/03/2016 19:19, Pablo M. S. Farias a écrit : > 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/ > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss