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] How to use the frama-c builtins programmatically?
- Subject: [Frama-c-discuss] How to use the frama-c builtins programmatically?
- From: virgile.prevosto at m4x.org (Virgile Prevosto)
- Date: Mon, 2 Sep 2013 10:48:24 +0200
- In-reply-to: <CAA1cxuix8sh_fqiVVNC24diwtjNqzRYgGbawnT8KkVF_16Qdzg@mail.gmail.com>
- References: <CAA1cxuix8sh_fqiVVNC24diwtjNqzRYgGbawnT8KkVF_16Qdzg@mail.gmail.com>
Hello David, 2013/9/2 David Yang <abiao.yang at gmail.com>: > I would like to use frama-c builtin functions programmatically. Frama-c has > builtin-functions that can make the value analysis more precise. > > I can use the following command to analysis a partial application: > > frama-c -lib-entry -main func file.c > /usr/local/share/frama-c/libc/fc_runtime.c > > Cil.add_special_builtin string... > Db.Value.register_builtin string... (-val-builtin options) > Cil.Frama_c_builtins.add ... > I think there is some misunderstanding here. When you add /usr/local/share/frama-c/libc/fc_runtime.c to the list of source files to consider, all C implementations present in this file will be treated as C functions to be analyzed, exactly that the functions that are defined in file.c Value analysis built-in mechanism allows to replace the normal analysis of a C function by a call to an OCaml function which operates directly to the internal states of Value analysis, simulating the behavior of the corresponding C function. These two behaviors are completely different. What are you trying to achieve? Best regards, -- E tutto per oggi, a la prossima volta Virgile
- References:
- [Frama-c-discuss] How to use the frama-c builtins programmatically?
- From: abiao.yang at gmail.com (David Yang)
- [Frama-c-discuss] How to use the frama-c builtins programmatically?
- Prev by Date: [Frama-c-discuss] How to use the frama-c builtins programmatically?
- Next by Date: [Frama-c-discuss] Proving a simple property on bitshift with WP
- Previous by thread: [Frama-c-discuss] How to use the frama-c builtins programmatically?
- Next by thread: [Frama-c-discuss] Proving a simple property on bitshift with WP
- Index(es):