--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on August 2015 ---
"Probably because slevel is too low. Try to increase it (-slevel option) to the value found in paysz." I'm not sure I understand. I already have the slevel set to 300 and my input buffer is at most 105 bytes long and the values of paysz are [0..69]. Is 300 insufficient for this analysis? On Mon, Aug 17, 2015 at 11:22 PM, David MENTRE <dmentre at linux-france.org> wrote: > Hello Tim, > > Le 18/08/2015 09:48, Tim Newsham a écrit : > >> ok = auth(buf,sz,& pay,& paysz); >> /*@ assert ok ⡠0 ⨠\initialized(pay+(0 .. paysz-1)); */ ; >> if (ok) { >> /*@ assert \initialized(pay+(0 .. paysz-1)); */ ; >> i = (unsigned int)0; >> while (i < paysz) { >> /*@ assert Value: initialisation: \initialized(pay+i); */ >> printf("%d\n",(int)*(pay + i)); >> i ++; >> } >> } >> >> here all the assertions are evaluated as valid except >> for the one before the printf. This is odd because the >> assertion above it says that pay[0..paysz-1] is valid >> and the value analysis knows that i is less than paysz >> at the printf. So why can't it discover that >> \initialized(pay+i) from \initialized(pay+(0..paysz-1)) ? >> > > Probably because slevel is too low. Try to increase it (-slevel option) to > the value found in paysz. > > In loops, by default Value analysis is only considering one possible path > (you have as many paths as turns in the loop) and thus applies the Widening > operator of Abstract Analysis theory which, most of the time, results in > (correct but) not precise enough values. > > I posted some explanation on slevel in June of last year: > > > http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2014-June/004493.html > > (apparently the mailing list archive mangled the UTF8 characters.) > > Best regards, > david > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > -- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150818/df30988f/attachment.html>