Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001263Frama-CKernelpublic2012-08-08 12:482012-09-19 17:16
Reporterboris 
Assigned Tovirgile 
PrioritylowSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001263: Identical lvals not equal in Cil_datatype.Lval.Hashtbl
DescriptionThe code below contains an lval this->gear at positions 1,2. If this->gear is hashed at position 1 using Cil_datatype.Lval.Hashtbl, a find for this->gear fails at position 2.

if(inp == up) {
  if(this->gear < MAX_GEARS && motor_rpm(this, this->gear + 1) >= RPM_MIN)
    this->gear++; // 1
} else if(inp == down) {
  if(this->gear > 1 && motor_rpm(this, this->gear + 1) <= RPM_MAX)
    this->gear--; // 2
}

The problem disappears if the lvals are converted to terms with

let xtl = Logic_utils.lval_to_term_lval false x in
Logic_const.term (TLval xtl) (Cil.typeOfTermLval xtl)

and hashed with

module TermHT = Hashtbl.Make(struct
    type t = Cil_types.term
    let equal = Logic_utils.is_same_term
    let hash = Logic_utils.hash_term
end)
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0003393)
yakobowski (manager)
2012-08-08 16:38

See my answer on the mailing list. I'm updating the severity accordingly.
(0003431)
virgile (developer)
2012-09-06 19:04

fixed in revision 19770

- Issue History
Date Modified Username Field Change
2012-08-08 12:48 boris New Issue
2012-08-08 16:38 yakobowski Note Added: 0003393
2012-08-08 16:38 yakobowski Priority normal => low
2012-08-08 16:38 yakobowski Severity major => feature
2012-08-09 19:29 yakobowski Status new => assigned
2012-08-09 19:29 yakobowski Assigned To => virgile
2012-09-06 19:04 virgile Note Added: 0003431
2012-09-06 19:04 virgile Status assigned => resolved
2012-09-06 19:04 virgile Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker