From ca14c2106ecfd895366e1cb836bdc578928b191c Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Mon, 26 Mar 2018 05:26:56 -0700 Subject: [PATCH] [inferbo] Refactoring 1/8: labels for arrayBlk functions Reviewed By: jvillard Differential Revision: D7397114 fbshipit-source-id: e63c82d --- infer/src/bufferoverrun/arrayBlk.ml | 8 +++++--- infer/src/bufferoverrun/bufferOverrunSemantics.ml | 2 +- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index e66cee56e..45f01efa3 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/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 = - fun a o sz st -> add a (ArrInfo.make (o, sz, st)) bot +let make : Allocsite.t -> offset:Itv.t -> size:Itv.t -> stride:Itv.t -> astate = + 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 diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 301572d6b..fc990f9df 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/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 =