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