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



At this point I come up against another oddity:

  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)) ?


On Mon, Aug 17, 2015 at 9:39 PM, Tim Newsham <tim.newsham at gmail.com> wrote:

> ack, I apologize, I found it as "-val-split-return-auto"
> and that did fix the analysis.  Thank you!
>
> On Mon, Aug 17, 2015 at 9:22 PM, Tim Newsham <tim.newsham at gmail.com>
> wrote:
>
>> Thank you. I tried this but it rejected the argument and I
>> couldn't find any arguments with "split" in the name:
>>
>> $ frama-c --version
>> Version: Sodium-20150201
>> Compilation date: Tue Aug  4 10:08:25 HST 2015
>> Share path: /usr/local/share/frama-c (may be overridden with FRAMAC_SHARE
>> variable)
>> Library path: /usr/local/lib/frama-c (may be overridden with FRAMAC_LIB
>> variable)
>> Plug-in paths: /usr/local/lib/frama-c/plugins (may be overridden with
>> FRAMAC_PLUGIN variable)
>> $ frama-c -kernel-help|grep split
>> $
>>
>> is the name bad or do I need to be on a different version?
>>
>>
>> On Mon, Aug 17, 2015 at 8:57 PM, Anne Pacalet <anne.pacalet at free.fr>
>> wrote:
>>
>>> Hi Tim,
>>>
>>> Le 18/08/2015 08:44, Tim Newsham a écrit :
>>> > What is confusing me is that the assertion right after the call site
>>> is the
>>> > same (seems to me!) as the "ensures" clause of the implementation!  So
>>> why
>>> > is the analyzer not drawing the connection?  Is there something I can
>>> do to
>>> > help it out?
>>>
>>> I suspect that the states computed at the end of the function are merged
>>> before
>>> returning, so the assertion cannot be verified anymore on the merged
>>> state.
>>> Maybe you should try to use the option:
>>> -val-split-return auto
>>> or
>>> -val-split-return-function auth:full
>>>
>>> Hope this helps.
>>>
>>> Anne.
>>> _______________________________________________
>>> 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
>>
>
>
>
> --
> Tim Newsham | www.thenewsh.com/~newsham | @newshtwit |
> thenewsh.blogspot.com
>



-- 
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/20150817/52daa76f/attachment.html>