--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on January 2014 ---
Dear all, In the value analysis manual "frama-c-value-analysis.pdf", I can find the introduction to "-lib-entry" option. What I want to know is while I am setting the "-lib-entry" option for analyzing a incomplete application (or a partial application): 1. Whether all the global variables will be initialized for the initial state ? whether those globals will be also initialized even if those variables are not used in the specified main function? 2. I am also using the -val-use-spec option for all the functions which called by the main function. there will be many global variables used in those called functions but might not used in the main function. whether those global variables also initialized for a initial stat? 3. I think the values of the initial state will propagate between those statements, so if the initial state is too large, whether it will largely influence the speed of value analysis? Thanks, -david