--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on December 2013 ---
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