Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000379Frama-CPlug-in > jessiepublic2010-01-21 16:152012-09-21 11:25
Reporterkerstin 
Assigned Tocmarche 
PrioritynormalSeveritycrashReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in Version 
Summary0000379: \separated
DescriptionHello,

we get a crash using the \separate clause in line 8 of the attached example.

Regards,

Kerstin
Additional Informationframa-c -jessie -jessie-why-opt="-exp goal" swap_range.c &

gwlan61:swap_ranges kerstin$ [kernel] preprocessing with "gcc -C -E -I. -dD swap_range.c"
[jessie] Starting Jessie translation
swap_range.c:8:[jessie] failure: Unexpected exception.
                  Please submit bug report (Ref. "Extlib.NotYetImplemented("Interp.pred Pseparated")").
[kernel] Plugin jessie aborted because of an internal error.
         Please report with 'crash' at http://bts.frama-c.com [^]
TagsNo tags attached.
Attached Filesc file icon swap_range.c [^] (997 bytes) 2010-01-21 16:15 [Show Content]

- Relationships
has duplicate 0001002closedcmarche weak feature request for \separated under why-2.30 

-  Notes
(0003090)
yakobowski (manager)
2012-06-10 13:25

Jessie ignoring \separated clauses would be great. This would make comparisons between Jessie and WP much easier, as the same specs could be used for both.
(0003478)
virgile (developer)
2012-09-21 11:25

Suggestion of note #3090 is now implemented: Jessie will only warn when it encounters a \separated (once per program) and just ignore it.

- Issue History
Date Modified Username Field Change
2010-01-21 16:15 kerstin New Issue
2010-01-21 16:15 kerstin Status new => assigned
2010-01-21 16:15 kerstin Assigned To => cmarche
2010-01-21 16:15 kerstin File Added: swap_range.c
2012-06-10 13:25 yakobowski Note Added: 0003090
2012-09-21 11:25 virgile Note Added: 0003478
2012-10-30 20:25 yakobowski Relationship added has duplicate 0001002


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker