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