--- layout: fc_discuss_archives title: Message 53 from Frama-C-discuss on February 2012 ---
Hello, On 02/15/2012 07:28 AM, Boris Hollas wrote: > 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? There is only one contract by function. One way to combine an old contract with a new one is to use Logic_utils.merge_funspec. > Also, with respect to what Virgile wrote, I guess I must apply set_spec > to the new kf of the copy visitor. It should be possible, but it is probably easier to modify the funspec itself by overloading method 'vspec' of your visitor (or similar methods handling particular subparts of the contract) in order to change the old spec by the new one during the copy. > 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? I guess you mean 'funspec' instead of 'fundec'. If no plug-in changes what the kernel does, it contains the default behavior (when it is required). That should be the case for all the provided plug-ins. Hope this helps, Julien