--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on February 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] multiple behaviors in statement contracts



Hi all,

I have a question on statement contracts. Am I correct in that a statement contract can 
only be applied to one specific behavior, but not multiple ones? I would like 
to write a local contract on a statement, but the contract should be different
for different behaviors, something like this:

/*@ behavior nominal:
       assumes ...
       ....
  @ behavior non_nominal:
       assumes ...
void foo (...)
{

...

for nominal:
    \requires ...
    \ensures ...

for non_nominal:
    \requires ...
    \ensures ...
{
/*code block the local contract applies to*/
}

...

}

My reading of the grammar is that this is currently impossible. Is there any easy way around
that?

Thanks in advance,

Romain Jobredeaux