diff --git a/infer/src/checkers/impurityDomain.ml b/infer/src/checkers/impurityDomain.ml index a7a27fe41..e8fd4437c 100644 --- a/infer/src/checkers/impurityDomain.ml +++ b/infer/src/checkers/impurityDomain.ml @@ -58,7 +58,7 @@ let add_to_errlog ~nesting ~str ModifiedVar.{var; trace_list} errlog = aux ~nesting:(nesting + 1) ( Errlog.make_trace_element nesting location (F.asprintf "%s '%a' is modified when calling %a at %a" str Var.pp var - PulseDomain.describe_call_event f Location.pp location) + PulseDomain.CallEvent.describe f Location.pp location) [] :: rev_errlog ) (WrittenTo action) diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index 1387f61a6..cc33cc9be 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -49,7 +49,7 @@ let get_message = function F.fprintf fmt "accessing memory that " | ViaCall {f; _} -> F.fprintf fmt "call to %a eventually accesses memory that " - PulseDomain.describe_call_event f + PulseDomain.CallEvent.describe f in let pp_invalidation_trace line fmt trace = match trace.PulseDomain.Trace.action with @@ -59,7 +59,7 @@ let get_message = function F.fprintf fmt "%a on line %d indirectly during the call to %a" PulseDomain.Invalidation.describe (PulseDomain.InterprocAction.get_immediate action) - line PulseDomain.describe_call_event f + line PulseDomain.CallEvent.describe f in let line_of_trace trace = let {Location.line; _} = diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index 467a1b9c2..4ddc2d57c 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/infer/src/pulse/PulseDomain.ml @@ -10,29 +10,31 @@ module L = Logging (* {2 Abstract domain description } *) -type call_event = - | Call of Typ.Procname.t - | Model of string - | SkippedKnownCall of Typ.Procname.t - | SkippedUnknownCall of Exp.t -[@@deriving compare] - -let pp_call_event_config ~verbose fmt = - let pp_proc_name = if verbose then Typ.Procname.pp else Typ.Procname.describe in - function - | Call proc_name -> - F.fprintf fmt "`%a`" pp_proc_name proc_name - | Model model -> - F.fprintf fmt "`%s` (modelled)" model - | SkippedKnownCall proc_name -> - F.fprintf fmt "function `%a` with no summary" pp_proc_name proc_name - | SkippedUnknownCall call_exp -> - F.fprintf fmt "unresolved call expression `%a`" Exp.pp call_exp - - -let pp_call_event = pp_call_event_config ~verbose:true - -let describe_call_event = pp_call_event_config ~verbose:false +module CallEvent = struct + type t = + | Call of Typ.Procname.t + | Model of string + | SkippedKnownCall of Typ.Procname.t + | SkippedUnknownCall of Exp.t + [@@deriving compare] + + let pp_config ~verbose fmt = + let pp_proc_name = if verbose then Typ.Procname.pp else Typ.Procname.describe in + function + | Call proc_name -> + F.fprintf fmt "`%a`" pp_proc_name proc_name + | Model model -> + F.fprintf fmt "`%s` (modelled)" model + | SkippedKnownCall proc_name -> + F.fprintf fmt "function `%a` with no summary" pp_proc_name proc_name + | SkippedUnknownCall call_exp -> + F.fprintf fmt "unresolved call expression `%a`" Exp.pp call_exp + + + let pp = pp_config ~verbose:true + + let describe = pp_config ~verbose:false +end module Invalidation = struct type std_vector_function = @@ -125,7 +127,7 @@ module ValueHistory = struct | CppTemporaryCreated of Location.t | Assignment of {location: Location.t} | Capture of {captured_as: Pvar.t; location: Location.t} - | Call of {f: call_event; location: Location.t} + | Call of {f: CallEvent.t; location: Location.t} [@@deriving compare] let pp_event_no_location fmt = function @@ -138,7 +140,7 @@ module ValueHistory = struct | Assignment _ -> F.pp_print_string fmt "assigned" | Call {f; location= _} -> - F.fprintf fmt "returned from call to %a" pp_call_event f + F.fprintf fmt "returned from call to %a" CallEvent.pp f let location_of_event = function @@ -175,7 +177,7 @@ end module InterprocAction = struct type 'a t = | Immediate of {imm: 'a; location: Location.t} - | ViaCall of {action: 'a t; f: call_event; location: Location.t} + | ViaCall of {action: 'a t; f: CallEvent.t; location: Location.t} [@@deriving compare] let dummy = Immediate {imm= (); location= Location.dummy} @@ -191,7 +193,7 @@ module InterprocAction = struct | Immediate {imm; _} -> pp_immediate fmt imm | ViaCall {f; action; _} -> - F.fprintf fmt "%a in call to %a" pp_immediate (get_immediate action) pp_call_event f + F.fprintf fmt "%a in call to %a" pp_immediate (get_immediate action) CallEvent.pp f let add_to_errlog ~nesting pp_immediate action errlog = @@ -206,7 +208,7 @@ module InterprocAction = struct | ViaCall {action; f; location} -> aux ~nesting:(nesting + 1) ( Errlog.make_trace_element nesting location - (F.asprintf "when calling %a here" pp_call_event f) + (F.asprintf "when calling %a here" CallEvent.pp f) [] :: rev_errlog ) action diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index 50bb3507e..dc066c076 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/infer/src/pulse/PulseDomain.mli @@ -8,13 +8,15 @@ open! IStd module F = Format -type call_event = - | Call of Typ.Procname.t (** known function with summary *) - | Model of string (** hardcoded model *) - | SkippedKnownCall of Typ.Procname.t (** known function without summary *) - | SkippedUnknownCall of Exp.t (** couldn't link the expression to a proc name *) +module CallEvent : sig + type t = + | Call of Typ.Procname.t (** known function with summary *) + | Model of string (** hardcoded model *) + | SkippedKnownCall of Typ.Procname.t (** known function without summary *) + | SkippedUnknownCall of Exp.t (** couldn't link the expression to a proc name *) -val describe_call_event : F.formatter -> call_event -> unit + val describe : F.formatter -> t -> unit +end module Invalidation : sig type std_vector_function = @@ -49,7 +51,7 @@ module ValueHistory : sig | CppTemporaryCreated of Location.t | Assignment of {location: Location.t} | Capture of {captured_as: Pvar.t; location: Location.t} - | Call of {f: call_event; location: Location.t} + | Call of {f: CallEvent.t; location: Location.t} type t = event list [@@deriving compare] @@ -60,7 +62,7 @@ end module InterprocAction : sig type 'a t = | Immediate of {imm: 'a; location: Location.t} - | ViaCall of {action: 'a t; f: call_event; location: Location.t} + | ViaCall of {action: 'a t; f: CallEvent.t; location: Location.t} [@@deriving compare] val get_immediate : 'a t -> 'a diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 537793dd1..1f8f7f59f 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -106,7 +106,7 @@ module StdBasicString = struct let destructor : model = fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate -> - let model = PulseDomain.Model "std::basic_string::~basic_string()" in + let model = PulseDomain.CallEvent.Model "std::basic_string::~basic_string()" in let call_event = PulseDomain.ValueHistory.Call {f= model; location} in match actuals with | [(this_hist, _)] ->