--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on February 2014 ---
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