--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on December 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] ACSL annotation for making function calls



Hello,

Le 13/12/2013 09:09, Pariente Dillon a ?crit :
>> but  by right-click on the "y = bar1();" , I did not have the option
>> >"insert callees contract (all calls)"  in context menu.
> This feature is at least available in Frama-C v. Fluorine.

Xiao-Lei, you need to right-click on the "=" sign, otherwise this option 
does not appear.

Best regards,
david