Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Not proving when predicate

  • Subject: [Frama-c-discuss] Not proving when predicate
  • From: iblissard at grammatech.com (Ian Blissard)
  • Date: Tue, 27 May 2014 14:13:20 -0400
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>