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