package mopsa
MOPSA: A Modular and Open Platform for Static Analysis using Abstract Interpretation
Install
Dune Dependency
Authors
Maintainers
Sources
mopsa-analyzer-v1.1.tar.gz
md5=fdee20e988343751de440b4f6b67c0f4
sha512=f5cbf1328785d3f5ce40155dada2d95e5de5cce4f084ea30cfb04d1ab10cc9403a26cfb3fa55d0f9da72244482130fdb89c286a9aed0d640bba46b7c00e09500
doc/src/core/manager.ml.html
Source file manager.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105
(****************************************************************************) (* *) (* This file is part of MOPSA, a Modular Open Platform for Static Analysis. *) (* *) (* Copyright (C) 2017-2019 The MOPSA Project. *) (* *) (* This program is free software: you can redistribute it and/or modify *) (* it under the terms of the GNU Lesser General Public License as published *) (* by the Free Software Foundation, either version 3 of the License, or *) (* (at your option) any later version. *) (* *) (* This program is distributed in the hope that it will be useful, *) (* but WITHOUT ANY WARRANTY; without even the implied warranty of *) (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) (* GNU Lesser General Public License for more details. *) (* *) (* You should have received a copy of the GNU Lesser General Public License *) (* along with this program. If not, see <http://www.gnu.org/licenses/>. *) (* *) (****************************************************************************) (** Manager - access to the top-level lattice and transfer functions *) open Ast.Stmt open Ast.Expr open Ast.Semantic open Lattice open Flow open Eval open Post open Cases open Route open Query open Print open Token open Path open Change (*==========================================================================*) (** {2 Managers} *) (*==========================================================================*) (** 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). *) type ('a, 't) man = { lattice : 'a lattice; (** Access to lattice operators on the toplevel abstract element ['a]. *) (** {3 Accessors to domain's abstract element} Each domain can get and set its abstract element in the transfer functions with [get] and [set]. *) get : token -> 'a flow -> ('a, 't) cases; (** Returns the domain's abstract element ['t]. A disjunction of cases is returned when partitioning is used. *) set : token -> 't -> 'a flow -> 'a post; (** Sets the domain's abstract element ['t]. *) (** {3 Toplevel Transfer Functions} The domains access the top-level lattice transfer function through the manager with these functions. It is possible to ask the manager to route the transfer functions (e.g. [eval]) to different domains with the optional [?route] parameter. If [?route] is not set, the routing starts from the root of the domains DAG. *) exec : ?route:route -> stmt -> 'a flow -> 'a post; (** [man.exec stmt flow] executes [stmt] in [flow] and returns the post state. *) eval : ?route:route -> ?translate:semantic -> ?translate_when:(semantic*(expr->bool)) list -> expr -> 'a flow -> 'a eval; (** [man.eval expr flow] evaluates [expr] in [flow] and returns the result expression. There are two kinds of evaluations: within the same semantic (simplifications), or to another semantic (translations). Calling [man.eval expr flow] performs both kinds of evaluations. The result [e'] of [man.eval expr flow] is a {i simplification} of [e] within the same semantic. To retrieve a translation to another semantic, one can use the [?translate] parameter: [man.eval expr flow ~translate:semantic] is a {i translation} of the {i simplification} of [e] in [semantic]. A common use case is to translate expressions to Universal with [man.eval expr flow ~translate:"Universal"]. It is possible to control when the translation is applied with [?translate_when]. *) ask : 'r. ?route:route -> ('a,'r) query -> 'a flow -> ('a, 'r) cases; (** [man.ask query flow] performs a query to other domains. If no domain can answer the query, [man.ask query flow] results in a runtime error. *) print_expr : ?route:route -> 'a flow -> (printer -> expr -> unit); (** [man.print_expr flow] is the expression printer for the type ['a]. *) (** {3 Changes Management} *) add_change : stmt -> path -> 'a flow -> change_map -> change_map; (** Add a statement to the changes map. *) }
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>