Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] why3IDE interactive proof session popup

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.