package mopsa

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

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.

Create a pair of two value abstractions.

module Make (V : Sig.Abstraction.Value.VALUE) (R : sig ... end) : Sig.Abstraction.Value.VALUE with type t = V.t

Create a reduced product from an n-tuple value abstraction and a list of reduction rules.

Create a reduced product from a list of value abstractions and a list of reduction rules.

OCaml

Innovation. Community. Security.