Value analysis generates incorrect Imperative outputs for arrays
ID0002030: This issue was created automatically from Mantis Issue 2030. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002030 | Frama-C | Plug-in > Eva | public | 2014-12-12 | 2015-01-07 |
| Reporter | gaggarwal | Assigned To | yakobowski | Resolution | no change required |
| Priority | normal | Severity | feature | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | - |
Description :
In case, the size of an array is not known, value analysis generated array[0..1] as Imperative outputs of a function updating array.
Additional Information :
In above example I tried adding some bound on variable count using requires clause as below:
/@ requires 0 < count < 8; / void copy(int src, int dest, int count) { for(int i=0; i<count; i++) { dest[i] = src[i]; } }
Even then imperative output of function copy generated was S_dest[0..1]
Steps To Reproduce :
For example: Consider a file f.c has below copy function:
void copy(int* src, int* dest, int count) { for(int i=0; i<count; i++) { dest[i] = src[i]; } }
Execute: frama-c -val -out-external -lib-entry -main copy f.c Result: [inout] Out (external) for function copy: S_dest[0..1]
S_dest[0..1] is not a over-estimation of location which can be modified by function copy.