--- layout: fc_discuss_archives title: Message 59 from Frama-C-discuss on October 2013 ---
Dear Pascal and Boris, Thank you very much for such amazing works on the Value analysis plugin. Here I would like to report a feature request for the Value analysis plugin. Value analysis will become time consuming while there are too many function calls. Sometimes users only want to get the Pdg or to perform intra-slicing a given function f. In this situation, they may not want to consider those functions that called by f. Therefore, I suggest to add an option: "-value-context-insensitive" for value analysis plugin to ignore those calls for the main function (mostly the main function is set by users). Maybe an alternative way to perform insensitive value analysis of a given function f is to use the specification instead of definition for all the functions that called by f. Therefore, we can first generate default contract for those functions by using the Annotations module, then we can set those function to use specification instead of definition by using "-val-use-spec" option. Maybe this is not the truly context-insensitive analysis. But by using this method, we can easy analysis the functions individually. I already implement this option for my own plugin, below is some code for this feature : (** generate default contract for a function *) let generate_default_funspec (funcname : string) = let emitter = Emitter.end_user in let kf = Globals.Functions.find_by_name funcname in let assigns = Cil_types.Writes (Infer_annotations.assigns_from_prototype kf) in let bhv = Cil.mk_behavior ~assigns () in Annotations.add_behaviors emitter kf [ bhv ]; let funspec = Annotations.funspec kf in Dynamic.Parameter.StringSet.add "-val-use-spec" funcname; ;; (** set context insensitive for value analysis *) let context_insensitive (fundec : Cil_types.fundec) = let callees = ... in (** all the functions called by fundec *) List.iter (fun funcname -> if not (Ast_info.is_frama_c_builtin funcname) then generate_default_funspec funcname; ) callees; !Db.Value.compute (); ;; Thank you very much for your consideration. Best regards, Yours sincerely, Yibiao Yang Department of computer science Nanjing University P.R. China -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131016/88329e46/attachment.html>