[inferbo] Refactoring 1/8: labels for arrayBlk functions

Reviewed By: jvillard

Differential Revision: D7397114

fbshipit-source-id: e63c82d

infer/src/bufferoverrun/arrayBlk.ml

@@ -21,7 +21,9 @@ module ArrInfo = struct
 
   let top : t = {offset= Itv.top; size= Itv.top; stride= Itv.top}
 
-  let make : Itv.t * Itv.t * Itv.t -> t = fun (o, s, stride) -> {offset= o; size= s; stride}
+  let make : offset:Itv.t -> size:Itv.t -> stride:Itv.t -> t =
+   fun ~offset ~size ~stride -> {offset; size; stride}
+
 
   let join : t -> t -> t =
    fun a1 a2 ->
@@ -102,8 +104,8 @@ let unknown : astate = add Allocsite.unknown ArrInfo.top bot
 
 let is_bot : astate -> bool = is_empty
 
-let make : Allocsite.t -> Itv.t -> Itv.t -> Itv.t -> astate =
+let make : Allocsite.t -> offset:Itv.t -> size:Itv.t -> stride:Itv.t -> astate =
- fun a o sz st -> add a (ArrInfo.make (o, sz, st)) bot
+ fun a ~offset ~size ~stride -> singleton a (ArrInfo.make ~offset ~size ~stride)
 
 
 let offsetof : astate -> Itv.t = fun a -> fold (fun _ arr -> Itv.join arr.ArrInfo.offset) a Itv.bot

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -333,7 +333,7 @@ module Make (CFG : ProcCfg.S) = struct
     let allocsite = get_allocsite pdesc node inst_num dimension in
     let int_stride = match stride0 with None -> sizeof typ | Some stride -> stride in
     let stride = Itv.of_int int_stride in
-    ArrayBlk.make allocsite offset size stride |> Val.of_array_blk
+    ArrayBlk.make allocsite ~offset ~size ~stride |> Val.of_array_blk
 
 
   let prune_unop : PrunePairs.t ref -> Exp.t -> Mem.astate -> Mem.astate =