6xxx strlen and 9xxx conclusions.

[libguestfs-talks.git] / 2020-frama-c / 6400-strlen.html

diff --git a/2020-frama-c/6400-strlen.html b/2020-frama-c/6400-strlen.html
new file mode 100644 (file)
index 0000000..962f06b
--- /dev/null
+++ b/2020-frama-c/6400-strlen.html
@@ -0,0 +1,33 @@
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
+<link rel="stylesheet" href="style.css" type="text/css"/>
+<script src="code.js" type="text/javascript"></script>
+
+<h1>strlen proven, but not by me</h1>
+
+<pre class="code">
+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;
+}
+</pre>
+
+<p>
+Where is the <code>/*@</code> comment for this function?
+We’ll come to that in a minute ...
+</p>
+
+
+<p class="attribution">
+Proof by Denis Efremov, Ivannikov Institute for System Programming
+at the Russian Academy of Sciences,
+<a href="https://github.com/evdenis/verker/blob/master/src/strlen.c">https://github.com/evdenis/verker/blob/master/src/strlen.c</a>
+</p>