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

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>