diff --git a/CodeHawk/CHB/bchanalyze/bCHReachingDefs.ml b/CodeHawk/CHB/bchanalyze/bCHReachingDefs.ml
index 708dd388..77d444b7 100644
--- a/CodeHawk/CHB/bchanalyze/bCHReachingDefs.ml
+++ b/CodeHawk/CHB/bchanalyze/bCHReachingDefs.ml
@@ -260,25 +260,28 @@ let analyze_procedure_with_flag_reaching_defs
 let extract_reaching_defs
       (finfo: function_info_int)
       (invariants: (string, (string, atlas_t) H.t) H.t) =
-  H.iter (fun k v ->
-      if H.mem v "reachingdefs" then
-        let inv = H.find v "reachingdefs" in
-        let domain = inv#getDomain "reachingdefs" in
-        let varObserver = domain#observer#getNonRelationalVariableObserver in
-        let vars = domain#observer#getObservedVariables in
-        List.iter (fun (v: variable_t) ->
-            let reachingdefs = (varObserver v)#toSymbolicSet in
-            if reachingdefs#isTop then
-              ()
-            else
-              match reachingdefs#getSymbols with
-              | SET symbols ->
-                 let symbols =
-                   List.sort (fun s1 s2 ->
-                       Stdlib.compare
-                         s1#getBaseName s2#getBaseName) symbols#toList in
-                 finfo#fvarinv#add_reaching_def k v symbols
-              | _ -> ()) vars) invariants
+  begin
+    H.iter (fun k v ->
+        if H.mem v "reachingdefs" then
+          let inv = H.find v "reachingdefs" in
+          let domain = inv#getDomain "reachingdefs" in
+          let varObserver = domain#observer#getNonRelationalVariableObserver in
+          let vars = domain#observer#getObservedVariables in
+          List.iter (fun (v: variable_t) ->
+              let reachingdefs = (varObserver v)#toSymbolicSet in
+              if reachingdefs#isTop then
+                ()
+              else
+                match reachingdefs#getSymbols with
+                | SET symbols ->
+                   let symbols =
+                     List.sort (fun s1 s2 ->
+                         Stdlib.compare
+                           s1#getBaseName s2#getBaseName) symbols#toList in
+                   finfo#add_reaching_def k v symbols;
+                | _ -> ()) vars) invariants;
+    finfo#fvarinv#collect_use_facts
+  end
 
 
 let extract_flag_reaching_defs
diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml
index f529c0a0..40d246ab 100644
--- a/CodeHawk/CHB/bchlib/bCHFloc.ml
+++ b/CodeHawk/CHB/bchlib/bCHFloc.ml
@@ -1557,6 +1557,8 @@ object (self)
      let useops = mk_ops ["defuse"] use_op_name use in
      let usehighops = mk_ops ["defusehigh"] usehigh_op_name usehigh in
      let flagdefops = mk_ops ["flagreachingdefs"] flagdef_op_name flagdefs in
+     let _ = List.iter (fun v -> self#f#add_use_loc v iaddr) use in
+     let _ = List.iter (fun v -> self#f#add_use_high_loc v iaddr) usehigh in
      useops @ usehighops @ defops @ clobberops @ flagdefops
 
    method private evaluate_fts_argument (p: fts_parameter_t) =
diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml
index 8f893058..353f8a19 100644
--- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml
+++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml
@@ -1750,6 +1750,50 @@ object (self)
 
   method fvarinv = varinvio
 
+  val uselocs = H.create 5
+  val usehighlocs = H.create 5
+
+  method add_reaching_def
+           (iaddr: string) (v: variable_t) (deflocs: symbol_t list) =
+    begin
+      self#fvarinv#add_reaching_def iaddr v deflocs;
+      List.iter (fun s ->
+          if (List.length s#getAttributes) = 0 then
+            let defloc = s#getBaseName in
+            begin
+              (if self#is_use_loc v iaddr then
+                 self#fvarinv#add_use_loc defloc v iaddr);
+              (if self#is_use_high_loc v iaddr then
+                 self#fvarinv#add_use_high_loc defloc v iaddr)
+            end) deflocs
+    end
+
+  method add_use_loc (v: variable_t) (iaddr: string) =
+    let varix = v#getName#getSeqNumber in
+    let entry =
+      if H.mem uselocs varix then
+        H.find uselocs varix
+      else
+        [] in
+    H.replace uselocs varix (iaddr :: entry)
+
+  method add_use_high_loc (v: variable_t) (iaddr: string) =
+    let varix = v#getName#getSeqNumber in
+    let entry =
+      if H.mem usehighlocs varix then
+        H.find usehighlocs varix
+      else
+        [] in
+    H.replace usehighlocs varix (iaddr :: entry)
+
+  method is_use_loc (v: variable_t) (iaddr: string) =
+    let varix = v#getName#getSeqNumber in
+    (H.mem uselocs varix) && (List.mem iaddr (H.find uselocs varix))
+
+  method is_use_high_loc (v: variable_t) (iaddr: string) =
+    let varix = v#getName#getSeqNumber in
+    (H.mem usehighlocs varix) && (List.mem iaddr (H.find usehighlocs varix))
+
   method iinv (iaddr: ctxt_iaddress_t): location_invariant_int =
     invio#get_location_invariant iaddr
 
diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli
index a8975447..6a43e2c0 100644
--- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli
+++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli
@@ -1656,6 +1656,9 @@ class type location_var_invariant_int =
   object
     method reset: unit
     method add_fact: var_invariant_fact_t -> unit
+    method add_use_loc: variable_t -> string -> unit
+    method add_use_high_loc: variable_t -> string -> unit
+    method collect_use_facts: unit
 
     (* accessors *)
     method get_var_facts: variable_t -> var_invariant_int list
@@ -1684,6 +1687,10 @@ class type var_invariant_io_int =
     method add_def_use: string -> variable_t -> symbol_t list -> unit
     method add_def_use_high: string -> variable_t -> symbol_t list -> unit
 
+    method add_use_loc: string -> variable_t -> string -> unit
+    method add_use_high_loc: string -> variable_t -> string -> unit
+    method collect_use_facts: unit
+
     (* accessors *)
     method get_location_var_invariant: string -> location_var_invariant_int
     method get_multiple_reaching_defs: (string * var_invariant_int) list
@@ -4971,6 +4978,16 @@ object
       [iaddr].*)
   method ivarinv: ctxt_iaddress_t -> location_var_invariant_int
 
+  method add_reaching_def: string -> variable_t -> symbol_t list -> unit
+
+  method add_use_loc: variable_t -> string -> unit
+
+  method add_use_high_loc: variable_t -> string -> unit
+
+  method is_use_loc: variable_t -> string -> bool
+
+  method is_use_high_loc: variable_t -> string -> bool
+
   (** {2 Invariant reset}
 
    Note: currently used only for x86.
diff --git a/CodeHawk/CHB/bchlib/bCHLocationVarInvariant.ml b/CodeHawk/CHB/bchlib/bCHLocationVarInvariant.ml
index b8a9c052..f7c9f504 100644
--- a/CodeHawk/CHB/bchlib/bCHLocationVarInvariant.ml
+++ b/CodeHawk/CHB/bchlib/bCHLocationVarInvariant.ml
@@ -145,10 +145,15 @@ object (self)
   val table = H.create 5  (* facts indexed by variable seq number *)
   val facts = H.create 3  (* var_invariant_fact index -> var_invariant_int *)
 
+  val uselocs = H.create 5 (* var-ix -> (var, use locations) *)
+  val usehighlocs = H.create 5  (* var-ix -> (var, use-high locations) *)
+
   method reset =
     begin
       H.clear table;
       H.clear facts;
+      H.clear uselocs;
+      H.clear usehighlocs;
     end
 
   method add_fact (fact: var_invariant_fact_t) =
@@ -164,6 +169,37 @@ object (self)
         H.replace table varindex (fact :: entry)
       end
 
+  method private add_loc table (v: variable_t) (useloc: string) =
+    let varix = v#getName#getSeqNumber in
+    let (_, entry) =
+      if H.mem table varix then
+        H.find table varix
+      else
+        let locset = new SymbolCollections.set_t in
+        begin
+          H.add table varix (v, locset);
+          (v, locset)
+        end in
+    entry#add (new symbol_t useloc)
+
+  method add_use_loc (var: variable_t) (useloc: string) =
+    self#add_loc uselocs var useloc
+
+  method add_use_high_loc (var: variable_t) (useloc: string) =
+    self#add_loc usehighlocs var useloc
+
+  method collect_use_facts =
+    begin
+      H.iter
+        (fun _ (var, locs) ->
+          let locs = List.sort Stdlib.compare locs#toList in
+          self#add_fact (DefUse (var, locs))) uselocs;
+      H.iter
+        (fun _ (var, locs) ->
+          let locs = List.sort Stdlib.compare locs#toList in
+          self#add_fact (DefUseHigh (var,locs))) usehighlocs
+    end
+
   method get_var_facts (var: variable_t): var_invariant_int list =
     List.filter (fun f -> f#get_variable#equal var) self#get_facts
 
@@ -232,10 +268,19 @@ object (self)
   method private add (iaddr: string) (fact: var_invariant_fact_t) =
     (self#get_location_var_invariant iaddr)#add_fact fact
 
+  method collect_use_facts =
+    invariants#iter (fun _ v -> v#collect_use_facts)
+
   method add_reaching_def
            (iaddr: string) (var: variable_t) (locs: symbol_t list) =
     self#add iaddr (ReachingDef (var, locs))
 
+  method add_use_loc (defloc: string) (v: variable_t) (useloc: string) =
+    (self#get_location_var_invariant defloc)#add_use_loc v useloc
+
+  method add_use_high_loc (defloc: string) (v: variable_t) (useloc: string) =
+    (self#get_location_var_invariant defloc)#add_use_high_loc v useloc
+
   method add_flag_reaching_def
            (iaddr: string) (var: variable_t) (locs: symbol_t list) =
     self#add iaddr (FlagReachingDef (var, locs))
diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml
index 0f71599b..a3a0cfce 100644
--- a/CodeHawk/CHB/bchlib/bCHVersion.ml
+++ b/CodeHawk/CHB/bchlib/bCHVersion.ml
@@ -95,8 +95,8 @@ end
 
 
 let version = new version_info_t 
-  ~version:"0.6.0_20241111"
-  ~date:"2024-11-11"
+  ~version:"0.6.0_20241118"
+  ~date:"2024-11-18"
   ~licensee: None
   ~maxfilesize: None
   ()
diff --git a/CodeHawk/CHB/bchlibelf/bCHELFHeader.ml b/CodeHawk/CHB/bchlibelf/bCHELFHeader.ml
index 874750cb..e3b46363 100644
--- a/CodeHawk/CHB/bchlibelf/bCHELFHeader.ml
+++ b/CodeHawk/CHB/bchlibelf/bCHELFHeader.ml
@@ -571,6 +571,8 @@ object(self)
             let cbv =
               if pv#equal wordzero then
                 CBValue numerical_zero
+              else if pv#equal wordnegone then
+                CBValue (mkNumerical (-1))
               else
                 match s with
                 | "address" -> CBAddress pv#to_hex_string
@@ -583,7 +585,7 @@ object(self)
             cbvalues := ((i * 4), cbv) :: !cbvalues) fieldkinds;
         (if List.for_all (fun (_, v) ->
                 match v with
-                | CBValue n -> n#equal numerical_zero
+                | CBValue n -> n#equal numerical_zero || n#equal (mkNumerical (-1))
                 | _ -> false) !cbvalues then
            nullrecord := true
          else
diff --git a/CodeHawk/CHC/cchpre/cCHCheckValid.ml b/CodeHawk/CHC/cchpre/cCHCheckValid.ml
index dc7657c5..9b8df1ed 100644
--- a/CodeHawk/CHC/cchpre/cCHCheckValid.ml
+++ b/CodeHawk/CHC/cchpre/cCHCheckValid.ml
@@ -128,7 +128,8 @@ let rec get_num_value env e =
       | (PlusA, Some v1, Some v2) -> Some (v1#add v2)
       | (MinusA, Some v1, Some v2) -> Some (v1#sub v2)
       | (Mult, Some v1, Some v2) -> Some (v1#mult v2)
-      | (Div, Some v1, Some v2) -> Some (v1#div v2)
+      | (Div, Some v1, Some v2) when not (v2#equal numerical_zero) ->
+         Some (v1#div v2)
       | (Mod, Some _, Some _) -> None
       (* TODO: add some code for mod Some (v1 mod v2) *)
       | _ -> None