package mopsa
Install
Dune Dependency
Authors
Maintainers
Sources
md5=fdee20e988343751de440b4f6b67c0f4
sha512=f5cbf1328785d3f5ce40155dada2d95e5de5cce4f084ea30cfb04d1ab10cc9403a26cfb3fa55d0f9da72244482130fdb89c286a9aed0d640bba46b7c00e09500
doc/combiner/Combiner/Domain/DomainToCombiner/argument-1-D/index.html
Parameter DomainToCombiner.D
Domain header
*****************
val id : t Core.All.idDomain identifier
val checks : Core.All.check listList of checks performed by the domain
val bottom : tLeast abstract element of the lattice.
val top : tGreatest abstract element of the lattice.
val is_bottom : t -> boolis_bottom a tests whether a is bottom or not.
Lattice operators
*********************
Partial order relation. subset a1 a2 tests whether a1 is related to (or included in) a2.
val widen : 'a Core.All.ctx -> t -> t -> twiden ctx a1 a2 computes an upper bound of a1 and a2 that ensures stabilization of ascending chains.
val merge : t -> (t * Core.All.change) -> (t * Core.All.change) -> tmerge 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
**********************
val init :
Core.All.program ->
('a, t) Core.All.man ->
'a Core.All.flow ->
'a Core.All.post optionInitialization function
val exec :
Core.All.stmt ->
('a, t) Core.All.man ->
'a Core.All.flow ->
'a Core.All.post optionPost-state of statements
val eval :
Core.All.expr ->
('a, t) Core.All.man ->
'a Core.All.flow ->
'a Core.All.eval optionEvaluation of expressions
val ask :
('a, 'r) Core.All.query ->
('a, t) Core.All.man ->
'a Core.All.flow ->
('a, 'r) Core.All.cases optionHandler of queries
Printing
************
val print_state : Core.All.printer -> t -> unitPrinter of an abstract element.
val print_expr :
('a, t) Core.All.man ->
'a Core.All.flow ->
Core.All.printer ->
Core.All.expr ->
unitPrinter of an expression's value