package mopsa
Install
Dune Dependency
Authors
Maintainers
Sources
md5=fdee20e988343751de440b4f6b67c0f4
sha512=f5cbf1328785d3f5ce40155dada2d95e5de5cce4f084ea30cfb04d1ab10cc9403a26cfb3fa55d0f9da72244482130fdb89c286a9aed0d640bba46b7c00e09500
doc/core/Core/Manager/index.html
Module Core.ManagerSource
Manager - access to the top-level lattice and transfer functions
Managers
type ('a, 't) man = {lattice : 'a Lattice.lattice;(*Access to lattice operators on the toplevel abstract element
*)'a.get : Token.token -> 'a Flow.flow -> ('a, 't) Cases.cases;(*Returns the domain's abstract element
*)'t. A disjunction of cases is returned when partitioning is used.set : Token.token -> 't -> 'a Flow.flow -> 'a Post.post;(*Sets the domain's abstract element
*)'t.exec : ?route:Route.route -> Ast.Stmt.stmt -> 'a Flow.flow -> 'a Post.post;(*
*)man.exec stmt flowexecutesstmtinflowand returns the post state.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 flowevaluatesexprinflowand returns the result expression.There are two kinds of evaluations: within the same semantic (simplifications), or to another semantic (translations). Calling
*)man.eval expr flowperforms both kinds of evaluations. The resulte'ofman.eval expr flowis a simplification ofewithin the same semantic. To retrieve a translation to another semantic, one can use the?translateparameter:man.eval expr flow ~translate:semanticis a translation of the simplification ofeinsemantic. A common use case is to translate expressions to Universal withman.eval expr flow ~translate:"Universal". It is possible to control when the translation is applied with?translate_when.ask : 'r. ?route:Route.route -> ('a, 'r) Query.query -> 'a Flow.flow -> ('a, 'r) Cases.cases;(*
*)man.ask query flowperforms a query to other domains. If no domain can answer the query,man.ask query flowresults in a runtime error.print_expr : ?route:Route.route -> 'a Flow.flow -> Print.printer -> Ast.Expr.expr -> unit;(*
*)man.print_expr flowis the expression printer for the type'a.add_change : Ast.Stmt.stmt -> Path.path -> 'a Flow.flow -> Change.change_map -> Change.change_map;(*Add a statement to the changes map.
*)
}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).