Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] \strlen

  • Subject: [Frama-c-discuss] \strlen
  • From: cconway at cs.nyu.edu (Christopher L Conway)
  • Date: Thu Oct 16 23:01:13 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>