package mopsa
Install
dune-project
Dependency
Authors
Maintainers
Sources
md5=37966e98ffeebcedc09bd6e9b2b81f69
sha512=40d4d826c25f680766c07eccbabdf5e8a4fa023016e8a164e4e4f6b3781c8484dc4df437055721dfd19b9db8fb7fe3b61236c4833186d346fc7204a68d01eaaa
doc/mopsa.mopsa_analyzer/Mopsa_analyzer/Framework/Sig/Abstraction/Value/index.html
Module Abstraction.Value
Signature of a value abstraction.
Value manager
type ('v, 't) value_man = {
bottom : 'v;
top : 'v;
is_bottom : 'v -> bool;
subset : 'v -> 'v -> bool;
join : 'v -> 'v -> 'v;
meet : 'v -> 'v -> 'v;
print : Core.All.printer -> 'v -> unit;
get : 'v -> 't;
set : 't -> 'v -> 'v;
eval : Core.All.expr -> 'v;
avalue : 'r. 'r Core.All.avalue_kind -> 'v -> 'r;
ask : 'a 'r. ('a, 'r) Core.All.query -> 'r;
}
Manager of value abstractions
Valued expressions
Valued exprssions annotate each node in the tree of the expression with its abstract value
val empty_vexpr : 'v vexpr
Empty valued expression
val singleton_vexpr : Core.All.expr -> 'v -> 'v vexpr -> 'v vexpr
Singleton representing a leaf expression and its value
val add_vexpr : Core.All.expr -> 'v -> 'v vexpr -> 'v vexpr -> 'v vexpr
Attache a value to a sub-expression in a value expression
val refine_vexpr : Core.All.expr -> 'v -> 'v vexpr -> 'v vexpr
Change the value of a sub-expression in a value expression
val find_vexpr : Core.All.expr -> 'v vexpr -> 'v * 'v vexpr
Find the value of a sub-expression in a valued expression. ** Raises Not_found
if the sub-expression is not found.
val find_vexpr_opt : Core.All.expr -> 'v vexpr -> ('v * 'v vexpr) option
Same as find_ctx_opt
but returns None
if the sub-expression is not found
val fold_root_vexpr :
('a -> Core.All.expr -> 'v -> 'v vexpr -> 'a) ->
'a ->
'v vexpr ->
'a
Fold over the direct sub-expressions only
val fold_vexpr :
('a -> Core.All.expr -> 'v -> 'v vexpr -> 'a) ->
'a ->
'v vexpr ->
'a
Fold over all sub-expression
Combine two valued expressions
Combine two valued expressions
Value domain
module type VALUE = sig ... end
val default_filter : bool -> Core.All.typ -> 't -> 't
val default_backward :
('v, 't) value_man ->
Core.All.expr ->
't vexpr ->
'v ->
't vexpr
val default_compare :
('v, 't) value_man ->
Core.All.operator ->
bool ->
Core.All.expr ->
't ->
Core.All.expr ->
't ->
't * 't
module DefaultValueFunctions : sig ... end
Helper module defining default transfer functions
Registration
val register_value_abstraction : (module VALUE) -> unit
Register a new value abstraction
val find_value_abstraction : string -> (module VALUE)
Find a value abstraction by its name