Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000584Frama-CPlug-in > jessiepublic2010-09-15 16:242010-12-17 19:35
Reporterpippijn 
Assigned Tocmarche 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000584: incorrect(?) jessie code generated from strcpy
DescriptionThe following code: // BEGIN #include 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
TagsNo tags attached.
Attached Files? file icon first.jc [^] (10,677 bytes) 2010-09-15 16:24

- Relationships

-  Notes
(0001142)
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.
(0001143)
pascal (reporter)
2010-09-15 23:04
edited on: 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

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker