--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on March 2016 ---
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