--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on February 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Kernel functions



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>