Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

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