Frama-C Bug Tracking System - Frama-C
View Issue Details
0000537Frama-CPlug-in > jessiepublic2010-07-09 13:592010-12-18 11:19
boris 
cmarche 
normalcrashalways
closedfixed 
Frama-C Boron-20100401 
Frama-C Carbon-20101202-beta2 
0000537: Predicate Sorted causes crash (norm.ml:1524:10)
Jessie crashes on the code attached. Without the predicated Sorted, Jessie doesn't crash.
No tags attached.
c bs-crash.c (1,150) 2010-07-09 13:59
https://bts.frama-c.com/file_download.php?file_id=107&type=bug
Issue History
2010-07-09 13:59borisNew Issue
2010-07-09 13:59borisStatusnew => assigned
2010-07-09 13:59borisAssigned To => cmarche
2010-07-09 13:59borisFile Added: bs-crash.c
2010-07-09 14:53cmarcheNote Added: 0000995
2010-12-16 16:45cmarcheNote Added: 0001314
2010-12-16 16:45cmarcheStatusassigned => resolved
2010-12-16 16:45cmarcheResolutionopen => fixed
2010-12-18 11:18signolesFixed in Version => Frama-C Carbon-20101202-beta2
2010-12-18 11:19signolesStatusresolved => closed

Notes
(0000995)
cmarche   
2010-07-09 14:53   
This is due to the distinction between int a[] and int *a introduced in Frama-C boron. So please use Sorted(int *a, ...) instead. I agree that this should be detected earlier by jessie.
(0001314)
cmarche   
2010-12-16 16:45   
Why 2.28 now outputs a better error message