Crash when merging contracts for duplicated functions with different formal parameters names
ID0001901: This issue was created automatically from Mantis Issue 1901. Further discussion may take place here.
Id | Project | Category | View | Due Date | Updated |
---|---|---|---|---|---|
ID0001901 | Frama-C | Kernel | public | 2014-07-30 | 2015-03-17 |
Reporter | bb | Assigned To | virgile | Resolution | fixed |
Priority | normal | Severity | crash | Reproducibility | always |
Platform | - | OS | - | OS Version | - |
Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | Frama-C Sodium |
Description :
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
Additional Information :
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) { ... }
Steps To Reproduce :
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; }