package mopsa

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

Create a pair of two value abstractions.

Parameters

Signature

Header of the abstraction

*****************************

type t = V1.t * V2.t

Type of the abstract value.

val id : t Core.All.id

Identifier of the value domain

val accept_type : Core.All.typ -> bool

Predicate of types abstracted by the value domain

val name : string

Name of the value domain

val display : string

Display name used in debug messages

val bottom : t

Least abstract element of the lattice.

val top : t

Greatest abstract element of the lattice.

Lattice operators

*********************

val is_bottom : t -> bool

is_bottom a tests whether a is bottom or not.

val subset : t -> t -> bool

Partial order relation. subset a1 a2 tests whether a1 is related to (or included in) a2.

val join : t -> t -> t

join a1 a2 computes an upper bound of a1 and a2.

val meet : t -> t -> t

meet a1 a2 computes a lower bound of a1 and a2.

val widen : 'a Core.All.ctx -> t -> t -> t

widen 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

Forward evaluation of expressions

val avalue : 'r Core.All.avalue_kind -> t -> 'r option

Create 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

Backward 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 -> t

Keep abstract values that represent a given truth value

val compare : ('v, t) Abstraction.Value.value_man -> Core.All.operator -> bool -> Core.All.expr -> t -> Core.All.expr -> t -> t * t

Backward 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) Abstraction.Value.value_man -> Core.All.expr -> 'v option

Extend evaluation of expressions returning the global abstract value of e. Note that the type of e may not satisfy the predicate accept_type.

Extend backward evaluation of an heterogenous expression's sub-parts

val compare_ext : ('v, t) Abstraction.Value.value_man -> Core.All.operator -> bool -> Core.All.expr -> 'v -> Core.All.expr -> 'v -> ('v * 'v) option

Extend comparison between heterogenous expressions

Communication handlers

***************************

val ask : ('v, t) Abstraction.Value.value_man -> ('a, 'r) Core.All.query -> 'r option

Handler of queries

Pretty printer

******************

val print : Core.All.printer -> t -> unit

Printer of an abstract element.

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