Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000716Frama-CKernelpublic2011-02-12 08:232014-02-12 16:54
Reporterregehr 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000716: crash from r11865
DescriptionSeen on Ubuntu 10.10 on x86.

regehr@home:~/tmp/3$ ~/z/frama-c/bin/toplevel.opt -val -slevel 1 foo_pp.c
[kernel] preprocessing with "gcc -C -E -I. foo_pp.c"
[kernel] The full backtrace is:
         Called from file "list.ml", line 57, characters 20-23
         Called from file "cil/src/frontc/cabs2cil.ml", line 1176, characters 16-47
         Called from file "cil/src/frontc/cabs2cil.ml", line 5778, characters 23-40
         Called from file "cil/src/frontc/cabs2cil.ml", line 5756, characters 16-50
         Called from file "cil/src/frontc/cabs2cil.ml", line 4967, characters 14-349
         Called from file "cil/src/frontc/cabs2cil.ml", line 5102, characters 16-53
         Called from file "cil/src/frontc/cabs2cil.ml", line 5096, characters 32-55
         Called from file "cil/src/frontc/cabs2cil.ml", line 5122, characters 29-58
         Called from file "cil/src/frontc/cabs2cil.ml", line 5102, characters 16-53
         Called from file "cil/src/frontc/cabs2cil.ml", line 5122, characters 29-58
         Called from file "cil/src/frontc/cabs2cil.ml", line 5727, characters 27-64
         Called from file "cil/src/frontc/cabs2cil.ml", line 5823, characters 11-40
         Called from file "cil/src/frontc/cabs2cil.ml", line 7463, characters 8-69
         Called from file "cil/src/frontc/cabs2cil.ml", line 7335, characters 25-48
         Called from file "list.ml", line 74, characters 24-34
         Called from file "cil/src/frontc/cabs2cil.ml", line 7324, characters 9-1023
         Called from file "cil/src/frontc/cabs2cil.ml", line 7448, characters 16-34
         Called from file "cil/src/frontc/cabs2cil.ml", line 7460, characters 18-42
         Called from file "cil/src/frontc/cabs2cil.ml", line 7335, characters 25-48
         Called from file "list.ml", line 74, characters 24-34
         Called from file "cil/src/frontc/cabs2cil.ml", line 7324, characters 9-1023
         Called from file "cil/src/frontc/cabs2cil.ml", line 7017, characters 14-321
         Called from file "cil/src/frontc/cabs2cil.ml", line 7874, characters 12-31
         Called from file "list.ml", line 69, characters 12-15
         Called from file "cil/src/frontc/cabs2cil.ml", line 7905, characters 2-26
         Called from file "cil/src/frontc/frontc.ml", line 43, characters 19-22
         Called from file "src/kernel/file.ml", line 651, characters 27-46
         Called from file "src/kernel/file.ml", line 698, characters 16-23
         Called from file "list.ml", line 74, characters 24-34
         Called from file "src/kernel/file.ml", line 695, characters 6-318
         Called from file "src/kernel/file.ml", line 1177, characters 12-30
         Called from file "src/kernel/file.ml", line 1265, characters 4-27
         Called from file "src/kernel/ast.ml", line 59, characters 2-28
         Called from file "src/kernel/ast.ml", line 66, characters 53-71
         Called from file "src/kernel/globals.ml", line 489, characters 2-16
         Called from file "src/value/eval.ml", line 5407, characters 22-44
         Re-raised at file "src/value/eval.ml", line 5424, characters 47-50
         Called from file "src/project/state_builder.ml", line 1025, characters 2-6
         Re-raised at file "src/project/state_builder.ml", line 1029, characters 8-11
         Called from file "src/value/register.ml", line 59, characters 4-24
         Called from file "queue.ml", line 134, characters 6-20
         Called from file "src/kernel/boot.ml", line 36, characters 4-20
         Called from file "src/kernel/cmdline.ml", line 713, characters 2-9
         Called from file "src/kernel/cmdline.ml", line 195, characters 4-8
         
         Unexpected error (File "cil/src/frontc/cabs2cil.ml", line 1173, characters 17-23: Assertion failed).
         Please report as 'crash' at http://bts.frama-c.com/ [^]
         Note that 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 [^]
Additional InformationThis is a front-end bug as it occurs without the -val option (bin/toplevel.opt ~/Downloads/foo_pp.c ).

Workaround: if this bug happens too often and causes wasted time, use option -no-allow-duplication to circumvent it.

This is where we regret to have forked CIL. It was unavoidable, but we'll have to check if the bug appears in original CIL too and report it there if it does.
TagsNo tags attached.
Attached Filesc file icon foo_pp.c [^] (61,730 bytes) 2011-02-12 08:23 [Show Content]
c file icon red716.c [^] (180 bytes) 2011-02-12 14:34 [Show Content]

- Relationships

-  Notes
(0001479)
pascal (reporter)
2011-02-12 14:36

Virgile: file red716.c contains a reduced version of foo_pp.c. The error is at line 6.

bin/toplevel.byte red716.c

[kernel] error occurring when exiting Frama-C: stopping exit procedure.
         The full backtrace is:
         Raised at file "cil/src/frontc/cabs2cil.ml", line 1183, characters 7-9
         Called from file "list.ml", line 57, characters 20-23
         Called from file "cil/src/frontc/cabs2cil.ml", line 1186, characters 16-47
         Called from file "cil/src/frontc/cabs2cil.ml", line 5788, characters 23-40
         Called from file "cil/src/frontc/cabs2cil.ml", line 4977, characters 14-349
         Called from file "cil/src/frontc/cabs2cil.ml", line 4856, characters 14-75
         Called from file "cil/src/frontc/cabs2cil.ml", line 5846, characters 20-48
         Called from file "cil/src/frontc/cabs2cil.ml", line 7440, characters 28-61
         Re-raised at file "cil/src/frontc/cabs2cil.ml", line 7824, characters 28-98
         Called from file "cil/src/frontc/cabs2cil.ml", line 7345, characters 25-48
         Called from file "list.ml", line 74, characters 24-34
         Called from file "cil/src/frontc/cabs2cil.ml", line 7334, characters 9-3225
         Called from file "cil/src/frontc/cabs2cil.ml", line 7027, characters 14-321
         Called from file "cil/src/frontc/cabs2cil.ml", line 7884, characters 12-31
         Called from file "list.ml", line 69, characters 12-15
         Called from file "cil/src/frontc/cabs2cil.ml", line 7915, characters 2-26
         Called from file "cil/src/frontc/frontc.ml", line 260, characters 14-54
         Called from file "src/kernel/file.ml", line 651, characters 27-46
         Called from file "src/kernel/file.ml", line 698, characters 16-23
         Re-raised at file "src/kernel/file.ml", line 685, characters 16-55
         Called from file "list.ml", line 74, characters 24-34
         Called from file "src/kernel/file.ml", line 695, characters 6-318
         Called from file "src/kernel/file.ml", line 1177, characters 12-30
         Called from file "src/kernel/file.ml", line 1265, characters 4-27
         Re-raised at file "src/kernel/file.ml", line 1232, characters 2-92
         Called from file "src/kernel/ast.ml", line 59, characters 2-28
         Called from file "src/kernel/ast.ml", line 66, characters 53-71
         Called from file "queue.ml", line 134, characters 6-20
         Called from file "src/kernel/cmdline.ml", line 169, characters 6-23
         
         Unexpected error (File "cil/src/frontc/cabs2cil.ml", line 1174, characters 7-13: Assertion failed).
         Please report as 'crash' at http://bts.frama-c.com/ [^]
         Note that 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 [^]
(0001804)
virgile (developer)
2011-04-21 10:23

rev 12293 indeed fixed the issue

- Issue History
Date Modified Username Field Change
2011-02-12 08:23 regehr New Issue
2011-02-12 08:23 regehr Status new => assigned
2011-02-12 08:23 regehr Assigned To => pascal
2011-02-12 08:23 regehr File Added: foo_pp.c
2011-02-12 11:29 pascal Assigned To pascal => virgile
2011-02-12 11:29 pascal Category Plug-in > value analysis => Kernel
2011-02-12 11:29 pascal Additional Information Updated
2011-02-12 14:34 pascal File Added: red716.c
2011-02-12 14:36 pascal Note Added: 0001479
2011-03-11 19:27 svn Checkin
2011-04-21 10:23 virgile Note Added: 0001804
2011-04-21 10:23 virgile Status assigned => resolved
2011-04-21 10:23 virgile Fixed in Version => Frama-C GIT, precise the release id
2011-04-21 10:23 virgile Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version Frama-C GIT, precise the release id => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker