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] Jessie - behavior-specific loop invariants

  • Subject: [Frama-c-discuss] Jessie - behavior-specific loop invariants
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
  • Date: Mon, 8 Nov 2010 13:59:08 +0100
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>