From 8dd041c5af678d6e842abf91c9739d3f219e28cb Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Wed, 31 May 2017 06:36:51 -0700 Subject: [PATCH] [inferbo] Moving stuff Reviewed By: jvillard Differential Revision: D5137593 fbshipit-source-id: a089d18 --- .../src/bufferoverrun/bufferOverrunChecker.ml | 22 +++++++++---------- .../src/bufferoverrun/bufferOverrunDomain.ml | 4 +--- 2 files changed, 12 insertions(+), 14 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 211e349ff..a63c720b4 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -263,17 +263,6 @@ struct : Dom.Mem.astate -> extras ProcData.t -> CFG.node -> Sil.instr -> Dom.Mem.astate = fun mem { pdesc; tenv; extras } node instr -> let pname = Procdesc.get_proc_name pdesc in - let try_decl_arr (mem, inst_num) (pvar, typ) = - match typ.Typ.desc with - | Typ.Tarray (typ, length, stride0) -> - let loc = Loc.of_pvar pvar in - let stride = Option.map ~f:IntLit.to_int stride0 in - let mem = - declare_array pname node loc typ ~length ?stride ~inst_num ~dimension:1 mem - in - (mem, inst_num + 1) - | _ -> (mem, inst_num) - in let output_mem = match instr with | Load (id, exp, _, loc) -> @@ -301,6 +290,17 @@ struct handle_unknown_call pname ret callee_pname params node mem loc) | Declare_locals (locals, _) -> (* array allocation in stack e.g., int arr[10] *) + let try_decl_arr (mem, inst_num) (pvar, typ) = + match typ.Typ.desc with + | Typ.Tarray (typ, length, stride0) -> + let loc = Loc.of_pvar pvar in + let stride = Option.map ~f:IntLit.to_int stride0 in + let mem = + declare_array pname node loc typ ~length ?stride ~inst_num ~dimension:1 mem + in + (mem, inst_num + 1) + | _ -> (mem, inst_num) + in let (mem, inst_num) = List.fold ~f:try_decl_arr ~init:(mem, 1) locals in declare_symbolic_parameter pdesc tenv node inst_num mem | Call (_, fun_exp, _, loc, _) -> diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 50c2834cf..30cdf07e2 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -163,9 +163,7 @@ module ConditionSet = struct include AbstractDomain.FiniteSet (Condition) - module Map = Caml.Map.Make (struct - type t = Location.t [@@deriving compare] - end) + module Map = Caml.Map.Make (Location) let add_bo_safety : Typ.Procname.t -> Location.t -> string -> idx:Itv.t -> size:Itv.t -> t -> t