--- layout: fc_discuss_archives title: Message 44 from Frama-C-discuss on April 2013 ---
Thanks for the bug report. Current status : 1. pointer comparison is actually missing in Why3 resources ; 2. pointer difference is incorrectly translated in WP ; 3. pointer comparison requires pointers to have the same base, which is actually missing in your loop invariant, but can be proved. 4. It seems that Alt-Ergo has some difficulties in guessing the final existential. An intermediate assertion with the witness solves the problem. I guess your axiomatic definitions are something like : /*@ axiomatic String { predicate Length_of_str_is(char * s,integer n) = 0 <= n && \valid( s + (0..n) ) && s[n] == 0 && \forall integer k ; 0 <= k < n ==> s[k] !=0 ; logic integer Length{L}(char *s) reads s[..] ; axiom Length_def : \forall char *s; \forall integer n; Length_of_str_is(s,n) ==> Length(s)==n ; } */ Things to be added for points 3 and 4 : loop invariant BASE and assertion END, below: /*@ requires \exists integer i; Length_of_str_is(s,i); assigns \nothing; ensures \exists integer i; Length_of_str_is(s,i) && \result == i; @*/ int strlen(const char *s) { const char *ss = s; /*@ loop invariant BASE: \base_addr(s) == \base_addr(ss) ; loop invariant RANGE: s <= ss <= s+Length(s); loop invariant ZERO: \forall integer i; 0 <= i < (ss-s) ==> s[i] != 0; loop assigns ss; loop variant Length(s) + (s-ss) ; @*/ while (*ss) ss++; /*@ assert END: Length_of_str_is(s,ss-s); */ return ss - s; } frama-c -wp addr.i -wp-par 1 [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] 14 goals scheduled [wp] [Alt-Ergo] Goal typed_strlen_post : Valid (Qed:1ms) (57ms) (32) [wp] [Qed] Goal typed_strlen_loop_inv_BASE_preserved : Valid (1ms) [wp] [Qed] Goal typed_strlen_loop_inv_BASE_established : Valid [wp] [Alt-Ergo] Goal typed_strlen_loop_inv_RANGE_preserved : Valid (Qed:2ms) (215ms) (57) [wp] [Alt-Ergo] Goal typed_strlen_loop_inv_RANGE_established : Valid (Qed:1ms) (103ms) (30) [wp] [Alt-Ergo] Goal typed_strlen_loop_inv_ZERO_preserved : Valid (Qed:1ms) (131ms) (44) [wp] [Qed] Goal typed_strlen_loop_inv_ZERO_established : Valid [wp] [Alt-Ergo] Goal typed_strlen_assert_END : Valid (Qed:1ms) (192ms) (55) [wp] [Qed] Goal typed_strlen_loop_assign : Valid [wp] [Qed] Goal typed_strlen_assign_part1 : Valid [wp] [Qed] Goal typed_strlen_assign_part2 : Valid [wp] [Qed] Goal typed_strlen_assign_part3 : Valid (1ms) [wp] [Qed] Goal typed_strlen_loop_term_decrease : Valid (1ms) [wp] [Alt-Ergo] Goal typed_strlen_loop_term_positive : Valid (Qed:2ms) (77ms) (39) Regards, L. Le 19 avr. 2013 ? 13:05, Cristiano Sousa a ?crit : > I'm very excited in finally having a new version of frama-c. > > Installation went smooth, and the first thing I did was checking POs of the project I'm currently am working on. > > The new memory model seems powerfull, sadly I cannot prove a simple function using alt-ergo (previously i could), and also cannot use why3 as it returns an error related to unbound variables: > > File "/Users/xxxxx/.frama-c-wp/typed/Axiomatic.why", line 16, characters 8-11: unused variable x_0 > > http://pastebin.com/JZHEskC5 > > > Error while reading file '../typed/strlen_Why3_ide.why': File "/Users/xxxxx/.frama-c-wp/project.session/../typed/strlen_Why3_ide.why", line 36, characters 4-11: Unbound symbol 'addr_le' > > http://pastebin.com/hxzBu0xw > > > function: http://pastebin.com/ahvWeYXh > > > -- > Regards, > Cristiano Sousa > _______________________________________________ > 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/20130419/b17f4084/attachment-0003.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: addr.i Type: application/octet-stream Size: 919 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130419/b17f4084/attachment-0002.obj> -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130419/b17f4084/attachment-0004.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: wp.patch Type: application/octet-stream Size: 8220 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130419/b17f4084/attachment-0003.obj> -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130419/b17f4084/attachment-0005.html>