--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on March 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Having Trouble Verifying a Simple Pointer Increment



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>