Imprecise result on almost deterministic program
ID0001074: This issue was created automatically from Mantis Issue 1074. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001074 | Frama-C | Plug-in > Eva | public | 2012-01-28 | 2012-09-19 |
| Reporter | yakobowski | Assigned To | pascal | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | Frama-C Oxygen-20120901 |
Description :
----- memsetff.c -------- int t[10];
void main (char c) { for (int i=0;i<sizeof(t);i++) ((char*)t)[i]=0xFF;
Frama_C_show_each(t[1]);
if(c) t[1] = 1; }
To be tested with frama-c -val memsetff.c -precise-unions -big-ints-hex 0x10 -slevel 100000 (-precise-unions has not effect in this case)
The obtained possible values for t[1] are [1] ? -..-, which is over-approximated.