diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 38142919b..ad44db671 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -11,7 +11,7 @@ open Result.Monad_infix open PulseBasicInterface let report summary diagnostic = - let open PulseDiagnostic in + let open Diagnostic in Reporting.log_error summary ~loc:(get_location diagnostic) ~ltr:(get_trace diagnostic) (get_issue_type diagnostic) (get_message diagnostic) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index a0b977be2..0bcb6bb1c 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -442,8 +442,7 @@ module PrePost = struct let access_trace = add_call callee_access_trace in match Memory.check_valid access_trace (fst addr_hist_caller) call_state.astate with | Error invalidated_by -> - Error - (PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= access_trace}) + Error (Diagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= access_trace}) | Ok astate -> let call_state = {call_state with astate} in Container.fold_result diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 9d2580e04..fc51f1e5d 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -95,7 +95,7 @@ module PrePost : sig -> formals:Var.t list -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list -> domain_t - -> (domain_t * (AbstractValue.t * ValueHistory.t) option, PulseDiagnostic.t) result + -> (domain_t * (AbstractValue.t * ValueHistory.t) option, Diagnostic.t) result (** return the abstract state after the call along with an optional return value *) end diff --git a/infer/src/pulse/PulseBasicInterface.ml b/infer/src/pulse/PulseBasicInterface.ml index e865d95a4..aa645bc06 100644 --- a/infer/src/pulse/PulseBasicInterface.ml +++ b/infer/src/pulse/PulseBasicInterface.ml @@ -12,6 +12,7 @@ module AbstractValue = PulseAbstractValue module Attribute = PulseAttribute module Attributes = PulseAttribute.Attributes module CallEvent = PulseCallEvent +module Diagnostic = PulseDiagnostic module Invalidation = PulseInvalidation module Trace = PulseTrace module ValueHistory = PulseValueHistory diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index 2ef3548cf..c0ec6bf0d 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -7,7 +7,10 @@ open! IStd module F = Format -open PulseBasicInterface +module CallEvent = PulseCallEvent +module Invalidation = PulseInvalidation +module Trace = PulseTrace +module ValueHistory = PulseValueHistory type t = | AccessToInvalidAddress of {invalidated_by: Invalidation.t Trace.t; accessed_by: unit Trace.t} diff --git a/infer/src/pulse/PulseDiagnostic.mli b/infer/src/pulse/PulseDiagnostic.mli index 1b667e644..d2944af97 100644 --- a/infer/src/pulse/PulseDiagnostic.mli +++ b/infer/src/pulse/PulseDiagnostic.mli @@ -6,7 +6,9 @@ *) open! IStd -open PulseBasicInterface +module Invalidation = PulseInvalidation +module Trace = PulseTrace +module ValueHistory = PulseValueHistory (** an error to report to the user *) type t = diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 8f23d9f97..20e126892 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -12,14 +12,14 @@ open PulseDomainInterface type t = AbductiveDomain.t -type 'a access_result = ('a, PulseDiagnostic.t) result +type 'a access_result = ('a, Diagnostic.t) result (** Check that the [address] is not known to be invalid *) let check_addr_access location (address, history) astate = let accessed_by = Trace.Immediate {imm= (); location; history} in Memory.check_valid accessed_by address astate |> Result.map_error ~f:(fun invalidated_by -> - PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by} ) + Diagnostic.AccessToInvalidAddress {invalidated_by; accessed_by} ) module Closures = struct @@ -304,7 +304,7 @@ let check_address_escape escape_location proc_desc address history astate = (* The returned address corresponds to a C++ temporary. It will have gone out of scope by now except if it was bound to a global. *) Error - (PulseDiagnostic.StackVariableAddressEscape + (Diagnostic.StackVariableAddressEscape {variable; location= escape_location; history}) | _ -> Ok () ) ) @@ -322,8 +322,7 @@ let check_address_escape escape_location proc_desc address history astate = L.d_printfln_escaped "Stack variable address &%a detected at address %a" Var.pp variable AbstractValue.pp address ; Error - (PulseDiagnostic.StackVariableAddressEscape - {variable; location= escape_location; history}) ) + (Diagnostic.StackVariableAddressEscape {variable; location= escape_location; history}) ) else Ok () ) in check_address_of_cpp_temporary () >>= check_address_of_stack_variable >>| fun () -> astate diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 420582d89..37b01b099 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -11,11 +11,10 @@ open PulseDomainInterface type t = PulseAbductiveDomain.t -type 'a access_result = ('a, PulseDiagnostic.t) result +type 'a access_result = ('a, Diagnostic.t) result module Closures : sig - val check_captured_addresses : - Location.t -> AbstractValue.t -> t -> (t, PulseDiagnostic.t) result + val check_captured_addresses : Location.t -> AbstractValue.t -> t -> (t, Diagnostic.t) result (** assert the validity of the addresses captured by the lambda *) end