Unbound variable raised by why in presence of an unsafe cast
ID0000291: This issue was created automatically from Mantis Issue 291. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000291 | Frama-C | Plug-in > jessie | public | 2009-10-20 | 2009-10-20 |
| Reporter | Sylvain Boulme | Assigned To | cmarche | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Beryllium-20090902 | Target Version | - | Fixed in Version | - |
Description :
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