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

[Frama-c-discuss] Kernel functions



On Mon, 2012-02-20 at 15:33 +0100, Virgile Prevosto wrote:
> will do what you want. As Julien said, vspec is probably the good
> place to start anyway if you're operating on the spec alone.

I add preconditions based on the formals, so I better work with vfunc.

Anyway, really good documentation is needed to understand all this. But
why not convert set_spec to a method, so set_spec can extract the right
kf by itself and properly handle the action, based on self#behavior?

> > For an inplace visitor, what should be used instead of
> > File.create_project_from_visitor?
> >
> 
> Visitor.visitFramacFile or Visitor.visitFramacFileSameGlobals

This brings up another problem: how do I get the Cil_types.file? It
doesn't work with Cil.dummyFile. 
-- 
Best regards,
Boris