Module Excluded.SimplifiedValueSource

Types

*********

module Set : sig ... end
Sourcetype t =
  1. | In of Set.t
  2. | NotIn of Set.t
Sourceval 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
Sourceval accept_type : Mopsa.typ -> bool
Sourceval bottom : t
Sourceval top : t
Sourceval is_bottom : t -> bool
Sourceval is_top : t -> bool

Options

***********

Sourceval opt_max_intset : int Stdlib.ref

Utilities

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

Sourceval zero : t
Sourceval one : t
Sourceval 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.

Sourceval 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.

Sourceval is_zero : t -> bool
Sourceval contains_zero : t -> bool
Sourceval contains_non_zero : t -> bool
Sourceval remove_zero : t -> t
Sourceval 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
Sourceval map : (Set.elt -> Set.elt) -> t -> t
Sourceval 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}.

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

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

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

Forward semantics

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

Sourceval constant : Mopsa.constant -> Mopsa.typ -> t
Sourceval unop : Mopsa.operator -> Mopsa.typ -> t -> Mopsa.typ -> t
Sourceval 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.

Sourceval 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
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
Sourceval avalue : 'r. 'r Mopsa.avalue_kind -> t -> 'r option
Sourceval compare : Mopsa.operator -> bool -> Mopsa.typ -> t -> Mopsa.typ -> t -> t * t