assertion at line 2772 of jc/jc_typing.ml fails
ID0000434: This issue was created automatically from Mantis Issue 434. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000434 | Frama-C | Plug-in > jessie | public | 2010-03-25 | 2010-12-18 |
| Reporter | Jochen | Assigned To | cmarche | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Beryllium-20090902 | Target Version | - | Fixed in Version | Frama-C Carbon-20101202-beta2 |
Description :
(Similar to report 432; Virgile encouraged me to resubmit:)
Calling the unix command <<frama-c -jessie -jessie-no-regions -jessie-why-opt="-exp goal" -jessie-atp simplify ftest.c>> causes the assertion in the jessie source file jc/jc_typing.ml, line 2772:25-31 to fail.
The error vanishes if I delete the subformula <<\base_addr(f) == \base_addr(b) &&>> in line 12 of the attached file ftest.c.