--- layout: fc_discuss_archives title: Message 21 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



Dear David,

Thank you very much for this information.

I don't want to initialize those unused global variables.

I will going to optimize it by myself by removing those unused global
variables in a newly created project.

Thanks,

-david

On 11 January 2014 23:27, David MENTR? <dmentre at linux-france.org> wrote:
> 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
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss