package mopsa
Install
Dune Dependency
Authors
Maintainers
Sources
md5=fdee20e988343751de440b4f6b67c0f4
sha512=f5cbf1328785d3f5ce40155dada2d95e5de5cce4f084ea30cfb04d1ab10cc9403a26cfb3fa55d0f9da72244482130fdb89c286a9aed0d640bba46b7c00e09500
doc/value/Value/Product/index.html
Module Value.ProductSource
Reduced product of value abstractions.
This combiner implements a reduced product between 𝑚 value abstractions 𝒱₁, ..., 𝒱ₘ. Each abstraction 𝒱ᵢ represent values of types 𝐓ᵢ, such that: ∀ j ≠ i: 𝐓ᵢ ∩ 𝐓ⱼ ≠ ∅. The types represented by the combiner is 𝐓₁ ∩ ... ∩ 𝐓ₘ.
The reduced is represented with a cartesian product. The concretization of a product of values is the intersection of the concretizations: γ(v₁,...,vₘ) = γ₁(v₁) ∩ ... ∩ γₘ(vₘ).
The reduced product is parameterized by a set of reduction rules ρ₁, ..., ρₖ. Each reduction rule is applied after each transfer function. Note that reduction rules can access to all abstractions and can reduce many values at the same time.
module MakeValuePair
(V1 : Sig.Abstraction.Value.VALUE)
(V2 : Sig.Abstraction.Value.VALUE) :
Sig.Abstraction.Value.VALUE with type t = V1.t * V2.tCreate a pair of two value abstractions.
module Make
(V : Sig.Abstraction.Value.VALUE)
(R : sig ... end) :
Sig.Abstraction.Value.VALUE with type t = V.tCreate a reduced product from an n-tuple value abstraction and a list of reduction rules.
val make :
(module Sig.Abstraction.Value.VALUE) list ->
(module Sig.Reduction.Value.VALUE_REDUCTION) list ->
(module Sig.Abstraction.Value.VALUE)Create a reduced product from a list of value abstractions and a list of reduction rules.