--- layout: fc_discuss_archives title: Message 67 from Frama-C-discuss on October 2008 ---
Is \strlen supported in the current version of Frama-C? When I use it in an annotation, I get the error: "illegal escape sequence \strlen" (see below). Also, does \valid_range(p,0,\strlen(p)) always hold? I.e., assuming \valid_range(p,0,j) holds when j < 0, does \strlen(p) >= 0 guarantee \valid_range(p,0,\strlen(p))? Thanks, Chris <code filename="strcat.c"> /*@ requires \strlen(dest) >= 0; @ requires \strlen(src) >= 0; @ requires \valid_range(dest,0,\strlen(dest) + \strlen(src)); */ char *strcat(char * dest, const char *src) { char *ret = dest; while( *dest ) { dest++; } while( *dest++ = *src++ ); return ret; } </code> <shell> $ frama-c strcat.c [preprocessing] running gcc -C -E -I. strcat.c File "strcat.c", line 1, characters 10-17: lexical error, illegal escape sequence \strlen Warning: ignoring logical annotation. Parsing Cleaning unused parts Symbolic link Starting semantical analysis </shell>