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] [FEATURE REQUEST] Context insensitive for Value analysis plugin

  • Subject: [Frama-c-discuss] [FEATURE REQUEST] Context insensitive for Value analysis plugin
  • From: cs.yang.yibiao at gmail.com (Yibiao Yang)
  • Date: Wed, 16 Oct 2013 16:24:53 +0100
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>