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



Dear all,

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

However, I do not want to use all the builtin functions in this file:
/usr/local/share/frama-c/libc/fc_runtime.c.

I only want to use some of those frama-c builtin functions such as memset
and strlen.

I do not know how to set a function name to use the frama-c builtin
function programmatically.

There are seems some API functions that relevant to frama-c builtin
function.

Cil.add_special_builtin string...
Db.Value.register_builtin string... (-val-builtin options)
Cil.Frama_c_builtins.add ...

The "Cil.add_special_builtin" function seems to make no difference. But i
don't kown how to use the Db.Value.register_builtin function.

Any suggestions?

David.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130902/6dd8041e/attachment.html>