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/abstraction/stacked.ml.html
Source file stacked.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 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165
(****************************************************************************) (* *) (* 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/>. *) (* *) (****************************************************************************) (** Signature of stacked domains *) open Core.All open Mopsa_utils (*==========================================================================*) (** {2 Signature} *) (*==========================================================================*) module type STACKED = sig (** {2 Domain header} *) (** ***************** *) type t (** Type of an abstract elements. *) val id : t id (** Domain identifier *) val name : string (** Name of the domain *) val checks : check list (** List of checks performed by the domain *) val bottom: t (** Least abstract element of the lattice. *) val top: t (** Greatest abstract element of the lattice. *) val is_bottom: t -> bool (** [is_bottom a] tests whether [a] is bottom or not. *) (** {2 Lattice operators} *) (** ********************* *) val subset: ('a,t) man -> 'a ctx -> t * 'a -> t * 'a -> bool * 'a * 'a val join : ('a,t) man -> 'a ctx -> t * 'a -> t * 'a -> t * 'a * 'a val meet : ('a,t) man -> 'a ctx -> t * 'a -> t * 'a -> t * 'a * 'a val widen : ('a,t) man -> 'a ctx -> t * 'a -> t * 'a -> t * 'a * 'a * bool val merge : t -> t * change -> t * change -> t (** [merge pre (post1, change1) (post2, change2)] synchronizes two divergent post-conditions [post1] and [post2] using a common pre-condition [pre]. Diverging post-conditions emerge after a fork-join trajectory in the abstraction DAG (e.g., a reduced product). The changes [change1] and [change2] represent a journal of internal statements executed during the the computation of the post-conditions over the two trajectories. *) (** {2 Transfer functions} *) (** ********************** *) val init : program -> ('a, t) man -> 'a flow -> 'a post option (** Initialization function *) val exec : stmt -> ('a,t) man -> 'a flow -> 'a post option (** Post-state of statements *) val eval : expr -> ('a,t) man -> 'a flow -> 'a eval option (** Evaluation of expressions *) val ask : ('a,'r) query -> ('a,t) man -> 'a flow -> ('a, 'r) cases option (** Handler of queries *) (** {2 Printing} *) (** ************ *) val print_state : printer -> t -> unit (** Printer of an abstract element. *) val print_expr : ('a,t) man -> 'a flow -> printer -> expr -> unit (** Printer of an expression's value *) end (*==========================================================================*) (** {2 Registration} *) (*==========================================================================*) (** Instrument transfer functions with some useful pre/post processing *) module Instrument(D:STACKED) : STACKED with type t = D.t = struct include D (* Add stmt to the changes of the domain *) let exec stmt man flow = if is_change_tracker_enabled () then D.exec stmt man flow |> OptionExt.lift @@ fun res -> Cases.map_changes (fun changes flow -> man.add_change stmt [] flow changes ) res else D.exec stmt man flow (* Remove duplicate evaluations *) let eval exp man flow = D.eval exp man flow |> OptionExt.lift @@ Eval.remove_duplicates man.lattice end let domains : (module STACKED) list ref = ref [] let register_stacked_domain dom = let module D = (val dom : STACKED) in domains := (module Instrument(D)) :: !domains let find_stacked_domain name = List.find (fun dom -> let module D = (val dom : STACKED) in compare D.name name = 0 ) !domains let mem_stacked_domain name = List.exists (fun dom -> let module D = (val dom : STACKED) in compare D.name name = 0 ) !domains let stacked_domain_names () = List.map (fun dom -> let module D = (val dom : STACKED) in D.name ) !domains
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>