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

  • Subject: [Frama-c-discuss] Unhelpful error message when missing "assigns" clause
  • From: jaseg at physik.tu-berlin.de (Sebastian Götte)
  • Date: Thu, 13 Dec 2018 15:30:21 +0900
Hi,

just in case someone else hits upon that problem:

I just got stuck at frama-c erroring out parsing a complex file with:
> 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.

Best regards,
Sebastian