E-ACSL type system crash
ID0002284: This issue was created automatically from Mantis Issue 2284. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002284 | Frama-C | Plug-in > E-ACSL | public | 2017-02-24 | 2017-05-31 |
| Reporter | kvorobyov | Assigned To | signoles | Resolution | fixed |
| Priority | normal | Severity | crash | Reproducibility | always |
| Platform | Linux | OS | Gentoo | OS Version | - |
| Product Version | Frama-C 14-Silicon | Target Version | - | Fixed in Version | Frama-C 15-Phosphorus |
Description :
Run:
e-acsl-gcc.sh --rte=mem mesa_error.c
crashes E-ACSL with the following message: [e-acsl] failure: expected an integral type for (int)((float)(*(red + i) * scale))
Base frama-C command: frama-c -no-frama-c-stdlib a.c -rte -no-warn-signed-overflow -no-warn-unsigned-overflow -no-warn-signed-downcast -no-warn-unsigned-downcast -rte-no-div -rte-no-float-to-int -rte-mem -rte-no-pointer-call -rte-no-precond -rte-no-shift -rte-no-trivial-annotations -then -e-acsl -then-last -print -ocode a.out.frama.c
Supposedly this happens because integer interval is computed incorrectly due to casts