Remove type argument from VD.update_offset

Author: sim642

src/analyses/base.ml

@@ -1093,9 +1093,6 @@ struct
      * not include the flag. *)
     let update_one_addr (x, offs) (nst, fl, dep): store =
       let cil_offset = Offs.to_cil_offset offs in
-      let t = match t_override with
-        | Some t -> t
-        | None -> Cil.typeOf (Lval(Var x, cil_offset)) in
       if M.tracing then M.tracel "setosek" ~var:firstvar "update_one_addr: start with '%a' (type '%a') \nstate:%a\n\n" AD.pretty (AD.from_var_offset (x,offs)) d_type x.vtype CPA.pretty st;
       if isFunctionType x.vtype then begin
         if M.tracing then M.tracel "setosek" ~var:firstvar "update_one_addr: returning: '%a' is a function type \n" d_type x.vtype;
@@ -1122,13 +1119,13 @@ struct
           if M.tracing then M.tracel "setosek" ~var:x.vname "update_one_addr: update a global var '%s' ...\n" x.vname;
           (* Here, an effect should be generated, but we add it to the local
            * state, waiting for the sync function to publish it. *)
-          update_variable x (VD.update_offset a (get x nst) offs value (Option.map (fun x -> Lval x) lval_raw) (Var x, cil_offset) t) nst, fl, dep
+          update_variable x (VD.update_offset a (get x nst) offs value (Option.map (fun x -> Lval x) lval_raw) (Var x, cil_offset)) nst, fl, dep
         end
       else begin
         if M.tracing then M.tracel "setosek" ~var:x.vname "update_one_addr: update a local var '%s' ...\n" x.vname;
         (* Normal update of the local state *)
         let lval_raw = (Option.map (fun x -> Lval x) lval_raw) in
-        let new_value = VD.update_offset a (CPA.find x nst) offs value lval_raw ((Var x), cil_offset) t in
+        let new_value = VD.update_offset a (CPA.find x nst) offs value lval_raw ((Var x), cil_offset) in
         (* what effect does changing this local variable have on arrays -
            we only need to do this here since globals are not allowed in the
            expressions for partitioning *)
