AbstractType of the abstract product of the product domain mapping (optional) property names to abstract domains
Type of the abstract product of the product domain mapping (optional) property names to abstract domains
StaticjoinJoins an array of abstract values by joining the first abstract value with the other values in the array. The provided array of abstract values must not be empty or a default value must be provided!
StaticmeetMeets an array of abstract values by meeting the first abstract value with the other values in the array. The provided array of abstract values must not be empty or a default value must be provided!
StatictoConverts an element of an abstract domain into a string.
Gets the Bottom element (least element) of the complete lattice (should additionally be provided as static function).
AbstractcreateCreates an abstract value of the lattice for a given value.
Optionalreduce: booleanChecks whether the current abstract value equals to another abstract value.
ProtectedequalsChecks whether the current abstract value is the Bottom element of the complete lattice.
Checks whether the current abstract value is the Top element of the complete lattice.
Checks whether the current abstract value is an actual value of the complete lattice (this may include the Top or Bottom element if they are also values and no separate symbols, for example).
Joins the current abstract value with another abstract value by creating the least upper bound (LUB) in the lattice.
Joins the current abstract value with multiple other abstract values.
ProtectedjoinProtectedjsonifyChecks whether the current abstract value is less than or equal to another abstract value with respect to the partial order of the lattice.
ProtectedleqMeets the current abstract value with another abstract value by creating the greatest lower bound (GLB) in the lattice.
Meets the current abstract value with multiple other abstract values.
ProtectedmeetNarrows the current abstract value with another abstract value as a sound over-approximation of the meet (greatest lower bound) to refine the value after widening.
ProtectednarrowProtectedreduceApplies the reductions of the (reduced) product domain to refine the abstract value based on its components. Subclasses may override this to implement a fixed reduction instead of (or in addition to) the configurable reductions.
ProtectedstringifyConverts the lattice into a JSON serializable value.
Gets the Top element (greatest element) of the complete lattice (should additionally be provided as static function).
Converts the lattice into a human-readable string.
Widens the current abstract value with another abstract value as a sound over-approximation of the join (least upper bound) for fixpoint iteration acceleration.
Protectedwiden
A partial product abstract domain as named Cartesian product of (optional) sub abstract domains. The sub abstract domains are represented by a (partial) record mapping property names to abstract domains. The Bottom element is defined as mapping every sub abstract domain to Bottom and the Top element is defined as having no sub abstract domain value.