--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on September 2013 ---
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