--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on November 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Partial verification



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>