package mopsa
Install
Dune Dependency
Authors
Maintainers
Sources
md5=9f673f79708b44a7effb3b6bb3618d2c
sha512=cb91cb428e43a22f1abbcb8219710d0c10a5b3756d0da392d4084b3b3a6157350776c596983e63def344f617d39964e91f244f60c07958695ee5c8c809a9f0f4
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 : 'a -> 't;(*Returns the domain's abstract element
*)'t.set : 't -> 'a -> 'a;(*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.get_effects : Effect.teffect -> Effect.teffect;(*Gets the effects tree.
*)set_effects : Effect.teffect -> Effect.teffect -> Effect.teffect;(*Sets the effect tree.
*)
}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).