--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on January 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] some questions about the "-lib-entry -main " option while value analysis a partial application



Hello David,

2014-01-11 15:51, David Yang:
> 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?

With "-lib-entry", all global variables are in an unknown state. In 
other words, Value analysis does not know if they have been initialized 
or not.

Best regards,
david