size_t strlen(const char *s) { const char *sc; /*@ loop invariant s <= sc <= s + strlen(s); loop invariant valid_str(sc); loop invariant strlen(s) == strlen(sc) + (sc - s); loop assigns sc; loop variant strlen(s) - (sc - s); */ for (sc = s; *sc != '\0'; ++sc) /* nothing */; return sc - s; }
Where is the /*@
comment for this function?
We’ll come to that in a minute ...
Proof by Denis Efremov, Ivannikov Institute for System Programming at the Russian Academy of Sciences, https://github.com/evdenis/verker/blob/master/src/strlen.c