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] my first frama verification

Hi again,

On Fri, Aug 21, 2015 at 6:41 PM, David MENTRE <dmentre at linux-france.org>
wrote:

>
> What dead code are you seeing?  Everything in seq.c should
>> be important and useful.
>>
>
> It appears that -lib-entry option triggers a different behaviour in
> open-source Frama-C and TIS Analyzer for fopen() result. Without this
> option, I found no warning on your code (sz == 256, verification took 1min)
> and the dead code disappeared (I did not make an exhaustive review though).
>

I noticed the same thing (very different results with and without
-lib-entry), and investigated a bit further. As it turns out, Tim's body
for fopen is incompatible with the specification we provide in the standard
library.

FILE *fopen(char *path, char *mode)
{
    if(coinflip())
        return stdin;
    return NULL;
}

while the specification contains

  ensures \result==\null || (\subset(\result,&__fc_fopen[0 ..
__FC_FOPEN_MAX-1])) ;

stdin cannot be equal to a cell of __fc_fopen, so the only possible result
is NULL. This is visible in the final analysis, because the postcondition
of fopen gets an Unknown/orange status. This also explains the dead code we
observe, because the caller checks the return value of fopen and fails when
it is NULL.


So the body of fopen should be removed entirely. But wait! There is also a
slight mistake in Frama-C's specification for fopen. In stdio.h,

const FILE*  __p_fc_fopen = __fc_fopen;

should be replaced by

FILE* const __p_fc_fopen = __fc_fopen;

This makes no difference without option -lib-entry, but changes everything
when this option is set. In this case, the ensures clause becomes partially
inconsistent with the assigns clauses, and the only remaining possible
value for \result is again NULL...

Once the body of fopen is removed, there are two possible fixes here:
- removing option -lib-entry altogether. I'm not sure is it useful for this
analysis
- patching share/frama-c/libc/stdio.h as indicated

HTH,

-- 
Boris
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150826/8e56fdae/attachment-0001.html>