--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on November 2011 ---
Hello Maria, There is the -verify option of jessie command line (see jessie -help). frama-c -jessie -jessie-jc-opt="-verify max" should do the job (see jessie plugin manual). Regards, - Nicolas > Message du 07/11/11 10:10 > De : "Virgile Prevosto" > A : "Frama-C public discussion" > Copie ? : > Objet : Re: [Frama-c-discuss] Partial verification > > Hello David and Maria, > > On 06/11/2011 12:44, David MENTRE wrote: > > 2011/11/6 Christofi Maria: > >> but, I meant without using GUI. Is there any option to use with the command? > > > > Using a combination of -lib-entry and -main? Something like "frama-c > > -lib-entry -main max". > > > > -lib-entry run analysis for an incomplete application e.g. an API > > call. See the -main option to set the entry point name > > -main set to name the entry point for analysis. Use -lib-entry > > if this is not for a complete application. Defaults to > > main > > -lib-entry and -main won't help here. jessie performs a modular > analysis. Basically, each function is analyzed separately, independently > from the contexts in which it might be called starting from the entry > point of the program. The options you mention are mainly useful for a > global analysis (as performed e.g. by the value analysis plugin). > The only thing that Jessie could do (it does not as far I know) with > -main f and without -lib-entry would be to produce extra hypotheses in > proof obligations related to f stating that the globals have their > initial value when entering the function. > > Now back to the initial problem: there is no easy way to do that with > jessie outside of the GUI (and even that won't do exactly what you want: > the goals are still generated, the GUI just lets you choose to launch a > prover over them or not). A possibility would be to remove the functions > you don't want to consider, either through #ifdef or through a copy > visitor in Frama-C that would create a new project by erasing the > globals that you don't want. > > On the other hand, you can have a look at the WP plugin whose -wp-fct > option does exactly what you want. > > Best regards, > -- > E tutto per oggi, a la prossima volta > Virgile > > _______________________________________________ > 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 > Une messagerie gratuite, garantie ? vie et des services en plus, ?a vous tente ? Je cr?e ma bo?te mail www.laposte.net -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20111107/e98d864c/attachment.htm>