package mopsa
Install
Dune Dependency
Authors
Maintainers
Sources
md5=9f673f79708b44a7effb3b6bb3618d2c
sha512=cb91cb428e43a22f1abbcb8219710d0c10a5b3756d0da392d4084b3b3a6157350776c596983e63def344f617d39964e91f244f60c07958695ee5c8c809a9f0f4
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
*)