Module Biabduction.Errdesc

val vpath_find : IR.Tenv.t -> 'a Prop.t -> IR.Exp.t -> IR.DecompiledExp.vpath * IR.Typ.t option

find the dexp, if any, where the given value is stored also return the type of the value if found

val hpred_is_open_resource : IR.Tenv.t -> 'a Prop.t -> Predicates.hpred -> IR.PredSymb.resource option

Check whether the hpred is a |-> representing a resource in the Racquire state

val find_ident_assignment : IR.Procdesc.Node.t -> IR.Ident.t -> (IR.Procdesc.Node.t * IR.Exp.t) option

Find a program variable assignment to id in the current node or predecessors.

val exp_rv_dexp : IR.Tenv.t -> IR.Procdesc.Node.t -> IR.Exp.t -> IR.DecompiledExp.t option

describe rvalue e as a dexp

val explain_array_access : IR.Procname.t -> IR.Tenv.t -> Absint.Localise.deref_str -> 'a Prop.t -> IBase.Location.t -> Absint.Localise.error_desc

Produce a description of the array access performed in the current instruction, if any.

val explain_class_cast_exception : IR.Tenv.t -> IR.Procname.t option -> IR.Exp.t -> IR.Exp.t -> IR.Exp.t -> IR.Procdesc.Node.t -> IBase.Location.t -> Absint.Localise.error_desc

explain a class cast exception

val explain_dereference : IR.Procname.t -> IR.Tenv.t -> ?⁠use_buckets:bool -> ?⁠is_nullable:bool -> ?⁠is_premature_nil:bool -> Absint.Localise.deref_str -> 'a Prop.t -> IBase.Location.t -> Absint.Localise.error_desc

Produce a description of which expression is dereferenced in the current instruction, if any.

val explain_dereference_as_caller_expression : IR.Procname.t -> IR.Tenv.t -> ?⁠use_buckets:bool -> Absint.Localise.deref_str -> 'a Prop.t -> 'b Prop.t -> IR.Exp.t -> IR.Procdesc.Node.t -> IBase.Location.t -> IR.Pvar.t list -> Absint.Localise.error_desc

return a description explaining value exp in prop in terms of a source expression using the formal parameters of the call

val explain_divide_by_zero : IR.Tenv.t -> IR.Exp.t -> IR.Procdesc.Node.t -> IBase.Location.t -> Absint.Localise.error_desc

explain a division by zero

val explain_condition_always_true_false : IR.Tenv.t -> IR.IntLit.t -> IR.Exp.t -> IR.Procdesc.Node.t -> IBase.Location.t -> Absint.Localise.error_desc

explain a condition which is always true or false

val explain_unary_minus_applied_to_unsigned_expression : IR.Tenv.t -> IR.Exp.t -> IR.Typ.t -> IR.Procdesc.Node.t -> IBase.Location.t -> Absint.Localise.error_desc

explain unary minus applied to unsigned expression

val explain_leak : IR.Tenv.t -> Predicates.hpred -> 'a Prop.t -> IR.PredSymb.t option -> string option -> bool * Absint.Localise.error_desc

Produce a description of a leak by looking at the current state. If the current instruction is a variable nullify, blame the variable. If it is an abstraction, blame any variable nullify at the current node. If there is an alloc attribute, print the function call and line number.

val warning_err : IBase.Location.t -> ('a, Stdlib.Format.formatter, unit) IStdlib.IStd.format -> 'a

warn at the given location

val find_outermost_dereference : IR.Tenv.t -> IR.Procdesc.Node.t -> IR.Exp.t -> IR.DecompiledExp.t option
val access_opt : ?⁠is_nullable:bool -> Predicates.inst -> Absint.Localise.access option