--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on November 2010 ---
Hallo, I got a syntactical question about specifying behavior-specific loop invariants. Having specified different behaviors in the function contract I can relate to them by assigning the specific loop invariants by using "for <behavior>: loop invariant..;" This works fine if specification and implementation are located in the same file. As we usually divide spec. and impl. I experienced the following problem: Including the specification file to the implementation file results in some unknown behavior error. I simplified an example and attached it. It is just about the syntax, I am aware that the content of specification, especially the loop invariants make no sense at all. By running frama-c -jessie test.c the following error occurs: test.c:11:[kernel] user error: Error during annotations analysis: reference to unknown behavior one Is this a bug? Or is there something I overlooked? Kind Regards, Kerstin -------------- next part -------------- A non-text attachment was scrubbed... Name: test.c Type: application/octet-stream Size: 158 bytes Desc: test.c URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20101108/8472ef90/attachment.obj> -------------- next part -------------- A non-text attachment was scrubbed... Name: test.spec Type: application/octet-stream Size: 104 bytes Desc: test.spec URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20101108/8472ef90/attachment-0001.obj>