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

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>