Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 168
    • Issues 168
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #1357
Closed
Open
Issue created Oct 19, 2011 by Pascal Cuoq@pascal

Crash with multiple incompatible declarations

ID0000990: This issue was created automatically from Mantis Issue 990. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0000990 Frama-C Kernel public 2011-10-19 2014-02-12
Reporter pascal Assigned To virgile Resolution fixed
Priority normal Severity crash Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Nitrogen-20111001 Target Version - Fixed in Version Frama-C Oxygen-20120901

Description :

~/ppc/bzip2-1.0.6 $ cat f1.c char s[100];

void perror(const char *);

void f(void){ perror(s); } ~/ppc/bzip2-1.0.6 $ cat f2.c char *s;

void perror(const char *);

void g(void){ perror(s); } ~/ppc/bzip2-1.0.6 $ ~/ppc/bin/toplevel.opt f2.c f1.c [kernel] warning: cannot load 4 plug-ins (incompatible with Nitrogen-20111001+dev). Aorai; Obfuscator; Security_slicing; Wp [kernel] preprocessing with "gcc -C -E -I. f2.c" [kernel] preprocessing with "gcc -C -E -I. f1.c" f2.c:1:[kernel] warning: Incompatible declaration for s (included from f2.c). Previous was at f1.c:1 (include from f1.c) (different type constructors: char [100] vs. char *)] f1.c:6:[kernel] failure: typeOf: StartOf on a non-array [kernel] error occurring when exiting Frama-C: stopping exit procedure. The full backtrace is: Raised at file "src/kernel/log.ml", line 509, characters 30-31 Called from file "src/kernel/log.ml", line 503, characters 9-16 Re-raised at file "src/kernel/log.ml", line 506, characters 15-16 Called from file "cil/src/mergecil.ml", line 1643, characters 36-48 Called from file "cil/src/cil.ml", line 2256, characters 12-53 Called from file "cil/src/cil.ml", line 1489, characters 13-16 Called from file "cil/src/cil.ml", line 2395, characters 38-57 Called from file "cil/src/cil.ml", line 1489, characters 13-16 Called from file "cil/src/cil.ml", line 1534, characters 24-57 Called from file "cil/src/cil.ml", line 2380, characters 5-52 Called from file "cil/src/cil.ml", line 2506, characters 14-21 Called from file "cil/src/cil.ml", line 1466, characters 21-41 Called from file "cil/src/cil.ml", line 2424, characters 5-86 Called from file "cil/src/cil.ml", line 1489, characters 13-16 Called from file "cil/src/cil.ml", line 2558, characters 16-40 Called from file "cil/src/cil.ml", line 1466, characters 21-41 Called from file "cil/src/cil.ml", line 2771, characters 14-39 Called from file "cil/src/cil.ml", line 1466, characters 21-41 Called from file "cil/src/cil.ml", line 2746, characters 5-91 Called from file "cil/src/cil.ml", line 2822, characters 16-38 Called from file "cil/src/cil.ml", line 1489, characters 13-16 Called from file "cil/src/cil.ml", line 1534, characters 24-57 Called from file "cil/src/cil.ml", line 2816, characters 5-53 Called from file "cil/src/mergecil.ml", line 2181, characters 11-41 Called from file "list.ml", line 69, characters 12-15 Called from file "cil/src/mergecil.ml", line 2465, characters 2-38 Called from file "cil/src/mergecil.ml", line 2612, characters 22-36 Called from file "list.ml", line 69, characters 12-15 Called from file "cil/src/mergecil.ml", line 2612, characters 2-61 Called from file "src/kernel/file.ml", line 830, characters 20-56 Called from file "src/kernel/file.ml", line 1327, characters 12-30 Called from file "src/kernel/file.ml", line 1412, characters 4-27 Called from file "src/kernel/ast.ml", line 64, characters 2-28 Called from file "src/kernel/ast.ml", line 71, characters 53-71 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/cmdline.ml", line 174, characters 6-23

     Frama-C aborted because of internal error.
     Please report as 'crash' at http://bts.frama-c.com/.
     Your Frama-C version is Nitrogen-20111001+dev.
     Note that a version and a backtrace alone often does not have information
     to understand the bug. Guidelines for reporting bugs are at:
     http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines

~/ppc/bzip2-1.0.6 $

Additional Information :

I think it would be ok just to be stricter for multiple incompatible declarations.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking