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
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information