Make_LOffset._
val default_offsetmap : Base.t -> Offsetmap.t Lattice_bounds.or_bottom
Value returned when a map is queried, and the base is not present. `Bottom
indicates that the base is never bound in such a map.
val default_contents : V.t default_contents
This function is used to optimize functions that add keys in a map, in particular when maintaining canonicity w.r.t. default contents. It describes the contents c
of the offsetmap resulting from default_offsetmap b
. The possible values are:
Bottom
means that c
is V.bottom
everywhere, and furthermore that V.bottom
has an empty concretization. We deduce from this fact that unmapped keys do not contribute to a join, and that join c v
is never c
as soon as v
is not itself v
.Top
means that c
is V.top
everywhere. Thus unmapped keys have a default value more general than the one in a map where the key is bound.`Constant v
means that c
is an offsetmap with a single interval containing v
everywhere. v
must be isotropic (in the sense of V.is_isotropic
).`Other
means that default_offsetmap
returns something arbitrary.This function is only used on keys that change values. Thus it is safe to have default_offsetmap
return something that do not match default_contents
on constant keys.