ID0002258: **This issue was created automatically from Mantis Issue 2258. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002258 | Frama-C | Plug-in > RTE | public | 2016-11-24 | 2016-12-05 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | julien-cohen | **Assigned To** | yakobowski | **Resolution** | fixed | | **Priority** | normal | **Severity** | major | **Reproducibility** | always | | **Platform** | PC | **OS** | Linux Ubuntu | **OS Version** | 16.04 LTS | | **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | - | ### Description : I have a program with an incorrect acces outside an array. When lauching frama-c-gui with no options and value analysis, the out-of-bounds access is detected and the corresponding annotation is displayed with an orange bullet. When using the -rte option, two annotations are displayed (for the lower and upper bound of the array), and a green bullet is displayed for both (which is not correct). /*@ assert rte: index_bound: 0 ≤ cpt; */ /*@ assert rte: index_bound: cpt < 5; */ The console says : tableau_erreur.c:11:[value] Assertion 'rte,index_bound' got status valid. ### Additional Information : Posted on http://stackoverflow.com/questions/40763614/unsound-behavior-with-rte-option-in-magnesium/40766174#40766174 . There are two screen captures there. Someone (anol) replied and gave additional information (see the post). ### Steps To Reproduce : Here is my program : int main(){ int t[5] = {1,2,3,4,5}; int cpt =0 ; int tmp ; while (cpt<10){ tmp = getchar() ; if ( t[cpt] > tmp ) { return 1 ; } cpt++ ; } return 10 ; } The problem occurs when launching frama-c-gui -rte and the calue analysis on this program.