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

gitlab.com 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.0.tar.gz
md5=9f673f79708b44a7effb3b6bb3618d2c
sha512=cb91cb428e43a22f1abbcb8219710d0c10a5b3756d0da392d4084b3b3a6157350776c596983e63def344f617d39964e91f244f60c07958695ee5c8c809a9f0f4

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 : 'a -> 't;
    (*

    Returns the domain's abstract element 't.

    *)
  3. set : 't -> 'a -> 'a;
    (*

    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. get_effects : Effect.teffect -> Effect.teffect;
    (*

    Gets the effects tree.

    *)
  9. set_effects : Effect.teffect -> Effect.teffect -> Effect.teffect;
    (*

    Sets the effect tree.

    *)
}

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).