--- layout: fc_discuss_archives title: Message 34 from Frama-C-discuss on May 2014 ---
Well, its surprising. Could you set -wp-out <dir> option and compare the generated proof obligations in each case ? (Files of interest looks like "<dir>/**/opal_list_construct_post_*_Alt-Ergo.mlw ?) L. Le 27 mai 2014 ? 20:13, Ian Blissard <iblissard at grammatech.com> a ?crit : > I have a predicate, ?list_valid? which is a post condition for a function. WP is unable to prove the predicate, but if I copy the predicate definition as another post condition, it is able to prove it. Why would this be the case? > > /*@ > > predicate list_valid{L} (opal_list_t *list) = > > \valid(list) && list_loop(list) && list_linked(list) > > && valid_opal_list_item_t(&(list->opal_list_sentinel)) && item_linked(&(list->opal_list_sentinel)) > > && length(list, list->opal_list_sentinel.opal_list_next) == list->opal_list_length; > > */ > > /*@ > > requires \valid(list); > > assigns list->opal_list_sentinel, list->opal_list_length; > > ensures list_empty(list); > > > > ensures \valid(list) && list_loop(list) && list_linked(list) > > && valid_opal_list_item_t(&(list->opal_list_sentinel)) && item_linked(&(list->opal_list_sentinel)) > > && length(list, list->opal_list_sentinel.opal_list_next) == list->opal_list_length; > > > > ensures list_valid(list); > > ensures valid_opal_list_item_t(&(list->opal_list_sentinel)); > > */ > > static void opal_list_construct(opal_list_t *list) > > > > The relevant output when ran with ?wp ?val -wp-timeout 30 -wp-par 1 > > [wp] [Alt-Ergo] Goal typed_opal_list_construct_post : Valid (49ms) (26) > > [wp] [Alt-Ergo] Goal typed_opal_list_construct_post_2 : Valid (Qed:1ms) (2s) (221) > > [wp] [Alt-Ergo] Goal typed_opal_list_construct_post_3 : Unknown (Qed:1ms) (2s) > > [wp] [Alt-Ergo] Goal typed_opal_list_construct_post_4 : Valid (73ms) (41) > > [wp] [Alt-Ergo] Goal typed_opal_list_construct_assign_part1 : Valid (38ms) (28) > > [wp] [Alt-Ergo] Goal typed_opal_list_construct_assign_part2 : Valid (31ms) (28) > > [wp] [Alt-Ergo] Goal typed_opal_list_construct_assign_part3 : Valid (22ms) (18) > > > > _______________________________________________ > 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/20140528/60ce5187/attachment.html>