package mopsa

  1. Overview
  2. Docs
package mopsa
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Packing.Static

Packing functor with static strategy.

This functor lifts an abstract domain to a set of packs with fewer dimensions. Users of the functor need to define a static strategy that gives the packs of a given variable.

The packs are represented as a map from packing keys to abstract elements. Lattice operators are defined pointwise. To compute the post-state of a statement, the functor inspects the statement to extract the affected variables, and propagate the (modified) statement to the appropriate pack.

module type STRATEGY = sig ... end

Signature of a static packing strategy

type MopsaLib.id +=
  1. | D_static_packing : 'k MopsaLib.id * 'a MopsaLib.id -> ('k, 'a) Framework.Lattices.Partial_map.map MopsaLib.id

Identifier of packed domains

Creation of a domain functor from a packing strategy

val register_strategy : (module STRATEGY) -> unit