--- layout: fc_discuss_archives title: Message 39 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



Hello,

2014-02-18 22:13 GMT+01:00 Jobredeaux, Romain J <jobredeaux at gatech.edu>:

> 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 ...

You're right, this is not possible. You can write several statement
contracts in sequence, like that:

/*@ behavior nominal: assumes x>=0;
    behavior non_nominal: assumes x < 0;
*/
int f(int x) {

  /*@ for nominal: ensures \true; */
  /*@ for non_nominal: ensures \true; */
  { return x; }

}

Note however that WP seems to ignore 'for behavior:' part of annotations.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile