Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000363Frama-CPlug-in > jessiepublic2009-12-16 13:282010-12-18 11:19
Reporterjschuhmacher 
Assigned Tocmarche 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in VersionFrama-C Carbon-20101202-beta2 
Summary0000363: Plugin jessie aborted because of an internal error.
DescriptionFrama-C aborts with the following message:

test_annotaties_jelle.c:368:[jessie] failure: Unexpected failure.
                  Please submit bug report (Ref. "norm.ml:143:26").
[kernel] Plugin jessie aborted because of an internal error.
         Please report with 'crash' at http://bts.frama-c.com [^]

when called as "frama-c -jessie test_annotaties_jelle.c"

The source file causing the problem is attached.
TagsNo tags attached.
Attached Filesc file icon test_annotaties_jelle.c [^] (15,815 bytes) 2009-12-16 13:28 [Show Content]

- Relationships

-  Notes
(0000610)
signoles (manager)
2009-12-16 15:06
edited on: 2009-12-16 15:07

Is it the following of task 0000299?

(0000615)
jschuhmacher (reporter)
2010-01-06 14:52

No I don't think so, Frama-C gives a different error code and it is a different source file.
(0001326)
cmarche (developer)
2010-12-16 17:44


Why 2.28, jessie reports now that it can't handle & in

\valid(&proc + (0..104-1));

instead,

\valid(proc + (0..104-1));

works

- Issue History
Date Modified Username Field Change
2009-12-16 13:28 jschuhmacher New Issue
2009-12-16 13:28 jschuhmacher Status new => assigned
2009-12-16 13:28 jschuhmacher Assigned To => cmarche
2009-12-16 13:28 jschuhmacher File Added: test_annotaties_jelle.c
2009-12-16 15:06 signoles Note Added: 0000610
2009-12-16 15:07 signoles Note Edited: 0000610
2010-01-06 14:52 jschuhmacher Note Added: 0000615
2010-12-16 17:44 cmarche Note Added: 0001326
2010-12-16 17:44 cmarche Status assigned => resolved
2010-12-16 17:44 cmarche Resolution open => 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