Frama-C Bug Tracking System - Frama-C
View Issue Details
0001263Frama-CKernelpublic2012-08-08 12:482012-09-19 17:16
boris 
virgile 
lowfeaturealways
closedfixed 
Frama-C Nitrogen-20111001 
Frama-C Oxygen-20120901 
0001263: Identical lvals not equal in Cil_datatype.Lval.Hashtbl
The 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)
No tags attached.
Issue History
2012-08-08 12:48borisNew Issue
2012-08-08 16:38yakobowskiNote Added: 0003393
2012-08-08 16:38yakobowskiPrioritynormal => low
2012-08-08 16:38yakobowskiSeveritymajor => feature
2012-08-09 19:29yakobowskiStatusnew => assigned
2012-08-09 19:29yakobowskiAssigned To => virgile
2012-09-06 19:04virgileNote Added: 0003431
2012-09-06 19:04virgileStatusassigned => resolved
2012-09-06 19:04virgileResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed

Notes
(0003393)
yakobowski   
2012-08-08 16:38   
See my answer on the mailing list. I'm updating the severity accordingly.
(0003431)
virgile   
2012-09-06 19:04   
fixed in revision 19770