Tried implementing some basic string manipulation functions in #frama-c today. Specifically, strlcpy() and my own strlen(). Quite tricky. But I did learn one can take a gander at /usr/share/frama-c/libc/string.h to get some ideas for more ACSL to decorate one's contracts with. #langsec