Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000537Frama-CPlug-in > jessiepublic2010-07-09 13:592010-12-18 11:19
Reporterboris 
Assigned Tocmarche 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101202-beta2 
Summary0000537: Predicate Sorted causes crash (norm.ml:1524:10)
DescriptionJessie crashes on the code attached. Without the predicated Sorted, Jessie doesn't crash.
TagsNo tags attached.
Attached Filesc file icon bs-crash.c [^] (1,150 bytes) 2010-07-09 13:59 [Show Content]

- Relationships

-  Notes
(0000995)
cmarche (developer)
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 (developer)
2010-12-16 16:45


Why 2.28 now outputs a better error message

- Issue History
Date Modified Username Field Change
2010-07-09 13:59 boris New Issue
2010-07-09 13:59 boris Status new => assigned
2010-07-09 13:59 boris Assigned To => cmarche
2010-07-09 13:59 boris File Added: bs-crash.c
2010-07-09 14:53 cmarche Note Added: 0000995
2010-12-16 16:45 cmarche Note Added: 0001314
2010-12-16 16:45 cmarche Status assigned => resolved
2010-12-16 16:45 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