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



>   
> /*@
>   loop assigns s;
>  */
>  while (*s++ !=((signed char) '\0'))
>  {
>     ;
>  }
>     This will discharge the following proof obligation:
> [wp] [Z3] Goal typed_strlen_loop_assign_part3.  
>   
>     But the post condition is still left unproved.

You cannot expect very much without a loop invariant ---
the only thing known after the loop right now is probably

  *(s - 1) == '\0'

(I haven't done C in a long time) if I remember correctly that
the ++ increments after the use in the expression...

Your postcondition probably does not follow from that alone...


Wolfram