--- layout: fc_discuss_archives title: Message 34 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



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>