--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on January 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [wp] unproved goals for strlen() function



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