Float promoted to double
ID0000329: This issue was created automatically from Mantis Issue 329. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000329 | Frama-C | Kernel > ACSL implementation | public | 2009-11-13 | 2014-02-12 |
| Reporter | sboldo | Assigned To | cmarche | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | Frama-C Boron-20100401 |
Description :
I am in the svn 33841 version.
In the given file, the float x is propoted by frama-c to a double precision number by frama-c itself (frama-c-gui): instead of \exact(x) I have \exact((double )x)