--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on March 2016 ---
Hello, all! I'm having trouble verifying a simple linear search program with pointers instead of indexing. I reduced the first problem to the file attached, which has simply this: /*@ lemma ptr_inc: \forall int n, *v, *p; n >= 0 ==> \valid_read(v + (0..n-1)) ==> v <= p < v+n ==> v <= p+1; */ What I wanted with this lemma was simply to say that incrementing pointer "p" does not invalidate "v <= p". Am I somehow mistaken? Running "frama-c-gui -wp lemma_ptr_inc.c" (Frama-C Magnesium-20151002) gives [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] [Alt-Ergo] Goal typed_lemma_ptr_inc : Unknown (53ms) [wp] Proved goals: 0 / 1 Alt-Ergo: 0 (unknown: 1) 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/850504ba/attachment.c>