package mopsa
Install
dune-project
Dependency
Authors
Maintainers
Sources
md5=37966e98ffeebcedc09bd6e9b2b81f69
sha512=40d4d826c25f680766c07eccbabdf5e8a4fa023016e8a164e4e4f6b3781c8484dc4df437055721dfd19b9db8fb7fe3b61236c4833186d346fc7204a68d01eaaa
doc/mopsa.mopsa_analyzer/Mopsa_analyzer/Framework/Combiners/Value/Union/Make/index.html
Module Union.Make
Create a disjoint union of two value abstractions
Parameters
module V1 : Sig.Abstraction.Value.VALUEmodule V2 : Sig.Abstraction.Value.VALUESignature
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) Sig.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) Sig.Abstraction.Value.value_man ->
Core.All.expr ->
t Sig.Abstraction.Value.vexpr ->
'v ->
t Sig.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) Sig.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) Sig.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) Sig.Abstraction.Value.value_man ->
Core.All.expr ->
'v Sig.Abstraction.Value.vexpr ->
'v ->
'v Sig.Abstraction.Value.vexpr optionExtend backward evaluation of an heterogenous expression's sub-parts
val compare_ext :
('v, t) Sig.Abstraction.Value.value_man ->
Core.All.operator ->
bool ->
Core.All.expr ->
'v ->
Core.All.expr ->
'v ->
('v * 'v) optionExtend comparison between heterogenous expressions
val domain_assumptions : Core.Alarm.assumption_kind listList of domain general assumptions (eg, prototype domain) *
Communication handlers
***************************
val ask :
('v, t) Sig.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.