package mopsa

  1. Overview
  2. Docs
MOPSA: A Modular and Open Platform for Static Analysis using Abstract Interpretation

Install 

dune-project
 Dependency

mopsa.lip6.fr Readme Changelog Edit opam file Versions (3)

Authors

  1. A
    Antoine Miné
  2. A
    Abdelraouf Ouadjaout
  3. M
    Matthieu Journault
  4. A
    Aymeric Fromherz
  5. R
    Raphaël Monat
  6. F
    Francesco Parolini
  7. M
    Marco Milanese
  8. J
    Jérôme Boillot

Maintainers

  1. A
    Antoine Miné <antoine.mine@lip6.fr>
  2. A
    Abdelraouf Ouadjaout <ouadjaout@gmail.com>
  3. R
    Raphaël Monat <raphael.monat@inria.fr>

Sources

mopsa-analyzer-v1.1.tar.gz
md5=fdee20e988343751de440b4f6b67c0f4
sha512=f5cbf1328785d3f5ce40155dada2d95e5de5cce4f084ea30cfb04d1ab10cc9403a26cfb3fa55d0f9da72244482130fdb89c286a9aed0d640bba46b7c00e09500

doc/abstraction/Abstraction/Simplified/index.html

Module Abstraction.SimplifiedSource

Simplified domains

The signature SIMPLIFIED provides a minimal interface to implement abstract domains that don't require communication with other domains. This is particularly useful for abstractions that are at the leaves of the abstraction DAG.

Lattice operations and transfer functions operate on the abstract element of the domain without being able to access to the top-level abstraction. The manager is therefore not accessible, only a simplified version is provided that can be used to perform queries on the pre-state.

Simplified manager

Sourcetype ('a, 't) simplified_man = {
  1. exec : Core.All.stmt -> 't;
    (*

    execute a statement on the pre-state

    *)
  2. ask : 'r. ('a, 'r) Core.All.query -> 'r;
    (*

    ask a query on the pre-state

    *)
}

Simplified managers provide access to the pre-state and can be used to perform queries or execute statements.

Signature

Sourcemodule type SIMPLIFIED = sig ... end

Registration

Sourceval register_simplified_domain : (module SIMPLIFIED) -> unit

Register a new simplified domain

Sourceval find_simplified_domain : string -> (module SIMPLIFIED)

Find a simplified domain by its name. Raise Not_found if no domain is found

Sourceval mem_simplified_domain : string -> bool

mem_simplified_domain name checks whether a simplified domain with name name is registered

Sourceval simplified_domain_names : unit -> string list

Return the names of registered simplified domains