--- layout: fc_discuss_archives title: Message 7 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?



? 2013/9/2 16:56, frama-c-discuss-request at lists.gforge.inria.fr ??:
> 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?
Dear Virgile,

Thank you for replying me promptly.
I am trying to treat those C functions in fc_runtime.c to be analyzed.
I can ahieve this by codeing like this:

Kernel.Files.add "/usr/local/share/frama-c/libc/fc_runtime.c";

Thanks again.

David