2021-02-27 11:35 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000584Frama-CPlug-in > jessiepublic2010-12-17 19:35
Assigned Tocmarche 
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000584: incorrect(?) jessie code generated from strcpy
DescriptionThe following code:

#include <string.h>

char *c_strcpy (char *dest, const char *src)
  return strcpy (dest, src);
// END

causes the following diagnostics:

$ frama-c -cpp-extra-args=-I`frama-c -print-path`/libc -jessie first.c
[kernel] preprocessing with "gcc -C -E -I. -I/usr/share/frama-c/libc -dD first.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir first.jessie
[jessie] File first.jessie/first.jc written.
[jessie] File first.jessie/first.cloc written.
[jessie] Calling Jessie tool in subdir first.jessie
File "first.jc", line 352, characters 22-39: typing error: label `Here' not found
[jessie] user error: Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs first.cloc first.jc
// END

Generated .jc file attached.
Additional Information$ frama-c -v
Version: Boron-20100401
Compilation date: Fri Jul 16 12:28:04 UTC 2010
Share path: /usr/share/frama-c (may be overridden with FRAMAC_SHARE variable)
Library path: /usr/lib/frama-c (may be overridden with FRAMAC_LIB variable)
Plug-in paths: /usr/lib/frama-c/plugins (may be overridden with FRAMAC_PLUGIN variable)

$ uname -a
Linux osiris 2.6.32-5-amd64 #1 SMP Wed Aug 25 13:59:41 UTC 2010 x86_64 GNU/Linux
TagsNo tags attached.
Attached Files
  • ? file icon first.jc (10,677 bytes) 2010-09-15 16:24




pascal (reporter)

This bug is known and partially fixed in the development version.

The first problem with

assigns dest[0..strlen(src)];

as written in the provided string.h is that strlen(src) is assumed to be shorthand for strlen{Here}(src) when it should be interpreted as strlen{Old}(src). This was fixed in the development version on 2010-06-10.

The second problem, that you will encounter if you circumvent the first one by writing strlen{Old}(src) explicitly, is the subject of bug report 502. http://bts.frama-c.com/view.php?id=502

While not exactly the same problem, I will mark this bug as a duplicate of that one.


pascal (reporter)

Last edited: 2010-09-15 23:05

Actually, I was overly pessimistic. You *can* circumvent the problem as in the following, and this is not a duplicate of bug report 502 but a duplicate of a verbal bug report that was fixed without being inserted in the BTS.

Tested with Boron 20100401 and Why 2.26, same command-line as yours.

#include <__fc_string_axiomatic.h>

/*@ requires \valid_range(dest,0,strlen(src)) && valid_string(src);
  @ assigns dest[0..strlen{Old}(src)];
  @ ensures strcmp(dest,src) == 0 && \result == dest;
  @ ensures \base_addr(\result) == \base_addr(dest);
extern char *strcpy(char *restrict dest, const char *restrict src);

char *c_strcpy (char *dest, const char *src)
  return strcpy (dest, src);


-Issue History
Date Modified Username Field Change
2010-09-15 16:24 pippijn New Issue
2010-09-15 16:24 pippijn Status new => assigned
2010-09-15 16:24 pippijn Assigned To => cmarche
2010-09-15 16:24 pippijn File Added: first.jc
2010-09-15 22:56 pascal Note Added: 0001142
2010-09-15 23:04 pascal Note Added: 0001143
2010-09-15 23:05 pascal Note Edited: 0001143
2010-09-15 23:06 pascal Status assigned => resolved
2010-09-15 23:06 pascal Resolution open => fixed
2010-12-10 15:46 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:35 signoles Status resolved => closed
+Issue History