--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on May 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Not proving when predicate



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>