Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] arbitrary buffers in analysis

On Thu, Aug 27, 2015 at 6:40 PM, Tim Newsham <tim.newsham at gmail.com> wrote:

> proves everything except the assertion
>>  /*@ assert \initialized(buf + (32..40)); */
>>
>> This is good because
>> - I'm not convinced it is a true assertion
>> -  /*@ assert \initialized(buf + (32..39)); */  is sufficient, and can be
>> proven
>>
>
> hrmm.. indeed.. this scares me because my previous analysis
> didnt catch this!
>

I looked into this and to my surprise frama-c's textual output
doesnt include a warning for this unverified assertion, but when
I loaded it up in the gui, it was clearly marked as yellow.  I had
previously assumed that no warnings in the output meant that
everything was good. Is there a way to force warnings in the
output for all unverified assertions?

Also thank you for the other email about the fopen issue.  I don't
> recall fopen reporting dead code in my model of fopen but I'll
> revisit the issue as I digest the ideas in your email further.
>

I verified that the sodium version isnt reporting any dead code
in my fopen model.  Perhaps it's unique to the newest version?

At any rate, I'm planning on retrying my tests in the latest version soon.

Once again, thank you for your feedback.. It's been very helpful.

-- 
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/20150827/912d2d60/attachment-0001.html>