Frama-C Bug Tracking System - Frama-C
View Issue Details
0001901Frama-CKernelpublic2014-07-30 10:252015-03-17 22:18
bb 
virgile 
normalcrashalways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Sodium 
0001901: Crash when merging contracts for duplicated functions with different formal parameters names
frama-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
monstrdup.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; }
when 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) { ... }
No tags attached.
Issue History
2014-07-30 10:25bbNew Issue
2014-08-04 15:45signolesAssigned To => virgile
2014-08-04 15:45signolesStatusnew => assigned
2014-08-19 18:42virgileNote Added: 0005408
2014-08-19 18:42virgileStatusassigned => confirmed
2014-08-26 17:45virgileNote Added: 0005414
2014-08-26 17:45virgileStatusconfirmed => resolved
2014-08-26 17:45virgileResolutionopen => fixed
2015-03-17 22:17signolesFixed in Version => Frama-C Sodium
2015-03-17 22:18signolesStatusresolved => closed

Notes
(0005408)
virgile   
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   
2014-08-26 17:45   
Fix committed to master branch.