--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on February 2012 ---
Hello, some questions on kernel functions: - why doesn't method vfunc f = begin Foo.feedback "%a\n" Cil.d_funspec f.sspec; Cil.SkipChildren end give the same result as method vfunc _ = begin let kf = Extlib.the self#current_kf in let fs = Kernel_function.get_spec kf in Foo.feedback "%a\n" Cil.d_funspec fs; Cil.SkipChildren end (the former doesn't print anything, the latter shows the contract) - why does this not work in example 5.14.7: let kf = Extlib.the self#current_kf in Queue.add (fun () -> Annotations.add_assert kf stmt [Ast.self] assertion) self#get_filling_actions; (instead, using Cil.get_kernel_function works) - why are the fields of type kernel_function mutable (and also the fields of many other records)? -- Best regards, Boris -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120214/8b17a2ea/attachment.htm>