--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on November 2011 ---
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>