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 <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
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 - 2019 MantisBT Team
Powered by Mantis Bugtracker