package mopsa
Install
Dune Dependency
Authors
Maintainers
Sources
md5=9f673f79708b44a7effb3b6bb3618d2c
sha512=cb91cb428e43a22f1abbcb8219710d0c10a5b3756d0da392d4084b3b3a6157350776c596983e63def344f617d39964e91f244f60c07958695ee5c8c809a9f0f4
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, effect1) (post2, effect2) 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 effects effect1 and effect2 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