| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0001099 | Frama-C | Kernel | public | 2012-02-18 15:40 | 2014-02-12 16:59 | ||||
| Reporter | yakobowski | ||||||||
| Assigned To | virgile | ||||||||
| Priority | low | Severity | crash | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Nitrogen-20111001 | ||||||||
| Target Version | Fixed in Version | Frama-C Oxygen-20120901 | |||||||
| Summary | 0001099: Crash when parsing an incorrect program with pointer to arrays | ||||||||
| Description | frama-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; } | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
signoles (manager) 2012-02-18 20:07 |
Please Boris, command line + backtrace? |
|
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 |
|
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 ... |
|
yakobowski (manager) 2012-02-19 10:36 |
The command-line was supposed to be clear enough with the correct summary :/ |
|
2014-02-12 16:59 |
Fix committed to stable/neon branch. |
| Notes |
| 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 | ||
| 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 |
| 2013-12-19 01:12 | Source_changeset_attached | => framac master aa940a73 | |
| 2014-02-12 16:54 | Source_changeset_attached | => framac stable/neon aa940a73 | |
| 2014-02-12 16:59 | Note Added: 0004723 | ||
| 2014-02-12 16:59 | Status | closed => resolved | |
| Issue History |