Frama-C Bug Tracking System - Frama-C
View Issue Details
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.
Relationships
Attached Fileslog jessie.log (50,400) 2009-10-21 18:15
https://bts.frama-c.com/file_download.php?file_id=25&type=bug
c system.c (25,114) 2010-01-06 15:20
https://bts.frama-c.com/file_download.php?file_id=42&type=bug

Notes
(0000513)
cmarche   
2009-11-03 16:34   
Cannot reproduce without the source file
(0000515)
signoles   
2009-11-03 16:57   
Please provide a reproducable example as minimal as possible.
(0000616)
jschuhmacher   
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   
2010-12-16 17:40   

Hopefully fixed by giving a better error message

Issue History
Date ModifiedUsernameFieldChange
2009-10-21 18:15jschuhmacherNew Issue
2009-10-21 18:15jschuhmacherFile Added: jessie.log
2009-10-22 13:15signolesStatusnew => assigned
2009-10-22 13:15signolesAssigned To => cmarche
2009-11-03 16:34cmarcheNote Added: 0000513
2009-11-03 16:34cmarcheStatusassigned => resolved
2009-11-03 16:34cmarcheResolutionopen => unable to reproduce
2009-11-03 16:57signolesNote Added: 0000515
2009-11-03 16:57signolesStatusresolved => feedback
2009-11-03 16:57signolesResolutionunable to reproduce => reopened
2010-01-06 15:20jschuhmacherFile Added: system.c
2010-01-06 15:21jschuhmacherNote Added: 0000616
2010-12-16 17:40cmarcheNote Added: 0001325
2010-12-16 17:40cmarcheStatusfeedback => resolved
2010-12-16 17:40cmarcheResolutionreopened => fixed
2010-12-18 11:18signolesFixed in Version => Frama-C Carbon-20101202-beta2
2010-12-18 11:19signolesStatusresolved => closed
2013-12-19 01:14Source_changeset_attached => framac master 83a85df6
2014-02-12 16:56Source_changeset_attached => framac stable/neon 83a85df6