| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0000584 | Frama-C | Plug-in > jessie | public | 2010-09-15 16:24 | 2010-12-17 19:35 | ||||
| Reporter | pippijn | ||||||||
| Assigned To | cmarche | ||||||||
| Priority | normal | Severity | major | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Boron-20100401 | ||||||||
| Target Version | Fixed in Version | Frama-C Carbon-20101201-beta1 | |||||||
| Summary | 0000584: incorrect(?) jessie code generated from strcpy | ||||||||
| 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=-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 | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
pascal (reporter) 2010-09-15 22:56 |
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) 2010-09-15 23:04 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); } |
| Notes |
| 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 |