package mopsa
Install
Dune Dependency
Authors
Maintainers
Sources
md5=fdee20e988343751de440b4f6b67c0f4
sha512=f5cbf1328785d3f5ce40155dada2d95e5de5cce4f084ea30cfb04d1ab10cc9403a26cfb3fa55d0f9da72244482130fdb89c286a9aed0d640bba46b7c00e09500
doc/value/Value/Nonrel/Make/argument-1-Value/index.html
Parameter Make.Value
Header of the abstraction
*****************************
val id : t Core.All.idIdentifier of the value domain
val accept_type : Core.All.typ -> boolPredicate of types abstracted by the value domain
val bottom : tLeast abstract element of the lattice.
val top : tGreatest abstract element of the lattice.
Lattice operators
*********************
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.
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.
Forward semantics
*********************
The forward semantics define how expressions are evaluated into abstract values
val eval : ('v, t) Abstraction.Value.value_man -> Core.All.expr -> tForward evaluation of expressions
val avalue : 'r Core.All.avalue_kind -> t -> 'r optionCreate an avalue over-approximating a given abstract value
Backward semantics
**********************
Backward semantics define how a refinement in the abstract value of an expression impact the abstract values of the sub-expressions
val backward :
('v, t) Abstraction.Value.value_man ->
Core.All.expr ->
t Abstraction.Value.vexpr ->
'v ->
t Abstraction.Value.vexprBackward evaluation of expressions. backward man e ve r refines the values ve of the sub-expressions such that the evaluation of the expression e is in r i.e., we filter the sub-values ve knowing that, after applying the evaluating the expression, the result is in r
val filter : bool -> Core.All.typ -> t -> tKeep abstract values that represent a given truth value
val compare :
('v, t) Abstraction.Value.value_man ->
Core.All.operator ->
bool ->
Core.All.expr ->
t ->
Core.All.expr ->
t ->
t * tBackward evaluation of boolean comparisons. compare man op true e1 v1 e2 v2 returns (v1',v2') where:
- v1' abstracts the set of v in v1 such that v1' op v' is true for some v' in v2'
- v2' abstracts the set of v' in v2 such that v2' op v' is true for some v in v1' i.e., we filter the abstract values v1 and v2 knowing that the test is true
Extended semantics
**********************
Extended semantics define the evaluation of mixed-types expressions. When an expression is composed of sub-expressions with different types, several abstraction may cooperate to compute the evaluation. The previous transfer functions can't be used, because they are defined over one abstraction only.
val eval_ext :
('v, t) Abstraction.Value.value_man ->
Core.All.expr ->
'v optionExtend evaluation of expressions returning the global abstract value of e. Note that the type of e may not satisfy the predicate accept_type.
val backward_ext :
('v, t) Abstraction.Value.value_man ->
Core.All.expr ->
'v Abstraction.Value.vexpr ->
'v ->
'v Abstraction.Value.vexpr optionExtend backward evaluation of an heterogenous expression's sub-parts
val compare_ext :
('v, t) Abstraction.Value.value_man ->
Core.All.operator ->
bool ->
Core.All.expr ->
'v ->
Core.All.expr ->
'v ->
('v * 'v) optionExtend comparison between heterogenous expressions
Communication handlers
***************************
val ask :
('v, t) Abstraction.Value.value_man ->
('a, 'r) Core.All.query ->
'r optionHandler of queries
Pretty printer
******************
val print : Core.All.printer -> t -> unitPrinter of an abstract element.