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] [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