--- layout: fc_discuss_archives title: Message 96 from Frama-C-discuss on October 2013 ---
While adding the frama-c builtins file: /usr/local/share/frama-c/libc/fc_runtime.c for the pre-processed source file (*.i), errors might come up like this because of these declaration is incompatible with the system header files: "user error: Incompatible declaration for ***". After slightly change some code in the corresponding source file in libc folder, it works. For example, adding some elements for the struct __fc_FILE in /usr/local/share/frama-c/libc/stdio.h I have three files in the folder "../share/frama-c/libc" that have been modified in order to be consistent with pre-processed file. HTH. Yibiao Yang On 16 October 2013 16:24, Yibiao Yang <cs.yang.yibiao at gmail.com> wrote: > > 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 -------------- A non-text attachment was scrubbed... Name: setjmp.h Type: text/x-chdr Size: 1872 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131030/ecc2c303/attachment.h> -------------- next part -------------- A non-text attachment was scrubbed... Name: stdio.h Type: text/x-chdr Size: 10060 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131030/ecc2c303/attachment-0001.h> -------------- next part -------------- A non-text attachment was scrubbed... Name: time.h Type: text/x-chdr Size: 3990 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131030/ecc2c303/attachment-0002.h>