package mopsa
Install
dune-project
Dependency
Authors
Maintainers
Sources
md5=37966e98ffeebcedc09bd6e9b2b81f69
sha512=40d4d826c25f680766c07eccbabdf5e8a4fa023016e8a164e4e4f6b3781c8484dc4df437055721dfd19b9db8fb7fe3b61236c4833186d346fc7204a68d01eaaa
doc/mopsa.mopsa_analyzer/Mopsa_analyzer/Framework/Combiners/Value/Nonrel/index.html
Module Value.Nonrel
Generic non-relational abstraction.
This combiner lifts a non-relational value abstraction 𝒱 into an abstract domain of partial environments 𝐕↛𝒱 from variables to values.
The concretization of the domain is: γ(X) = ρ | dom(ρ) ⊆ dom(X) ∧ ∀ v ∈ dom(ρ): ρ(v) ∈ γᵥ(X(v))
Identifier for the non-relation domain
******************************************
type Core.All.id += | D_nonrel : (module Sig.Abstraction.Value.VALUE with type t = 'v) -> (Core.All.var, 'v) Lattices.Partial_map.map Core.All.id
Identifier of a non-relational domain
Variable's context
**********************
The context of a variable keeps (flow-insensitive) information about the variable that can pushed by external domains and consumed by the value abstraction.
This is useful to implement a widening with thresholds: external heuristics discover the theresholds and put them in the context of the variable. When widen is called on a the value of a variable, it is enriched with its context.
val var_ctx_key : ('a, 'a Core.All.ctx Core.Ast.Var.VarMap.t) Core.All.ctx_keyAccess key to the map of variables contexts
val add_var_ctx :
Core.All.var ->
('a, 'v) Core.All.ctx_key ->
'v ->
'a Core.All.ctx ->
'a Core.All.ctxAdd a context to a variable
val find_var_ctx_opt :
Core.All.var ->
('a, 'v) Core.All.ctx_key ->
'a Core.All.ctx ->
'v optionFind the context attached to a variable
val find_var_ctx :
Core.All.var ->
('a, 'v) Core.All.ctx_key ->
'a Core.All.ctx ->
'vFind the context attached to a variable
val remove_var_ctx :
Core.All.var ->
('a, 'v) Core.All.ctx_key ->
'a Core.All.ctx ->
'a Core.All.ctxRemove the context attached to a variable
Variable bounds
*******************
The bounds of a variable is an invariant about its value that is always valid. It is put in the context of the variable and is used to refine its value whenever it changes.
val var_bounds_ctx : ('a, Core.All.constant) Core.All.ctx_keyContext for saving the bounds of a variable
val add_var_bounds_ctx :
Core.All.var ->
Core.All.constant ->
'a Core.All.ctx ->
'a Core.All.ctxAdd the bounds of a variable to a context
val add_var_bounds_flow :
Core.All.var ->
Core.All.constant ->
'a Core.All.flow ->
'a Core.All.flowAdd the bounds of a variable to a flow
val remove_var_bounds_ctx : Core.All.var -> 'a Core.All.ctx -> 'a Core.All.ctxRemove the bounds of a variable from a context
val remove_var_bounds_flow :
Core.All.var ->
'a Core.All.flow ->
'a Core.All.flowRemove the bounds of a variable from a flow
val find_var_bounds_ctx_opt :
Core.All.var ->
'a Core.All.ctx ->
Core.All.constant optionFind the bounds of a variable in a context
Non-relational domain
*************************
module Make
(Value : Sig.Abstraction.Value.VALUE) :
Sig.Abstraction.Simplified.SIMPLIFIED
with type t = (Core.All.var, Value.t) Lattices.Partial_map.mapCreate a non-relational domain from a value abstraction