package mopsa
Install
Dune Dependency
Authors
Maintainers
Sources
md5=fdee20e988343751de440b4f6b67c0f4
sha512=f5cbf1328785d3f5ce40155dada2d95e5de5cce4f084ea30cfb04d1ab10cc9403a26cfb3fa55d0f9da72244482130fdb89c286a9aed0d640bba46b7c00e09500
doc/value/Value/Nonrel/index.html
Module Value.NonrelSource
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.
Access 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
Find 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.
Context 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
Remove the bounds of a variable from a context
Remove the bounds of a variable from a flow
Find 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