package mopsa
Install
Dune Dependency
Authors
Maintainers
Sources
md5=9f673f79708b44a7effb3b6bb3618d2c
sha512=cb91cb428e43a22f1abbcb8219710d0c10a5b3756d0da392d4084b3b3a6157350776c596983e63def344f617d39964e91f244f60c07958695ee5c8c809a9f0f4
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.