Frama-C Bug Tracking System - Frama-C
View Issue Details
0000363Frama-CPlug-in > jessiepublic2009-12-16 13:282010-12-18 11:19
jschuhmacher 
cmarche 
normalcrashalways
closedfixed 
Frama-C Beryllium-20090902 
Frama-C Carbon-20101202-beta2 
0000363: Plugin jessie aborted because of an internal error.
Frama-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.
No tags attached.
c test_annotaties_jelle.c (15,815) 2009-12-16 13:28
https://bts.frama-c.com/file_download.php?file_id=41&type=bug
Issue History
2009-12-16 13:28jschuhmacherNew Issue
2009-12-16 13:28jschuhmacherStatusnew => assigned
2009-12-16 13:28jschuhmacherAssigned To => cmarche
2009-12-16 13:28jschuhmacherFile Added: test_annotaties_jelle.c
2009-12-16 15:06signolesNote Added: 0000610
2009-12-16 15:07signolesNote Edited: 0000610
2010-01-06 14:52jschuhmacherNote Added: 0000615
2010-12-16 17:44cmarcheNote Added: 0001326
2010-12-16 17:44cmarcheStatusassigned => resolved
2010-12-16 17:44cmarcheResolutionopen => fixed
2010-12-18 11:18signolesFixed in Version => Frama-C Carbon-20101202-beta2
2010-12-18 11:19signolesStatusresolved => closed

Notes
(0000610)
signoles   
2009-12-16 15:06   
(edited on: 2009-12-16 15:07)
Is it the following of task 0000299?

(0000615)
jschuhmacher   
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   
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