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] Re : Frama-c-discuss Digest, Vol 35, Issue 6

  • Subject: [Frama-c-discuss] Re : Frama-c-discuss Digest, Vol 35, Issue 6
  • From: uaz11 at yahoo.fr (zakaria chihani)
  • Date: Thu, 14 Apr 2011 12:04:35 +0100 (BST)
  • In-reply-to: <mailman.21779.1302561613.26568.frama-c-discuss@lists.gforge.inria.fr>
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>