--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on November 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie - behavior-specific loop invariants



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>