Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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>