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 and_equal_string_concat :
Pulselib.PulseBasicInterface.AbstractValue.t ->
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_dynamic_type_is :
Pulselib.PulseBasicInterface.AbstractValue.t ->
IR.Typ.t ->
?source_file:IBase.SourceFile.t ->
AbductiveDomain.t ->
AbductiveDomain.t AccessResult.t Pulselib.PulseBasicInterface.SatUnsat.tval get_dynamic_type :
Pulselib.PulseBasicInterface.AbstractValue.t ->
AbductiveDomain.t ->
Pulselib.PulseBasicInterface.Formula.dynamic_type_data optionval copy_type_constraints :
Pulselib.PulseBasicInterface.AbstractValue.t ->
Pulselib.PulseBasicInterface.AbstractValue.t ->
AbductiveDomain.t ->
AbductiveDomain.tval and_dynamic_type_is_unsafe :
Pulselib.PulseBasicInterface.AbstractValue.t ->
IR.Typ.t ->
?source_file:IBase.SourceFile.t ->
AbductiveDomain.t ->
AbductiveDomain.tval absval_of_int :
AbductiveDomain.t ->
IR.IntLit.t ->
AbductiveDomain.t * Pulselib.PulseBasicInterface.AbstractValue.tval absval_of_string :
AbductiveDomain.t ->
string ->
AbductiveDomain.t * Pulselib.PulseBasicInterface.AbstractValue.tval as_constant_string :
AbductiveDomain.t ->
Pulselib.PulseBasicInterface.AbstractValue.t ->
string option