--- layout: fc_discuss_archives title: Message 55 from Frama-C-discuss on February 2012 ---
Hi, > If wp is dynamically called with code to prove the invariants it can > only be proved one by one. How to get the "VALID" results above? The command `frama-c-gui henry1.c -wp` will prove all of your invariants at once. Another solution is to call Frama-C programatically, ie: frama-c henry1.c -wp -then -report Then WP yields: [wp] [WP:simplified] Goal store_phase_loop_inv_established : Valid [wp] [WP:simplified] Goal store_phase_loop_inv_2_established : Valid [wp] [Alt-Ergo] Goal store_phase_loop_inv_preserved : Valid [wp] [Alt-Ergo] Goal store_phase_loop_inv_2_preserved : Valid and Report synthesizes: -------------------------------------------------------------------------------- --- Properties of Function 'phase' -------------------------------------------------------------------------------- [ Valid ] Invariant (file henry1.c, line 7) by WP-Store. [ Valid ] Invariant (file henry1.c, line 8) by WP-Store. -------------------------------------------------------------------------------- --- Status Report Summary -------------------------------------------------------------------------------- 2 Completely validated 2 Total -------------------------------------------------------------------------------- HTH, Florent. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120215/eb40cca6/attachment.htm> -------------- next part -------------- A non-text attachment was scrubbed... Name: florent_kirchner.vcf Type: text/x-vcard Size: 308 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120215/eb40cca6/attachment.vcf>