@@ -1675,9 +1672,8 @@ struct
         | `Bot -> (* current value is VD `Bot *)
           (match Addr.to_var_offset (AD.choose lval_val) with
           | [(x,offs)] ->
-            let t = v.vtype in
             let iv = bot_value ctx.ask ctx.global ctx.local v.vtype in (* correct bottom value for top level variable *)
-            let nv = VD.update_offset ctx.ask iv offs rval_val (Some  (Lval lval)) lval t in (* do desired update to value *)
+            let nv = VD.update_offset ctx.ask iv offs rval_val (Some  (Lval lval)) lval in (* do desired update to value *)
             set_savetop ctx.ask ctx.global ctx.local (AD.from_var v) nv (* set top-level variable to updated value *)
           | _ ->
             set_savetop ctx.ask ctx.global ctx.local lval_val rval_val ~lval_raw:lval ~rval_raw:rval

src/cdomains/valueDomain.ml

@@ -17,7 +17,7 @@ sig
   include Lattice.S
   type offs
   val eval_offset: Q.ask -> (AD.t -> t) -> t-> offs -> exp option -> lval option -> t
-  val update_offset: Q.ask -> t -> offs -> t -> exp option -> lval -> typ -> t
+  val update_offset: Q.ask -> t -> offs -> t -> exp option -> lval -> t
   val update_array_lengths: (exp -> t) -> t -> Cil.typ -> t
   val affect_move: ?replace_with_const:bool -> Q.ask -> t -> varinfo -> (exp -> int option) -> t
   val affecting_vars: t -> varinfo list
@@ -739,19 +739,19 @@ struct
     in
     do_eval_offset ask f x offs exp l o v
 
-  let update_offset (ask: Q.ask) (x:t) (offs:offs) (value:t) (exp:exp option) (v:lval) (t:typ): t =
-    let rec do_update_offset (ask:Q.ask) (x:t) (offs:offs) (value:t) (exp:exp option) (l:lval option) (o:offset option) (v:lval) (t:typ):t =
+  let update_offset (ask: Q.ask) (x:t) (offs:offs) (value:t) (exp:exp option) (v:lval): t =
+    let rec do_update_offset (ask:Q.ask) (x:t) (offs:offs) (value:t) (exp:exp option) (l:lval option) (o:offset option) (v:lval):t =
       let mu = function `Blob (`Blob (y, s'), s) -> `Blob (y, ID.join s s') | x -> x in
       match x, offs with
       | `Blob (x,s), `Index (_,ofs) ->
         begin
           let l', o' = shift_one_over l o in
-          mu (`Blob (join x (do_update_offset ask x ofs value exp l' o' v t), s))
+          mu (`Blob (join x (do_update_offset ask x ofs value exp l' o' v), s))
         end
       | `Blob (x,s),_ ->
         begin
           let l', o' = shift_one_over l o in
-          mu (`Blob (join x (do_update_offset ask x offs value exp l' o' v t), s))
+          mu (`Blob (join x (do_update_offset ask x offs value exp l' o' v), s))
         end
       | _ ->
       let result =
@@ -762,12 +762,11 @@ struct
             | _ -> value
           end
         | `Field (fld, offs) when fld.fcomp.cstruct -> begin
-            let t = fld.ftype in
             match x with
             | `Struct str ->
               begin
                 let l', o' = shift_one_over l o in
-                let value' =  (do_update_offset ask (Structs.get str fld) offs value exp l' o' v t) in
+                let value' =  (do_update_offset ask (Structs.get str fld) offs value exp l' o' v) in
                 `Struct (Structs.replace str fld value')
               end
             | `Bot ->
@@ -778,12 +777,11 @@ struct
               in
               let strc = init_comp fld.fcomp in
               let l', o' = shift_one_over l o in
-              `Struct (Structs.replace strc fld (do_update_offset ask `Bot offs value exp l' o' v t))
+              `Struct (Structs.replace strc fld (do_update_offset ask `Bot offs value exp l' o' v))
             | `Top -> M.warn "Trying to update a field, but the struct is unknown"; top ()
             | _ -> M.warn "Trying to update a field, but was not given a struct"; top ()
           end
         | `Field (fld, offs) -> begin
-            let t = fld.ftype in
             let l', o' = shift_one_over l o in
             match x with
             | `Union (last_fld, prev_val) ->
@@ -812,25 +810,22 @@ struct
                     top (), offs
                 end
               in
-              `Union (`Lifted fld, do_update_offset ask tempval tempoffs value exp l' o' v t)
-            | `Bot -> `Union (`Lifted fld, do_update_offset ask `Bot offs value exp l' o' v t)
+              `Union (`Lifted fld, do_update_offset ask tempval tempoffs value exp l' o' v)
+            | `Bot -> `Union (`Lifted fld, do_update_offset ask `Bot offs value exp l' o' v)
             | `Top -> M.warn "Trying to update a field, but the union is unknown"; top ()
             | _ -> M.warn_each "Trying to update a field, but was not given a union"; top ()
           end
         | `Index (idx, offs) -> begin
             let l', o' = shift_one_over l o in
             match x with
             | `Array x' ->
-              (match t with
-              | TArray(t1 ,_,_) ->
-                let e = determine_offset ask l o exp (Some v) in
-                let new_value_at_index = do_update_offset ask (CArrays.get ask x' (e,idx)) offs value exp l' o' v t1 in
-                let new_array_value = CArrays.set ask x' (e, idx) new_value_at_index in
-                `Array new_array_value
-              | _ ->  M.warn "Trying to update an array, but the type was not array"; top ())
+              let e = determine_offset ask l o exp (Some v) in
+              let new_value_at_index = do_update_offset ask (CArrays.get ask x' (e,idx)) offs value exp l' o' v in
+              let new_array_value = CArrays.set ask x' (e, idx) new_value_at_index in
+              `Array new_array_value
             | `Bot ->  M.warn_each("encountered array bot, made array top"); `Array (CArrays.top ());
             | `Top -> M.warn "Trying to update an index, but the array is unknown"; top ()
-            | x when IndexDomain.to_int idx = Some 0L -> do_update_offset ask x offs value exp l' o' v t
+            | x when IndexDomain.to_int idx = Some 0L -> do_update_offset ask x offs value exp l' o' v
             | _ -> M.warn_each ("Trying to update an index, but was not given an array("^short 80 x^")"); top ()
           end
       in mu result
@@ -839,7 +834,7 @@ struct
       | Some(Lval (x,o)) -> Some ((x, NoOffset)), Some(o)
       | _ -> None, None
     in
-    do_update_offset ask x offs value exp l o v t
+    do_update_offset ask x offs value exp l o v
 
   let rec affect_move ?(replace_with_const=false) ask (x:t) (v:varinfo) movement_for_expr:t =
     let move_fun x = affect_move ~replace_with_const:replace_with_const ask x v movement_for_expr in