--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on August 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] trouble debugging assertions



"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>