Adding Code of missing functions in frama-c

问题:

Forgive my ignorance. I need to do calculate backward slices for a project. After some searching, I came across frama-c. I downloaded the package on my ubuntu system which got me Frama-c Version: Fluorine-20130601. I am trying to use it for the first time. When finding out the undefined functions in my project almost all library functions are undefined, even printf, scanf etc(Neither code nor specification for function printf). According to the tutorial, I have to add stubs for all the undefined functions. Do I really have to add code for every library function that I am using even printf? Please guide.

回答1:

You should update to Frama-C Phosphorus, which brings tons of improvements regarding Variadic functions. In particular, specifications are automatically generated for printf/scanf-like functions when they are called on a constant format string. For non-variadic functions, some basic implementations are available in the directory $FRAMA_C_INSTALL/share/libc/*.c (in recent releases of Frama-C).