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

[Frama-c-discuss] How to specify the options when calling wp_compute?



This is done by assigning values to parameters of WP.
Use:  frama-c -journal-enable -wp -wp-proof z3 -wp-model Hoare ...
And have a look to the generated journal.
Typically :

let run () =
   ...
   Dynamic.Parameter.String.set "-wp-proof" "z3";
   Dynamic.Parameter.String.set "-wp-model" "Hoare";
   ...

Regards,
	L.


Le 2 nov. 11 ? 05:36, ??? a ?crit :

> Hi,
>
>    I find that some annotations cannot be proved with wp_compute  
> only, but they are proved in "Frama-C -wp" with some options such as  
> setting the model as Hoare or setting prover as Z3. I cannot find  
> how to specify the options when calling wp_compute. Can they be  
> specified?
>
>
> Best Wishes to You.
>
> _______________________________________________
> 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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20111102/c01ac33c/attachment.htm>