--- layout: fc_discuss_archives title: Message 67 from Frama-C-discuss on October 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] \strlen



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>