package mopsa

  1. Overview
  2. Docs
package mopsa
Legend:
Library
Module
Module type
Parameter
Class
Class type

Signature of a value abstraction.

Value manager

type ('v, 't) value_man = {
  1. bottom : 'v;
  2. top : 'v;
  3. is_bottom : 'v -> bool;
  4. subset : 'v -> 'v -> bool;
  5. join : 'v -> 'v -> 'v;
  6. meet : 'v -> 'v -> 'v;
  7. print : Core.All.printer -> 'v -> unit;
  8. get : 'v -> 't;
  9. set : 't -> 'v -> 'v;
  10. eval : Core.All.expr -> 'v;
  11. avalue : 'r. 'r Core.All.avalue_kind -> 'v -> 'r;
  12. ask : 'a 'r. ('a, 'r) Core.All.query -> 'r;
}

Manager of value abstractions

Valued expressions

type 'v vexpr

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 root_vexpr : 'v vexpr -> 'v vexpr

Get the root value expressions

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 map_vexpr : ('v -> 's) -> 'v vexpr -> 's vexpr

Map the value of each sub-expression

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

val map2_vexpr : ('v -> 't) -> ('s -> 't) -> ('v -> 's -> 't) -> 'v vexpr -> 's vexpr -> 't vexpr

Combine two valued expressions

val merge_vexpr : ('v -> 'v -> 'v) -> 'v vexpr -> 'v vexpr -> 'v vexpr

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

val mem_value_abstraction : string -> bool

Check if an abstraction exists

val value_abstraction_names : unit -> string list

Get the list of registered abstractions

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct