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] Kernel functions

  • Subject: [Frama-c-discuss] Kernel functions
  • From: hollas at informatik.htw-dresden.de (Boris Hollas)
  • Date: Tue, 14 Feb 2012 08:28:36 +0100
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>