strange value-set for loop-variable in presence of flexible array
ID0000924: This issue was created automatically from Mantis Issue 924. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000924 | Frama-C | Plug-in > Eva | public | 2011-08-12 | 2011-08-13 |
| Reporter | Jochen | Assigned To | pascal | Resolution | no change required |
| Priority | normal | Severity | text | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Carbon-20110201 | Target Version | - | Fixed in Version | - |
Description :
Analyzing the attached program with "frama-c -val ftest.c -main f -no-unicode -slevel 1000" reports "i IN {0; 1; 2; }", which seems a too small set.
When "n" is replaced by e.g. "9" in line 1 (col.19 only) and 4, the computed set "i IN {9; }" seems ok. When instead "a[i]" is replaced by "i" in line 5, the computed set "i IN [0..2147483647]" seems ok, too. (Only in this case, messages like "[value] Semantic level unrolling superposing up to ..." are printed - is this ok?)
If arrays with non-constants upper-bound expressions are not supported, a corresponding warning should be emitted for line 1.