--- layout: fc_discuss_archives title: Message 117 from Frama-C-discuss on November 2013 ---
Hello Xiao-lei, 2013/11/20 Xiao-lei Cui <x_cui at hotmail.com>: > And for contracts for each function, I have only seen examples that shows > how to embed them along with the function body. are you suggesting put the > contract along with the function prototype in some header file(.h), rather > than put them in the .c file? Yes. If the same function f() is called several times, by putting the contract in the .h file you can use the same contract for both calls to f() (to prove other contracts) and for proving that f() indeed fulfils its contract. Do not forget that Frama-C only sees contracts. When you have a function f(), Frama-C only sees the contract of f(), not the body of f()[1]. If at a call point you have no contract for function f(), Frama-C/Jessie cannot do much. Best regards, david [1] This is a bit misleading. With Frama-C/Value, Value analysis do use the body of f() if this body is available. But for Jessie, my simplification is true.