--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on April 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Re : Frama-c-discuss Digest, Vol 35, Issue 6



Hello!

We overrode vspec as you advised, and we didn't do vglob_aux, because we don't actually change the function body (yet) we just process the body of the function (with a self-made method) so we just call it with the fundec returned by the self#current_func.

We print the result with the cil.d_funspec, but we still don't get it on the outed file.

?method vspec spec=
??? begin match self#current_func with
????? |Some fdec? -> 
?????????? (*? extractCostFrom fdec.sbody.bstmts ; 
?????????? create a new spec with adding the spec_behavior : newSpecc
????????? *)

??? ?? Cil.d_funspec Format.std_formatter newSpecc ; (*prints well*)
??? ?? ChangeDoChildrenPost(newSpecc,fun x -> x) (*doesn't show*)
????? | _ -> JustCopy
??? end

So maybe it's a problem with the way we out the file, but we can't figure out where...
Here's what we do : 

let cost ((fname, _) as file, cost_id, cost_incr) =
(*(fname,_) is a Cabs.file that we passed to CerCo earlier, now we create a new project
with its name*)
? let annotatedFile =??? 
??? Parameters.Files.set [fname];
??? File.init_from_cmdline ();
??? File.create_project_from_visitor 
????? "cerCo_Annotated" 
????? (new cost cost_incr cost_id) 
?????????????????????? (*? inherits from? Visitor.generic_frama_c_visitor prj (Cil.copy_visit())? *)
? in 
??? Project.on
????? annotatedFile
?????? (fun _ ->
?????? Parameters.CodeOutput.set "tests/_out.c";
?????? File.pretty_ast ())
???? ();
annotatedFile

Thank you so much for your time.

H. Zakaria Chihani.



PS : here's to keep track ;)
Message: 6
Date: Mon, 11 Apr 2011 15:58:20 +0200
From: Virgile Prevosto <virgile.prevosto at cea.fr>
Subject: Re: [Frama-c-discuss] Difference between Kernel_function and
??? GFun node
To: frama-c-discuss at lists.gforge.inria.fr
Message-ID: <20110411155820.676d940a at is010235>
Content-Type: text/plain; charset=ISO-8859-1

Le lun. 11 avril 2011 10:46:38 CEST,
zakaria chihani <uaz11 at yahoo.fr> a ?crit :

> I can't understand the difference between the GFun node and the kernel_function. sspec can't be completely irrelevant, I presume.

Well, for most practical purposes, sspec is irrelevant. It is only used
in freshly type-checked AST, until Frama-C's internal tables are
properly filled. It's not a stage where plug-ins intervene much (in
fact, there isn't any hook to do so).

> The only thing changing is indeed the vspec, but it changes with regards to what is in the function itself, we need to process the body (with vglob_aux) in order to get "what to put" in the postcondition (with vspec). 

OK, then you're right, it makes sense to use vglob_aux to do that.

> 
> So we need to also override vglob_aux.
> The thing is, we don't know the specific order in which these two (vglob_aux and vspec) are gonna be called. 

the spec is somehow a child of the function, thus vspec is called after
vglob_aux (on the other hand, an action in ChangeDoChildrenPost for
vspec will be performed before an action in ChangeDoChildrenPost for
vglob_aux)

> Isn't there an easier way to use Visitor.current_kf and set_current_kf, to link the generated GFun node, with the associated kernel_function?

Unfortunately no: current_kf always refer to original function being
visited. In fact, since the visitor can return more than
one global (or for that matter, to turn a decl into def or vice-versa),
it is not really possible to have a current_kf for the new function in
the general case. Only the original one is meaningful.

-- 
Virgile Prevosto
Ing?nieur-Chercheur, CEA, LIST
Laboratoire de S?ret? des Logiciels
+33/0 1 69 08 82 98



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110414/143f7cb1/attachment.htm>