Pulselib.PulseArithmetic
module AbductiveDomain = PulseAbductiveDomain
module AccessResult = PulseAccessResult
Wrapper 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.t
val and_not_equal :
operand ->
operand ->
AbductiveDomain.t ->
AbductiveDomain.t AccessResult.t Pulselib.PulseBasicInterface.SatUnsat.t
val and_equal_string_concat :
Pulselib.PulseBasicInterface.AbstractValue.t ->
operand ->
operand ->
AbductiveDomain.t ->
AbductiveDomain.t AccessResult.t Pulselib.PulseBasicInterface.SatUnsat.t
val 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.t
eval_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.t
val prune_eq_zero :
Pulselib.PulseBasicInterface.AbstractValue.t ->
AbductiveDomain.t ->
AbductiveDomain.t AccessResult.t Pulselib.PulseBasicInterface.SatUnsat.t
helper function wrapping prune_binop
val prune_ne_zero :
Pulselib.PulseBasicInterface.AbstractValue.t ->
AbductiveDomain.t ->
AbductiveDomain.t AccessResult.t Pulselib.PulseBasicInterface.SatUnsat.t
helper function wrapping prune_binop
val prune_nonnegative :
Pulselib.PulseBasicInterface.AbstractValue.t ->
AbductiveDomain.t ->
AbductiveDomain.t AccessResult.t Pulselib.PulseBasicInterface.SatUnsat.t
helper function wrapping prune_binop
val prune_positive :
Pulselib.PulseBasicInterface.AbstractValue.t ->
AbductiveDomain.t ->
AbductiveDomain.t AccessResult.t Pulselib.PulseBasicInterface.SatUnsat.t
helper function wrapping prune_binop
val prune_gt_one :
Pulselib.PulseBasicInterface.AbstractValue.t ->
AbductiveDomain.t ->
AbductiveDomain.t AccessResult.t Pulselib.PulseBasicInterface.SatUnsat.t
helper function wrapping prune_binop
val prune_eq_one :
Pulselib.PulseBasicInterface.AbstractValue.t ->
AbductiveDomain.t ->
AbductiveDomain.t AccessResult.t Pulselib.PulseBasicInterface.SatUnsat.t
helper function wrapping prune_binop
val is_known_zero :
AbductiveDomain.t ->
Pulselib.PulseBasicInterface.AbstractValue.t ->
bool
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 and_equal_instanceof :
Pulselib.PulseBasicInterface.AbstractValue.t ->
Pulselib.PulseBasicInterface.AbstractValue.t ->
IR.Typ.t ->
?nullable:bool ->
AbductiveDomain.t ->
AbductiveDomain.t AccessResult.t Pulselib.PulseBasicInterface.SatUnsat.t
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.t
val get_dynamic_type :
Pulselib.PulseBasicInterface.AbstractValue.t ->
AbductiveDomain.t ->
Pulselib.PulseBasicInterface.Formula.dynamic_type_data option
val copy_type_constraints :
Pulselib.PulseBasicInterface.AbstractValue.t ->
Pulselib.PulseBasicInterface.AbstractValue.t ->
AbductiveDomain.t ->
AbductiveDomain.t
val and_dynamic_type_is_unsafe :
Pulselib.PulseBasicInterface.AbstractValue.t ->
IR.Typ.t ->
?source_file:IBase.SourceFile.t ->
IBase.Location.t ->
AbductiveDomain.t ->
AbductiveDomain.t
val absval_of_int :
AbductiveDomain.t ->
IR.IntLit.t ->
AbductiveDomain.t * Pulselib.PulseBasicInterface.AbstractValue.t
val absval_of_string :
AbductiveDomain.t ->
string ->
AbductiveDomain.t * Pulselib.PulseBasicInterface.AbstractValue.t
val as_constant_string :
AbductiveDomain.t ->
Pulselib.PulseBasicInterface.AbstractValue.t ->
string option