--- layout: fc_discuss_archives title: Message 49 from Frama-C-discuss on February 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Plugin development: Modifying a contract



On Mon, 2012-02-13 at 09:23 +0100, Julien Signoles wrote:

> With Frama-C Nitrogen, Kernel_function.set_spec is what you need.

Are function contracts -- in contrast to assertions -- not queued?

Also, with respect to what Virgile wrote, I guess I must apply set_spec
to the new kf of the copy visitor.

As set_spec expects a function of type fundec -> fundec, I may write a
function that constructs a fundec by copying some fields and replacing
others. May I assume that spec_behavior is either empty or contains at
least the default behavior?
-- 
Best regards,
Boris