package mopsa

  1. Overview
  2. Docs
On This Page
  1. Managers
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/core/Core/Manager/index.html

Module Core.ManagerSource

Manager - access to the top-level lattice and transfer functions

Managers

Sourcetype ('a, 't) man = {
  1. lattice : 'a Lattice.lattice;
    (*

    Access to lattice operators on the toplevel abstract element 'a.

    *)
  2. get : Token.token -> 'a Flow.flow -> ('a, 't) Cases.cases;
    (*

    Returns the domain's abstract element 't. A disjunction of cases is returned when partitioning is used.

    *)
  3. set : Token.token -> 't -> 'a Flow.flow -> 'a Post.post;
    (*

    Sets the domain's abstract element 't.

    *)
  4. exec : ?route:Route.route -> Ast.Stmt.stmt -> 'a Flow.flow -> 'a Post.post;
    (*

    man.exec stmt flow executes stmt in flow and returns the post state.

    *)
  5. eval : ?route:Route.route -> ?translate:Ast.Semantic.semantic -> ?translate_when:(Ast.Semantic.semantic * (Ast.Expr.expr -> bool)) list -> Ast.Expr.expr -> 'a Flow.flow -> 'a Eval.eval;
    (*

    man.eval expr flow evaluates expr in flow and returns the result expression.

    There are two kinds of evaluations: within the same semantic (simplifications), or to another semantic (translations). Calling man.eval expr flow performs both kinds of evaluations. The result e' of man.eval expr flow is a simplification of e within the same semantic. To retrieve a translation to another semantic, one can use the ?translate parameter: man.eval expr flow ~translate:semantic is a translation of the simplification of e in semantic. A common use case is to translate expressions to Universal with man.eval expr flow ~translate:"Universal". It is possible to control when the translation is applied with ?translate_when.

    *)
  6. ask : 'r. ?route:Route.route -> ('a, 'r) Query.query -> 'a Flow.flow -> ('a, 'r) Cases.cases;
    (*

    man.ask query flow performs a query to other domains. If no domain can answer the query, man.ask query flow results in a runtime error.

    *)
  7. print_expr : ?route:Route.route -> 'a Flow.flow -> Print.printer -> Ast.Expr.expr -> unit;
    (*

    man.print_expr flow is the expression printer for the type 'a.

    *)
  8. add_change : Ast.Stmt.stmt -> Path.path -> 'a Flow.flow -> Change.change_map -> Change.change_map;
    (*

    Add a statement to the changes map.

    *)
}

Managers provide access to full analyzer.

'a is the type of the toplevel abstract element, and 't is the type of local abstract element (that is, the type of the domain that calls the manager).