+ /*@
+ requires valid_read_string (str);
+ assigns \nothing;
+ ensures (\forall integer i; 0 <= i < \result ==> str[i] != '\0') &&
+ str[\result] == '\0';
+ */
+ size_t strlen (const char *str)
+ {
+ ...
+
+It would be possible to use this to prove a simple strlen
+implementation that just worked character by character.
+
+Unfortunately for the actual glibc function we hit another limitation
+of the WP plugin, called the Typed Memory Model.
+
+WP models memory as a set of cells, with a type attached to each cell.
+So a string for example is a set of char cells, each cell being typed
+as char. You cannot cast these cells to something like a word and try
+to do a proof over that. Simply a limitation which is well
+documented.
+
+So a proof of the glibc function eludes me.
+
+There is a set of open source licensed string functions with Frama-C
+proofs available:
+
+https://github.com/evdenis/verker
+
+and this is what the strlen function with proof looks like from that: