Pulselib.PulseArithmeticmodule AbductiveDomain = PulseAbductiveDomainmodule AccessResult = PulseAccessResultWrapper around PulseFormula that operates on AbductiveDomain.t.
type operand = Pulselib.PulseBasicInterface.Formula.operand = | AbstractValueOperand of Pulselib.PulseBasicInterface.AbstractValue.t| ConstOperand of IR.Const.t| FunctionApplicationOperand of {f : PulseFormula.function_symbol;actuals : Pulselib.PulseBasicInterface.AbstractValue.t list;}val and_equal :
operand ->
operand ->
AbductiveDomain.t ->
AbductiveDomain.t AccessResult.t Pulselib.PulseBasicInterface.SatUnsat.tval and_not_equal :
operand ->
operand ->
AbductiveDomain.t ->
AbductiveDomain.t AccessResult.t Pulselib.PulseBasicInterface.SatUnsat.tval eval_binop_absval :
Pulselib.PulseBasicInterface.AbstractValue.t ->
IR.Binop.t ->
Pulselib.PulseBasicInterface.AbstractValue.t ->
Pulselib.PulseBasicInterface.AbstractValue.t ->
AbductiveDomain.t ->
(AbductiveDomain.t * Pulselib.PulseBasicInterface.AbstractValue.t)
AccessResult.t
Pulselib.PulseBasicInterface.SatUnsat.teval_binop_absval ret binop lhs rhs astate is eval_binop ret binop (AbstractValueOperand lhs) (AbstractValueOperand rhs) astate
val prune_binop :
negated:bool ->
IR.Binop.t ->
operand ->
operand ->
AbductiveDomain.t ->
AbductiveDomain.t AccessResult.t Pulselib.PulseBasicInterface.SatUnsat.tval prune_eq_zero :
Pulselib.PulseBasicInterface.AbstractValue.t ->
AbductiveDomain.t ->
AbductiveDomain.t AccessResult.t Pulselib.PulseBasicInterface.SatUnsat.thelper function wrapping prune_binop
val prune_ne_zero :
Pulselib.PulseBasicInterface.AbstractValue.t ->
AbductiveDomain.t ->
AbductiveDomain.t AccessResult.t Pulselib.PulseBasicInterface.SatUnsat.thelper function wrapping prune_binop
val prune_nonnegative :
Pulselib.PulseBasicInterface.AbstractValue.t ->
AbductiveDomain.t ->
AbductiveDomain.t AccessResult.t Pulselib.PulseBasicInterface.SatUnsat.thelper function wrapping prune_binop
val prune_positive :
Pulselib.PulseBasicInterface.AbstractValue.t ->
AbductiveDomain.t ->
AbductiveDomain.t AccessResult.t Pulselib.PulseBasicInterface.SatUnsat.thelper function wrapping prune_binop
val prune_gt_one :
Pulselib.PulseBasicInterface.AbstractValue.t ->
AbductiveDomain.t ->
AbductiveDomain.t AccessResult.t Pulselib.PulseBasicInterface.SatUnsat.thelper function wrapping prune_binop
val prune_eq_one :
Pulselib.PulseBasicInterface.AbstractValue.t ->
AbductiveDomain.t ->
AbductiveDomain.t AccessResult.t Pulselib.PulseBasicInterface.SatUnsat.thelper function wrapping prune_binop
val is_known_zero :
AbductiveDomain.t ->
Pulselib.PulseBasicInterface.AbstractValue.t ->
boolval is_manifest : AbductiveDomain.Summary.t -> boolwhether 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 and_equal_instanceof :
Pulselib.PulseBasicInterface.AbstractValue.t ->
Pulselib.PulseBasicInterface.AbstractValue.t ->
IR.Typ.t ->
tenv:IR.Tenv.t ->
AbductiveDomain.t ->
AbductiveDomain.t AccessResult.t Pulselib.PulseBasicInterface.SatUnsat.tval absval_of_int :
AbductiveDomain.t ->
IR.IntLit.t ->
AbductiveDomain.t * Pulselib.PulseBasicInterface.AbstractValue.t