package mopsa
Install
Dune Dependency
Authors
Maintainers
Sources
md5=fdee20e988343751de440b4f6b67c0f4
sha512=f5cbf1328785d3f5ce40155dada2d95e5de5cce4f084ea30cfb04d1ab10cc9403a26cfb3fa55d0f9da72244482130fdb89c286a9aed0d640bba46b7c00e09500
doc/abstraction/Abstraction/Simplified_value/MakeValue/index.html
Module Simplified_value.MakeValueSource
Functor to create a value abstraction from a simplified value abstraction
Parameters
module V : SIMPLIFIED_VALUESignature
Header of the abstraction
*****************************
type t = V.tType of the abstract value.
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
Forward 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) Value.value_man ->
Core.All.expr ->
t Value.vexpr ->
'v ->
t 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) 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.
Extend 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) Value.value_man ->
Core.All.expr ->
'v Value.vexpr ->
'v ->
'v Value.vexpr optionExtend backward evaluation of an heterogenous expression's sub-parts
val compare_ext :
('v, t) Value.value_man ->
Core.All.operator ->
bool ->
Core.All.expr ->
'v ->
Core.All.expr ->
'v ->
('v * 'v) optionExtend comparison between heterogenous expressions
Communication handlers
***************************
Handler of queries
Pretty printer
******************
val print : Core.All.printer -> t -> unitPrinter of an abstract element.