Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001099Frama-CKernelpublic2012-02-18 15:402014-02-12 16:59
Reporteryakobowski 
Assigned Tovirgile 
PrioritylowSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001099: Crash when parsing an incorrect program with pointer to arrays
Descriptionframa-c crashes on the following program typedef int t[10]; typedef int u[4]; void main () { int tab1[4]; u* p = &tab1; t* p2 = (t) p; }
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0002712)
signoles (manager)
2012-02-18 20:07

Please Boris, command line + backtrace?
(0002713)
pascal (reporter)
2012-02-18 20:18

It crashes when crashing. I think it's clear. SVN 17245 $ ppc/bin/toplevel.opt t.c [kernel] warning: cannot load 4 plug-ins (incompatible with Nitrogen-20111001+dev). Aorai; Obfuscator; Report; Security_slicing [kernel] preprocessing with "gcc -C -E -I. t.c" t.c:8:[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 528, characters 30-31 Called from file "src/kernel/log.ml", line 522, characters 9-16 Re-raised at file "src/kernel/log.ml", line 525, characters 15-16 Called from file "cil/src/mergecil.ml", line 1611, characters 36-48 Called from file "cil/src/cil.ml", line 2301, characters 12-53 Called from file "cil/src/cil.ml", line 2437, characters 38-44 Called from file "cil/src/cil.ml", line 1556, characters 13-16 Called from file "cil/src/cil.ml", line 1601, characters 24-57 Called from file "cil/src/cil.ml", line 2425, characters 5-52 Called from file "cil/src/cil.ml", line 2551, characters 14-21 Called from file "cil/src/cil.ml", line 1533, characters 21-41 Called from file "cil/src/cil.ml", line 2469, characters 5-86 Called from file "cil/src/cil.ml", line 1556, characters 13-16 Called from file "cil/src/cil.ml", line 2603, characters 16-40 Called from file "cil/src/cil.ml", line 1533, characters 21-41 Called from file "cil/src/cil.ml", line 2816, characters 14-39 Called from file "cil/src/cil.ml", line 1533, characters 21-41 Called from file "cil/src/cil.ml", line 2791, characters 5-91 Called from file "cil/src/cil.ml", line 2867, characters 16-38 Called from file "cil/src/cil.ml", line 1556, characters 13-16 Called from file "cil/src/cil.ml", line 1601, characters 24-57 Called from file "cil/src/cil.ml", line 2861, characters 5-53 Called from file "cil/src/mergecil.ml", line 2161, characters 11-41 Called from file "list.ml", line 69, characters 12-15 Called from file "cil/src/mergecil.ml", line 2445, characters 2-38 Called from file "cil/src/mergecil.ml", line 2674, characters 22-36 Called from file "list.ml", line 69, characters 12-15 Called from file "cil/src/mergecil.ml", line 2674, characters 2-61 Called from file "src/kernel/file.ml", line 842, characters 20-56 Called from file "src/kernel/file.ml", line 1339, characters 12-30 Called from file "src/kernel/file.ml", line 1439, characters 4-27 Called from file "src/kernel/ast.ml", line 70, characters 2-28 Called from file "src/kernel/ast.ml", line 79, 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
(0002714)
pascal (reporter)
2012-02-18 20:20

Note that t.c is not a well-formed C program and it's enough to reject it without crashing. $ gcc -Wall t.c t.c:5: warning: return type of ‘main’ is not ‘int’ t.c: In function ‘main’: t.c:8: error: cast specifies array type ...
(0002715)
yakobowski (manager)
2012-02-19 10:36

The command-line was supposed to be clear enough with the correct summary :/
(0004723)

2014-02-12 16:59

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2012-02-18 15:40 yakobowski New Issue
2012-02-18 20:07 signoles Note Added: 0002712
2012-02-18 20:18 pascal Note Added: 0002713
2012-02-18 20:20 pascal Note Added: 0002714
2012-02-19 10:36 yakobowski Note Added: 0002715
2012-02-19 10:36 yakobowski Summary Crash when crashing an incorrect program with pointer to arrays => Crash when parsing an incorrect program with pointer to arrays
2012-02-21 11:16 virgile Status new => assigned
2012-02-21 11:16 virgile Assigned To => virgile
2012-02-21 16:54 svn Checkin
2012-02-21 16:54 svn Status assigned => resolved
2012-02-21 16:54 svn Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2014-02-12 16:59 Note Added: 0004723
2014-02-12 16:59 Status closed => resolved


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker