--- layout: fc_discuss_archives title: Message 7 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



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