--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on January 2014 ---
Hello Nichol, > the assertion at the end me thinks is plain wrong - s was modified and actually > is now pointing right at \0 so it should be > > //@ assert *s == '\0'; > > not > > //@ assert s[i] == '\0'; Thanks for pointing out that error. I noticed it later.? And now I added the preconditions too: #define EOS '\0' /*@ predicate valid_string{L}(signed char *s) = ? @?? 0 <= strlen(s) && \valid(s+(0..strlen(s))); ? @ ? @ predicate valid_string_or_null{L}(signed char *s) = ? @?? s == \null || valid_string(s); ? @*/ /*@ ??? requires valid_string_or_null(s); ??? requires s==NULL || s == EOS || *(s+strlen(s))==EOS; assigns \result; ...... */ ? But I am still stuck somewhere.? Z3 and CVC3 struggles with the last two goals: [wp] [Z3] Goal typed_szos_strlen_post : Timeout (Qed:4ms) (10s) [wp] [Z3] Goal typed_szos_strlen_assert : Timeout ? ? the version I am using is : WP 0.7 for Fluorine-20130401 cheers, xiaolei > > just kicked in your example + the fixed assertion > > root at debian:/home/hofrat/frama-c# frama-c -wp -wp-out /tmp/ -wp-prover z3 str_len.c > [kernel] preprocessing with "gcc -C -E -I. str_len.c" > str_len.c:8:[kernel] warning: parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead. > [wp] Running WP plugin... > [wp] Collecting axiomatic usage > [wp] warning: Missing RTE guards > [wp] 18 goals scheduled > [wp] [Qed] Goal typed_strlen_loop_inv_preserved : Valid > [wp] [Qed] Goal typed_strlen_loop_inv_established : Valid > [wp] [Qed] Goal typed_strlen_loop_inv_2_preserved : Valid > [wp] [Qed] Goal typed_strlen_loop_inv_2_established : Valid > [wp] [Qed] Goal typed_strlen_loop_inv_3_preserved : Valid > [wp] [Qed] Goal typed_strlen_loop_inv_3_established : Valid > [wp] [Z3] Goal typed_strlen_post : Failed > Error: Why3 exits with status [127] > [wp] [Qed] Goal typed_strlen_loop_inv_4_preserved : Valid > [wp] [Qed] Goal typed_strlen_loop_inv_4_established : Valid (4ms) > [wp] [Qed] Goal typed_strlen_loop_inv_5_preserved : Valid > [wp] [Qed] Goal typed_strlen_loop_inv_5_established : Valid > [wp] [Qed] Goal typed_strlen_assert : Valid > [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 > [wp] [Qed] Goal typed_strlen_assign_part4 : Valid > [wp] [Qed] Goal typed_strlen_assign_part5 : Valid > > quite a different result I would say ? - what versions are you using ? > > hofrat