Module Pulselib.PulseArithmetic

module AbductiveDomain = PulseAbductiveDomain
module AccessResult = PulseAccessResult

Wrapper around PulseFormula that operates on AbductiveDomain.t.

type operand = Pulselib.PulseBasicInterface.Formula.operand =
  1. | AbstractValueOperand of Pulselib.PulseBasicInterface.AbstractValue.t
  2. | ConstOperand of IR.Const.t
  3. | FunctionApplicationOperand of {
    1. f : PulseFormula.function_symbol;
    2. actuals : Pulselib.PulseBasicInterface.AbstractValue.t list;
    }

eval_binop_absval ret binop lhs rhs astate is eval_binop ret binop (AbstractValueOperand lhs) (AbstractValueOperand rhs) astate

helper function wrapping prune_binop

helper function wrapping prune_binop

helper function wrapping prune_binop

helper function wrapping prune_binop

helper function wrapping prune_binop

helper function wrapping prune_binop

val is_manifest : AbductiveDomain.Summary.t -> bool

whether the state is *manifest* according to PulseFormula.is_manifest, with an additional condition that some equalities path conditions may be represented implicitly by having several edges pointing to the same value in the precondition; if the pre exhibits sharing that means some access paths in the precondition are equal, which means that equality on these access paths has been assumed at some point in the function so the set of assumptions is not empty (see also the documentation for PulseFormula.is_manifest and PulseAbductiveDomain.Summary.pre_heap_has_assumptions)

val as_constant_string : AbductiveDomain.t -> Pulselib.PulseBasicInterface.AbstractValue.t -> string option