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