--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on December 2018 ---
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