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] Unhelpful error message when missing "assigns" clause

Le jeu. 13 déc. 2018 à 07:36, Sebastian Götte <jaseg at physik.tu-berlin.de> a
écrit :

>
> > dev~/r/l/src <3 frama-c -wp test.c
> > [kernel] Parsing test.c (with preprocessing)
> > [...]
> > [kernel:annot:missing-spec] test.c:6: Warning:
> >   Neither code nor specification for function frob, generating default
> assigns from the prototype
> > [...]
> > [wp] test.c:7: User Error: Invalid infinite range null+(0..)
> > [kernel] Plug-in wp aborted: invalid user input.
>
> test.c demonstrating the issue:
> > // assigns \nothing;
> > int frob(void *state);
> >
> > //@ assigns \nothing;
> > void foo(void) {
> >     frob(0);
> > }
>
> It turned out the "Invalid infinite range" error is caused by the missing
> assigns specification. Change the "//" in the testcase into "//@" and it
> works. As I'm still new to frama-c, I have no idea *why* the missing spec
> causes this error, please educate me if you know. It would have been
> helpful in any case if the error message contained some indication of the
> source of that error, since it took me a while to track down.
>
>
You right that the error message is indeed confusing. The issue comes from
the generated assigns clause that is supplied by the kernel when there
isn't one in the first place (as is the case of frob here). When there is a
pointer parameter p to a non-const base type, the kernel considers that
 the corresponding memory location might be modified by the function, and
puts *p in the generated assigns clause. Now, it appears that, in the
special case of a pointer to void or to char, the kernel tries to be a
little smarter than that, and says the whole range p[0 .. ] might be
assigned. Apparently, WP is not too keen on such locations, especially for
a call where the actual argument is NULL, i.e. where none of the locations
involved are valid: if you have a call frob(p), the infinite range is
merely a warning. On the other hand, if you write by hand `assigns ((char
*)state)[0 .. ];`, you'll have the same error. However, I suspect that such
handwritten contract is quite rare, as usually a void * is accompanied by a
size_t argument giving the length of the block and the assigns would become
`assigns ((char *)state[ 0 .. (length  - 1)];`

Note that in any case, there is absolutely no guarantee that the generated
assigns clause is correct.  You might want to treat annot:missing-spec as
an error (i.e. use -kernel-warn-key annot:missing-spec=abort) in order to
spot as early as possible the cases where you're missing an assigns.
Assigns are generated only on a by-need basis, so that making the warning
an error won't force you to write assigns clauses for functions that are
not involved in the part of the code you're currently trying to analyze.

Best regards,
--
E tutto per oggi, a la prossima volta
Virgile
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181213/b6cb7b36/attachment.html>