package mopsa
Install
Dune Dependency
Authors
Maintainers
Sources
md5=fdee20e988343751de440b4f6b67c0f4
sha512=f5cbf1328785d3f5ce40155dada2d95e5de5cce4f084ea30cfb04d1ab10cc9403a26cfb3fa55d0f9da72244482130fdb89c286a9aed0d640bba46b7c00e09500
doc/core/Core/Query/index.html
Module Core.QuerySource
Generic query mechanism for extracting information from domains.
Extensible type of queries
val join_query :
?ctx:'a Context.ctx option ->
?lattice:'a Lattice.lattice option ->
('a, 'r) query ->
'r ->
'r ->
'rJoin two queries
val meet_query :
?ctx:'a Context.ctx option ->
?lattice:'a Lattice.lattice option ->
('a, 'r) query ->
'r ->
'r ->
'rMeet two queries
Registration
****************
type query_pool = {pool_join : 'a 'r. ('a, 'r) query -> 'r -> 'r -> 'r;pool_meet : 'a 'r. ('a, 'r) query -> 'r -> 'r -> 'r;
}Pool of registered queries
type query_info = {join : 'a 'r. query_pool -> ('a, 'r) query -> 'r -> 'r -> 'r;meet : 'a 'r. query_pool -> ('a, 'r) query -> 'r -> 'r -> 'r;
}Registraction info for new queries
Register a new query
type lattice_query_pool = {pool_join : 'a 'r. 'a Context.ctx -> 'a Lattice.lattice -> ('a, 'r) query -> 'r -> 'r -> 'r;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 = {join : 'a 'r. lattice_query_pool -> 'a Context.ctx -> 'a Lattice.lattice -> ('a, 'r) query -> 'r -> 'r -> 'r;meet : 'a 'r. lattice_query_pool -> 'a Context.ctx -> 'a Lattice.lattice -> ('a, 'r) query -> 'r -> 'r -> 'r;
}Registration info for new lattice queries
Register a new lattice query
Common queries
******************
type query += | 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
*)| Q_allocated_addresses : ('a, Ast.Addr.addr list) query(*Query to extract the list of addresses allocated in the heap
*)| Q_variables_linked_to : Ast.Expr.expr -> ('a, Ast.Var.VarSet.t) query(*Query to extract the auxiliary variables related to an expression
*)