Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000299Frama-CPlug-in > jessiepublic2009-10-21 18:152014-02-12 16:56
Reporterjschuhmacher 
Assigned Tocmarche 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in VersionFrama-C Carbon-20101202-beta2 
Summary0000299: Frama-C stops with unexpected failure (Ref. "norm.ml:1105:8")
DescriptionWhile trying to check a file from the Minix3 kernel frama-c stops with an unexpected failure. A log is attached.
TagsNo tags attached.
Attached Fileslog file icon jessie.log [^] (50,400 bytes) 2009-10-21 18:15
c file icon system.c [^] (25,114 bytes) 2010-01-06 15:20 [Show Content]

- Relationships

-  Notes
(0000513)
cmarche (developer)
2009-11-03 16:34

Cannot reproduce without the source file
(0000515)
signoles (manager)
2009-11-03 16:57

Please provide a reproducable example as minimal as possible.
(0000616)
jschuhmacher (reporter)
2010-01-06 15:21

Sorry, I don't know why it crashes. This error occurred as the result of the command:
frama-c -cpp-command "gcc -E -C -D_EM_WSIZE=4 -D_EM_PSIZE=4 -nostdinc -I<CHECKOUTDIR>/include -ICHECKOUTDIR/kernel/arch/i386/include -I." -jessie -jessie-atp alt-ergo -jessie-debug 10 system.c

I have now attached the file "system.c", but that is probably useless without the rest. The rest can be obtained by:
svn --username anonymous checkout https://gforge.cs.vu.nl/svn/minix/trunk/src@r4817 [^] CHECKOUTDIR

The logfile produced by Frama-C was attached.
(0001325)
cmarche (developer)
2010-12-16 17:40


Hopefully fixed by giving a better error message

- Issue History
Date Modified Username Field Change
2009-10-21 18:15 jschuhmacher New Issue
2009-10-21 18:15 jschuhmacher File Added: jessie.log
2009-10-22 13:15 signoles Status new => assigned
2009-10-22 13:15 signoles Assigned To => cmarche
2009-11-03 16:34 cmarche Note Added: 0000513
2009-11-03 16:34 cmarche Status assigned => resolved
2009-11-03 16:34 cmarche Resolution open => unable to reproduce
2009-11-03 16:57 signoles Note Added: 0000515
2009-11-03 16:57 signoles Status resolved => feedback
2009-11-03 16:57 signoles Resolution unable to reproduce => reopened
2010-01-06 15:20 jschuhmacher File Added: system.c
2010-01-06 15:21 jschuhmacher Note Added: 0000616
2010-12-16 17:40 cmarche Note Added: 0001325
2010-12-16 17:40 cmarche Status feedback => resolved
2010-12-16 17:40 cmarche Resolution reopened => fixed
2010-12-18 11:18 signoles Fixed in Version => Frama-C Carbon-20101202-beta2
2010-12-18 11:19 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker