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