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.