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

Since I am a beginner with Frama-C, could some more experienced user at 
least tell me whether I'm making some obvious mistake?

PS: By the way, replacing "n >= 0" with "n >= 1" didn't help, nor did 
adding "-wp-prover alt-ergo,z3,cvc4" (Z3 version 4.4.1, CVC4 version 
1.5-prerelease).

---
Pablo
http://lia.ufc.br/~pmsf/

Em 2016-03-08 11:15, Pablo M. S. Farias escreveu:
> 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/
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss