Frama-C Bug Tracking System - Frama-C
View Issue Details
0000291Frama-CPlug-in > jessiepublic2009-10-20 10:352009-10-20 10:50
Sylvain Boulme 
cmarche 
normalminoralways
assignedopen 
Frama-C Beryllium-20090902 
 
0000291: Unbound variable raised by why in presence of an unsafe cast
In presence of an unsafe cast (that breaks the hypothesis of non-alias between pointers of distinct types), "frama-c -jessie" crashes with the error below instead of a more friendly error message:

 File "why/septype0.why", line 617, characters 44-65:
 Unbound variable bitvector_alloc_table
No tags attached.
c septype0.c (493) 2009-10-20 10:35
https://bts.frama-c.com/file_download.php?file_id=24&type=bug
Issue History
2009-10-20 10:35Sylvain BoulmeNew Issue
2009-10-20 10:35Sylvain BoulmeFile Added: septype0.c
2009-10-20 10:50signolesStatusnew => assigned
2009-10-20 10:50signolesAssigned To => cmarche

There are no notes attached to this issue.