Frama-C Bug Tracking System - Frama-C
View Issue Details
0002284Frama-CPlug-in > E-ACSLpublic2017-02-24 14:262017-05-31 19:05
kvorobyov 
signoles 
normalcrashalways
closedfixed 
LinuxGentoo
Frama-C 14 Silicon 
Frama-C 15 Phosphorus 
0002284: E-ACSL type system crash
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
No tags attached.
c mesa_int_.c (269) 2017-02-24 14:26
https://bts.frama-c.com/file_download.php?file_id=1148&type=bug
Issue History
2017-02-24 14:26kvorobyovNew Issue
2017-02-24 14:26kvorobyovStatusnew => assigned
2017-02-24 14:26kvorobyovAssigned To => signoles
2017-02-24 14:26kvorobyovFile Added: mesa_int_.c
2017-02-27 11:15signolesStatusassigned => resolved
2017-02-27 11:15signolesResolutionopen => fixed
2017-05-31 19:04signolesFixed in Version => Frama-C 15 Phosphorus
2017-05-31 19:05signolesStatusresolved => closed

There are no notes attached to this issue.