diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli index abc6feb5e..3fc960667 100644 --- a/infer/src/bufferoverrun/bounds.mli +++ b/infer/src/bufferoverrun/bounds.mli @@ -35,26 +35,13 @@ module Bound : sig val pinf : t - val of_normal_path : - (unsigned:bool -> Symb.SymbolPath.t -> Symb.Symbol.t) - -> unsigned:bool - -> Symb.SymbolPath.partial - -> t + val of_normal_path : Symb.Symbol.make_t -> unsigned:bool -> Symb.SymbolPath.partial -> t - val of_offset_path : - is_void:bool - -> (unsigned:bool -> Symb.SymbolPath.t -> Symb.Symbol.t) - -> Symb.SymbolPath.partial - -> t + val of_offset_path : is_void:bool -> Symb.Symbol.make_t -> Symb.SymbolPath.partial -> t - val of_length_path : - is_void:bool - -> (unsigned:bool -> Symb.SymbolPath.t -> Symb.Symbol.t) - -> Symb.SymbolPath.partial - -> t + val of_length_path : is_void:bool -> Symb.Symbol.make_t -> Symb.SymbolPath.partial -> t - val of_modeled_path : - (unsigned:bool -> Symb.SymbolPath.t -> Symb.Symbol.t) -> Symb.SymbolPath.partial -> t + val of_modeled_path : Symb.Symbol.make_t -> Symb.SymbolPath.partial -> t val is_offset_path_of : Symb.SymbolPath.partial -> t -> bool diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index bc9ecd02f..7617b78ee 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -424,6 +424,12 @@ module Val = struct let trace = if Loc.is_global l then Trace.Global l else Trace.Parameter l in TraceSet.singleton location trace in + let itv_val () = + let l = Loc.of_path path in + let traces = traces_of_loc l in + let unsigned = Typ.is_unsigned_int typ in + of_itv ~traces (Itv.of_normal_path ~unsigned path) + in let ptr_to_c_array_alloc deref_path size = let allocsite = Allocsite.make_symbol deref_path in let offset = Itv.zero in @@ -436,10 +442,7 @@ module Val = struct (if is_java then ", is_java" else "") ; match typ.Typ.desc with | Tint _ | Tfloat _ | Tvoid | Tfun _ | TVar _ -> - let l = Loc.of_path path in - let traces = traces_of_loc l in - let unsigned = Typ.is_unsigned_int typ in - of_itv ~traces (Itv.of_normal_path ~unsigned path) + itv_val () | Tptr (elt, _) -> if is_java || SPath.is_this path then let deref_kind = @@ -489,10 +492,7 @@ module Val = struct let length = Itv.of_length_path ~is_void:false path in of_java_array_alloc allocsite ~length ~traces | Some JavaInteger -> - let l = Loc.of_path path in - let traces = traces_of_loc l in - let unsigned = Typ.is_unsigned_int typ in - of_itv ~traces (Itv.of_normal_path ~unsigned path) + itv_val () | None -> let l = Loc.of_path path in let traces = traces_of_loc l in diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index fee65db24..6ba32300e 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/infer/src/bufferoverrun/symb.ml @@ -293,11 +293,11 @@ module Symbol = struct SymbolPath.equal path1 path2 - let make_onevalue : unsigned:bool -> SymbolPath.t -> t = - fun ~unsigned path -> OneValue {unsigned; path} + type make_t = unsigned:bool -> SymbolPath.t -> t + let make_onevalue : make_t = fun ~unsigned path -> OneValue {unsigned; path} - let make_boundend : BoundEnd.t -> unsigned:bool -> SymbolPath.t -> t = + let make_boundend : BoundEnd.t -> make_t = fun bound_end ~unsigned path -> BoundEnd {unsigned; path; bound_end} diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index 27d110083..7dc954723 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/infer/src/bufferoverrun/symb.mli @@ -110,9 +110,11 @@ module Symbol : sig val assert_bound_end : t -> BoundEnd.t -> unit - val make_onevalue : unsigned:bool -> SymbolPath.t -> t + type make_t = unsigned:bool -> SymbolPath.t -> t - val make_boundend : BoundEnd.t -> unsigned:bool -> SymbolPath.t -> t + val make_onevalue : make_t + + val make_boundend : BoundEnd.t -> make_t val exists_str : f:(string -> bool) -> t -> bool end