--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on January 2014 ---
> > /*@ > 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