package mopsa

  1. Overview
  2. Docs
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/Query/index.html

Module Core.QuerySource

Generic query mechanism for extracting information from domains.

Sourcetype ('a, _) query = ..

Extensible type of queries

Sourceval join_query : ?ctx:'a Context.ctx option -> ?lattice:'a Lattice.lattice option -> ('a, 'r) query -> 'r -> 'r -> 'r

Join two queries

Sourceval meet_query : ?ctx:'a Context.ctx option -> ?lattice:'a Lattice.lattice option -> ('a, 'r) query -> 'r -> 'r -> 'r

Meet two queries

Registration

****************

Sourcetype query_pool = {
  1. pool_join : 'a 'r. ('a, 'r) query -> 'r -> 'r -> 'r;
  2. pool_meet : 'a 'r. ('a, 'r) query -> 'r -> 'r -> 'r;
}

Pool of registered queries

Sourcetype query_info = {
  1. join : 'a 'r. query_pool -> ('a, 'r) query -> 'r -> 'r -> 'r;
  2. meet : 'a 'r. query_pool -> ('a, 'r) query -> 'r -> 'r -> 'r;
}

Registraction info for new queries

Sourceval register_query : query_info -> unit

Register a new query

Sourcetype lattice_query_pool = {
  1. pool_join : 'a 'r. 'a Context.ctx -> 'a Lattice.lattice -> ('a, 'r) query -> 'r -> 'r -> 'r;
  2. pool_meet : 'a 'r. 'a Context.ctx -> 'a Lattice.lattice -> ('a, 'r) query -> 'r -> 'r -> 'r;
}

Pool of registered lattice queries. Lattice queries are queries that return elements of the global abstract state lattice. Join/meet operators are enriched with the lattice and the context so that we can compute join/meet over the abstract elements.

Sourcetype lattice_query_info = {
  1. join : 'a 'r. lattice_query_pool -> 'a Context.ctx -> 'a Lattice.lattice -> ('a, 'r) query -> 'r -> 'r -> 'r;
  2. meet : 'a 'r. lattice_query_pool -> 'a Context.ctx -> 'a Lattice.lattice -> ('a, 'r) query -> 'r -> 'r -> 'r;
}

Registration info for new lattice queries

Sourceval register_lattice_query : lattice_query_info -> unit

Register a new lattice query

Common queries

******************

Sourcetype query +=
  1. | Q_defined_variables : string option -> ('a, Ast.Var.var list) query
    (*

    Extract the list of defined variables, in a given function call site, or in all scopes

    *)
  2. | Q_allocated_addresses : ('a, Ast.Addr.addr list) query
    (*

    Query to extract the list of addresses allocated in the heap

    *)
  3. | Q_variables_linked_to : Ast.Expr.expr -> ('a, Ast.Var.VarSet.t) query
    (*

    Query to extract the auxiliary variables related to an expression

    *)