Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Having Trouble Verifying a Simple Pointer Increment
  • From: pmsf at lia.ufc.br (Pablo M. S. Farias)
  • Date: Tue, 08 Mar 2016 11:15:38 -0300
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>