Module `InferModules__Tabulation`

type call_result = | CR_success successful call | CR_not_met precondition not met | CR_not_found the callee has no specs | CR_skip the callee was skipped: kind of result of a procedure call

val log_call_trace : caller_name:InferIR.Typ.Procname.t -> callee_name:InferIR.Typ.Procname.t -> ?⁠callee_attributes:InferIR.ProcAttributes.t -> ?⁠reason:string -> ?⁠dynamic_dispatch:InferBase.EventLogger.dynamic_dispatch -> InferBase.Location.t -> call_result -> unit

val remove_constant_string_class : InferIR.Tenv.t -> 'a InferModules.Prop.t -> InferModules.Prop.normal InferModules.Prop.t: Remove constant string or class from a prop

val check_attr_dealloc_mismatch : InferIR.PredSymb.t -> InferIR.PredSymb.t -> unit: Check if the attribute change is a mismatch between a kind of allocation and a different kind of deallocation

val find_dereference_without_null_check_in_sexp : InferIR.Sil.strexp -> (int * InferIR.PredSymb.path_pos) option: Check whether a sexp contains a dereference without null check, and return the line number and path position

val create_cast_exception : InferIR.Tenv.t -> InferBase.Logging.ocaml_pos -> InferIR.Typ.Procname.t option -> InferIR.Exp.t -> InferIR.Exp.t -> InferIR.Exp.t -> exn: raise a cast exception

val prop_is_exn : InferIR.Typ.Procname.t -> 'a InferModules.Prop.t -> bool: check if a prop is an exception

val prop_get_exn_name : InferIR.Typ.Procname.t -> 'a InferModules.Prop.t -> InferIR.Typ.Name.t option: when prop is an exception, return the exception name

val lookup_custom_errors : 'a InferModules.Prop.t -> string option: search in prop contains an error state

val exe_function_call : ?⁠dynamic_dispatch:InferBase.EventLogger.dynamic_dispatch -> InferModules.Exe_env.t -> InferModules.Summary.t -> InferIR.Tenv.t -> InferIR.Ident.t -> InferIR.Procdesc.t -> InferIR.Typ.Procname.t -> InferBase.Location.t -> (InferIR.Exp.t * InferIR.Typ.t) list -> InferModules.Prop.normal InferModules.Prop.t -> InferModules.Paths.Path.t -> (InferModules.Prop.normal InferModules.Prop.t * InferModules.Paths.Path.t) list: Execute the function call and return the list of results with return value

val get_specs_from_payload : InferModules.Summary.t -> InferModules.Prop.normal InferModules.BiabductionSummary.spec list: Get the specs from the payload of the summary.