--- layout: fc_discuss_archives title: Message 96 from Frama-C-discuss on October 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [FEATURE REQUEST] Context insensitive for Value analysis plugin



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>