package mopsa
Install
Dune Dependency
Authors
Maintainers
Sources
md5=fdee20e988343751de440b4f6b67c0f4
sha512=f5cbf1328785d3f5ce40155dada2d95e5de5cce4f084ea30cfb04d1ab10cc9403a26cfb3fa55d0f9da72244482130fdb89c286a9aed0d640bba46b7c00e09500
doc/value/Value/Nonrel/Make/index.html
Module Nonrel.MakeSource
Create a non-relational domain from a value abstraction
Parameters
module Value : Sig.Abstraction.Value.VALUESignature
Domain header
*****************
type t = (Core.All.var, Value.t) Lattices.Partial_map.mapType of an abstract elements.
Domain identifier
Domain name
val bottom : tLeast abstract element of the lattice.
val top : tGreatest abstract element of the lattice.
Predicates
**************
val is_bottom : t -> boolis_bottom a tests whether a is bottom or not.
Partial order relation. subset a1 a2 tests whether a1 is related to (or included in) a2.
Operators
*************
widen ctx a1 a2 computes an upper bound of a1 and a2 that ensures stabilization of ascending chains.
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.
Transfer functions
**********************
Initial abstract element
val exec :
Core.All.stmt ->
('a, t) Abstraction.Simplified.simplified_man ->
'a Core.All.ctx ->
t ->
t optionComputation of post-conditions
val ask :
('a, 'r) Core.All.query ->
('a, t) Abstraction.Simplified.simplified_man ->
'a Core.All.ctx ->
t ->
'r optionHandler of queries
Printing
************
Printer of an abstract element.
val print_expr :
('a, t) Abstraction.Simplified.simplified_man ->
'a Core.All.ctx ->
t ->
Core.All.printer ->
Core.All.expr ->
unitPrinter of an expression's value