Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001901Frama-CKernelpublic2014-07-30 10:252015-03-17 22:18
Reporterbb 
Assigned Tovirgile 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Sodium 
Summary0001901: Crash when merging contracts for duplicated functions with different formal parameters names
Descriptionframa-c monstrdup.c /usr/local/share/frama-c/libc/string.h /usr/local/share/frama-c/libc/string.c -cpp-extra-args='-I/usr/local/share/frama-c/libc/' -check produces preprocessing with "gcc -C -E -I. -I/usr/local/share/frama-c/libc/ monstrdup.c" [kernel] preprocessing with "gcc -C -E -I. -I/usr/local/share/frama-c/libc/ FRAMAC_SHARE/libc/string.h" [kernel] preprocessing with "gcc -C -E -I. -I/usr/local/share/frama-c/libc/ FRAMAC_SHARE/libc/string.c" FRAMAC_SHARE/libc/string.c:44:[kernel] warning: def'n of func strdup at FRAMAC_SHARE/libc/string.c:44 (sum 4631) conflicts with the one at monstrdup.c:4 (sum 2976051); keeping the one at monstrdup.c:4. monstrdup.c:4:[kernel] warning: found two contracts. Merging them FRAMAC_SHARE/libc/string.h:258:[kernel] failure: [AST Integrity Check] initial AST logic variable s (2504) is not declared [kernel] Current source was: FRAMAC_SHARE/libc/string.h:258 The full backtrace is: Raised at file "src/kernel/log.ml", line 524, characters 30-31 Called from file "src/kernel/log.ml", line 518, characters 9-16 Re-raised at file "src/kernel/log.ml", line 521, characters 15-16 Called from file "src/kernel/file.ml", line 393, characters 26-36 Called from file "cil/src/cil.ml", line 2014, characters 15-31 Called from file "cil/src/cil.ml", line 2311, characters 16-41 Called from file "cil/src/cil.ml", line 2029, characters 21-41 Called from file "cil/src/cil.ml", line 2302, characters 14-39 Called from file "cil/src/cil.ml", line 2029, characters 21-41 Called from file "cil/src/cil.ml", line 2168, characters 18-30 Called from file "cil/src/cil.ml", line 2029, characters 21-41 Called from file "cil/src/cil.ml", line 2145, characters 12-44 Called from file "cil/src/cil.ml", line 2029, characters 21-41 Called from file "cil/src/cil.ml", line 2141, characters 12-63 Called from file "cil/src/cil.ml", line 2053, characters 13-16 Called from file "cil/src/cil.ml", line 2535, characters 14-34 Called from file "cil/src/cil.ml", line 2029, characters 21-41 Called from file "cil/src/cil.ml", line 2523, characters 17-48 Called from file "cil/src/cil.ml", line 2029, characters 21-41 Called from file "cil/src/cil.ml", line 2517, characters 11-39 Called from file "cil/src/cil.ml", line 2029, characters 21-41 Called from file "cil/src/cil.ml", line 2053, characters 13-16 Called from file "cil/src/cil.ml", line 2696, characters 19-54 Called from file "cil/src/cil.ml", line 2029, characters 21-41 Called from file "cil/src/cil.ml", line 2053, characters 13-16 Called from file "cil/src/cil.ml", line 2719, characters 21-58 Called from file "cil/src/cil.ml", line 2029, characters 21-41 Called from file "cil/src/cil.ml", line 3502, characters 4-28 Called from file "cil/src/cil.ml", line 2053, characters 13-16 Called from file "cil/src/cil.ml", line 2098, characters 24-57 Called from file "cil/src/cil.ml", line 3469, characters 5-53 Called from file "cil/src/cil.ml", line 6090, characters 16-36 Called from file "list.ml", line 75, characters 12-15 Called from file "cil/src/cil.ml", line 5680, characters 3-30 Called from file "cil/src/cil.ml", line 6091, characters 2-420 Called from file "cil/src/cil.ml", line 2029, characters 21-41 Called from file "cil/src/cil.ml", line 6124, characters 7-84 Called from file "src/kernel/file.ml", line 1657, characters 36-147 Called from file "src/kernel/file.ml", line 2265, characters 4-27 Called from file "src/kernel/ast.ml", line 113, characters 2-28 Called from file "src/kernel/ast.ml", line 125, characters 53-71 Called from file "src/kernel/boot.ml", line 29, characters 6-20 Called from file "src/kernel/cmdline.ml", line 752, characters 2-9 Called from file "src/kernel/cmdline.ml", line 214, characters 4-8
Steps To Reproducemonstrdup.c contains : #include "string.h" #include "stdlib.h" char * strdup(const char *str) { if (str != NULL) { register char *copy = malloc(strlen(str) + 1); if (copy != NULL) return strcpy(copy, str); } return NULL; }
Additional Informationwhen using -print option instead of -check i get the following contract for strdup: /*@ requires valid_string_src: valid_string(str); requires valid_string_src: valid_string(s); ensures \valid(\result+(0 .. strlen(\old(str)))) ∧ strcmp(\result, \old(str)) ≡ 0; ensures \valid(\result+(0 .. strlen(\old(s)))) ∧ strcmp(\result, \old(s)) ≡ 0; assigns \nothing; */ char *strdup(char const *str) { ... }
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0005408)
virgile (developer)
2014-08-19 18:42

Presence of string.h explicitely on the command line seems to be necessary to trigger the issue (although it does not contain a definition of strdup, only a declaration)
(0005414)
virgile (developer)
2014-08-26 17:45

Fix committed to master branch.

- Issue History
Date Modified Username Field Change
2014-07-30 10:25 bb New Issue
2014-08-04 15:45 signoles Assigned To => virgile
2014-08-04 15:45 signoles Status new => assigned
2014-08-19 18:42 virgile Note Added: 0005408
2014-08-19 18:42 virgile Status assigned => confirmed
2014-08-26 17:45 virgile Note Added: 0005414
2014-08-26 17:45 virgile Status confirmed => resolved
2014-08-26 17:45 virgile Resolution open => fixed
2015-03-17 22:17 signoles Fixed in Version => Frama-C Sodium
2015-03-17 22:18 signoles Status resolved => closed


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker