incorrect(?) jessie code generated from strcpy
ID0000584: This issue was created automatically from Mantis Issue 584. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000584 | Frama-C | Plug-in > jessie | public | 2010-09-15 | 2010-12-17 |
| Reporter | pippijn | Assigned To | cmarche | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Boron-20100401 | Target Version | - | Fixed in Version | Frama-C Carbon-20101201-beta1 |
Description :
The following code:
// BEGIN #include <string.h>
char *c_strcpy (char *dest, const char *src) { return strcpy (dest, src); } // END
causes the following diagnostics:
// BEGIN
$ frama-c -cpp-extra-args=-Iframa-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