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
Assigned Tocmarche 
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
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
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.
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 - 2020 MantisBT Team
Powered by Mantis Bugtracker