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] Plugin development: Modifying a contract

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