package mopsa

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

Types

*********

module Set : sig ... end
type t =
  1. | In of Set.t
  2. | NotIn of Set.t
val print : Mopsa.printer -> t -> unit

Header of the abstraction

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

include sig ... end
val id : t Core__Id.id
val name : string
val display : string
val debug : ('a, Stdlib.Format.formatter, unit, unit) Stdlib.format4 -> 'a
val accept_type : Mopsa.typ -> bool
val bottom : t
val top : t
val is_bottom : t -> bool
val is_top : t -> bool

Options

***********

val opt_max_intset : int Stdlib.ref

Utilities

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

val zero : t
val one : t
val bound_size : t -> t

bound a is a if the number of elements in a is lesser or equal to the maximum number of elements allowed, otherwise it is top. Does not bound the size of NotIn, as there are no infinite ascending chains for NotIn.

val of_bounds : Z.t -> Z.t -> t

of_bounds l r is {l, l+1, ..., r} if this set has size up to the maximum number of elements, otherwise it is NotIn {l-1, r+1}. This is a precision optimization compared to simply return top, as we already know that l - 1 and r + 1 will not be in the set of elements. Due to this optimization, top is often represented as ∉{MININT - 1, MAXINT + 1} in C programs.

val is_zero : t -> bool
val contains_zero : t -> bool
val contains_non_zero : t -> bool
val remove_zero : t -> t
val of_bool : bool -> bool -> t

of_bool t f is:

  • ∅ if t = false and f = false
  • {0} if t = false and f = true
  • {1} if t = true and f = false
  • {0,1} if t = true and f = true
val map : (Set.elt -> Set.elt) -> t -> t
val combine : (Set.elt -> Set.elt -> Set.elt) -> Set.t -> Set.t -> Set.t

combine combiner s1 s2 is {combiner x1 x2 | x1 ∈ s1, x2 ∈ s2}.

val combine_opt : (Set.elt -> Set.elt -> Set.elt option) -> Set.t -> Set.t -> Set.t
val subset : t -> t -> bool

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

val join : t -> t -> t
val meet : t -> t -> t
val widen : 'a -> t -> t -> t

Forward semantics

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

val constant : Mopsa.constant -> Mopsa.typ -> t
val unop : Mopsa.operator -> Mopsa.typ -> t -> Mopsa.typ -> t
val combine_with : ('a -> Set.t -> Set.t -> Set.t) -> 'a -> t -> t -> t

combine_with combiner a1 a2 combines the elements of a1 and a2 with combiner. If a1 and a2 are finite sets, it applies combiner to the cartesian product of the two. If a1 and a2 are both exclued powersets, returns top. If one of the two is a finite set of size exactly one (and therefore, it is a definite value), returns an excluded set where the constant is combined with the excluded powerset. Otherwise, returns top.

val binop : Mopsa.operator -> Mopsa.typ -> t -> Mopsa.typ -> t -> Mopsa.typ -> t
include module type of struct include Mopsa.Sig.Abstraction.Simplified_value.DefaultValueFunctions end

Template module with default transfer functions

Template module with default transfer functions

Template module with default transfer functions

Template module with default transfer functions

val filter : bool -> Core.All.typ -> 't -> 't
val backward_unop : Core.All.operator -> Core.All.typ -> 't -> Core.All.typ -> 't -> 't
val backward_binop : Core.All.operator -> Core.All.typ -> 't -> Core.All.typ -> 't -> Core.All.typ -> 't -> 't * 't
val avalue : 'r. 'r Mopsa.avalue_kind -> t -> 'r option
val compare : Mopsa.operator -> bool -> Mopsa.typ -> t -> Mopsa.typ -> t -> t * t
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