2020-frama-c/6400-strlen.html

   1 <meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
   2 <link rel="stylesheet" href="style.css" type="text/css"/>
   3 <script src="code.js" type="text/javascript"></script>
   4
   5 <h1>strlen proven, but not by me</h1>
   6
   7 <pre class="code">
   8 size_t strlen(const char *s)
   9 {
  10         const char *sc;
  11         /*@ loop invariant s <= sc <= s + strlen(s);
  12             loop invariant valid_str(sc);
  13             loop invariant strlen(s) == strlen(sc) + (sc - s);
  14             loop assigns sc;
  15             loop variant strlen(s) - (sc - s);
  16          */
  17         for (sc = s; *sc != '\0'; ++sc)
  18                 /* nothing */;
  19         return sc - s;
  20 }
  21 </pre>
  22
  23 <p>
  24 Where is the <code>/*@</code> comment for this function?
  25 We’ll come to that in a minute ...
  26 </p>
  27
  28
  29 <p class="attribution">
  30 Proof by Denis Efremov, Ivannikov Institute for System Programming
  31 at the Russian Academy of Sciences,
  32 <a href="https://github.com/evdenis/verker/blob/master/src/strlen.c">https://github.com/evdenis/verker/blob/master/src/strlen.c</a>
  33 </p>