package mopsa

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

Generic query mechanism for extracting information from domains.

type ('a, _) query = ..

Extensible type of queries

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

Join two queries

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

Meet two queries

Registration

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

type 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

type 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

val register_query : query_info -> unit

Register a new query

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

type 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

val register_lattice_query : lattice_query_info -> unit

Register a new lattice query

Common queries

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

type 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

    *)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct