package mopsa

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

Common constructs for numeric abstractions.

Integer intervals

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

type int_itv = I.t_with_bot

Integer intervals

type Mopsa.avalue_kind +=
  1. | V_int_interval : int_itv Mopsa.avalue_kind
    (*

    Query to evaluate the integer interval of an expression

    *)
type Mopsa.avalue_kind +=
  1. | V_int_interval_fast : int_itv Mopsa.avalue_kind
    (*

    Same as V_int_interval but should be handled by optimized domains, such Boxes

    *)
val mk_int_interval_query : ?fast:bool -> Ast.Expr.expr -> ('a, int_itv) Core.Query.query
val pp_int_interval : Format.formatter -> I.t Utils_core.Bot.with_bot -> unit
val compare_int_interval : I.t Utils_core.Bot.with_bot -> I.t Utils_core.Bot.with_bot -> int

Integer intervals with congruence

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

type int_congr_itv = int_itv * C.t_with_bot

Integer step intervals

type Mopsa.avalue_kind +=
  1. | V_int_congr_interval : int_congr_itv Mopsa.avalue_kind

Query to evaluate the integer interval of an expression

val mk_int_congr_interval_query : Ast.Expr.expr -> ('a, int_congr_itv) Core.Query.query

Rounding mode of floats

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

val opt_float_rounding : Apron.Texpr1.round ref
val rounding_option_name : string

Float intervals

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

type float_itv = F.t

Float intervals

type Mopsa.avalue_kind +=
  1. | V_float_interval : Lang.Ast.float_prec -> float_itv Mopsa.avalue_kind
    (*

    Query to evaluate the float interval of an expression, with infinities and NaN

    *)
  2. | V_float_maybenan : Lang.Ast.float_prec -> bool Mopsa.avalue_kind
val mk_float_interval_query : ?prec:Lang.Ast.float_prec -> Ast.Expr.expr -> ('a, float_itv) Core.Query.query
val mk_float_maybenan_query : ?prec:Lang.Ast.float_prec -> Ast.Expr.expr -> ('a, bool) Core.Query.query
val pp_float_interval : Format.formatter -> F.t -> unit
val compare_float_interval : F.t -> F.t -> int

Fast assume on numeric conditions

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

val interval_of_num_expr : Mopsa.expr -> ('a, 'b) Mopsa.man -> 'a Core.Flow.flow -> int_itv

Get the intervals of a numeric expression

val eval_num_cond : Ast.Expr.expr -> ('a, 'b) Mopsa.man -> 'a Core.Flow.flow -> bool option

Evaluate a numeric condition using intervals

val assume_num : Ast.Expr.expr -> fthen:('a Core.Flow.flow -> ('a, 'b) Core.Cases.cases) -> felse:('a Core.Flow.flow -> ('a, 'b) Core.Cases.cases) -> ?route:Mopsa.route -> ('a, 'c) Mopsa.man -> 'a Core.Flow.flow -> ('a, 'b) Mopsa.Cases.cases

Optimized assume function that uses intervals to check a condition or falls back to classic assume

Widening thresholds

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

module K : sig ... end
val widening_thresholds_ctx_key : ('a, Mopsa.SetExt.ZSet.t) Core__Context.ctx_key

Key for accessing widening thresholds

val add_widening_threshold : Core.All.var -> Mopsa.SetExt.ZSet.elt -> 'a Core.All.ctx -> 'a Core.All.ctx

Add a constant to the widening thresholds of a variable

val remove_widening_thresholds : Core.All.var -> 'a Core.All.ctx -> 'a Core.All.ctx

Remove all widening thresholds of a variable

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