package mopsa
Install
dune-project
Dependency
Authors
Maintainers
Sources
md5=37966e98ffeebcedc09bd6e9b2b81f69
sha512=40d4d826c25f680766c07eccbabdf5e8a4fa023016e8a164e4e4f6b3781c8484dc4df437055721dfd19b9db8fb7fe3b61236c4833186d346fc7204a68d01eaaa
doc/mopsa.mopsa_analyzer/Mopsa_analyzer/Framework/Combiners/Value/Nonrel/Make/index.html
Module Nonrel.Make
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.
val id : t Core.All.idDomain identifier
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
*************
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 -> t * Core.Alarm.assumption_kind listInitial abstract element, and assumptions about the domain (prototype, ...)
val exec :
Core.All.stmt ->
('a, t) Sig.Abstraction.Simplified.simplified_man ->
'a Core.All.ctx ->
t ->
t optionComputation of post-conditions
val ask :
('a, 'r) Core.All.query ->
('a, t) Sig.Abstraction.Simplified.simplified_man ->
'a Core.All.ctx ->
t ->
'r optionHandler of queries
Printing
************
val print_state : Core.All.printer -> t -> unitPrinter of an abstract element.
val print_expr :
('a, t) Sig.Abstraction.Simplified.simplified_man ->
'a Core.All.ctx ->
t ->
Core.All.printer ->
Core.All.expr ->
unitPrinter of an expression's value