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

[Frama-c-discuss] How to use the frama-c builtins programmatically?



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