--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on May 2014 ---
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) -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140527/17dae68d/attachment-0001.html>