Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002258Frama-CPlug-in > RTEpublic2016-11-24 13:532016-12-05 20:30
Reporterjulien-cohen 
Assigned Toyakobowski 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformPCOSLinux Ubuntu OS Version16.04 LTS
Product VersionFrama-C Magnesium 
Target VersionFixed in Version 
Summary0002258: Annotation wrongly displayed as checked (green bullet) whereas it is false, when using the option -rte on command line.
DescriptionI 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.
Steps To ReproduceHere 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.
Additional InformationPosted 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).
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006288)
maroneze (developer)
2016-11-24 14:30

Thank you, we are currently looking at it.
(0006289)
yakobowski (manager)
2016-11-28 10:52

The fix will be part of the Silicon version of Frama-C.
(0006297)
yakobowski (manager)
2016-12-05 20:30

Fixed in Frama-C Silicon.

- Issue History
Date Modified Username Field Change
2016-11-24 13:53 julien-cohen New Issue
2016-11-24 13:53 julien-cohen Status new => assigned
2016-11-24 13:53 julien-cohen Assigned To => signoles
2016-11-24 14:28 maroneze Assigned To signoles => maroneze
2016-11-24 14:30 maroneze Note Added: 0006288
2016-11-24 14:30 maroneze Status assigned => confirmed
2016-11-28 10:52 yakobowski Note Added: 0006289
2016-11-29 17:33 yakobowski Status confirmed => resolved
2016-11-29 17:33 yakobowski Resolution open => fixed
2016-11-29 17:33 yakobowski Assigned To maroneze => yakobowski
2016-12-05 20:30 yakobowski Status resolved => closed
2016-12-05 20:30 yakobowski Note Added: 0006297


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker