package mopsa

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

Module Numeric_common.CommonSource

Common constructs for numeric abstractions.

Integer intervals

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

Sourcetype int_itv = I.t_with_bot

Integer intervals

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

    Query to evaluate the integer interval of an expression

    *)
Sourcetype 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

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

Creates var \in itv constraint

Integer intervals with congruence

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

Sourcetype int_congr_itv = int_itv * C.t_with_bot

Integer step intervals

Query to evaluate the integer interval of an expression

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

Rounding mode of floats

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

Sourceval opt_float_rounding : Apron.Texpr1.round Stdlib.ref
Sourceval rounding_option_name : string

Float intervals

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

Sourcetype float_itv = F.t

Float intervals

Sourcetype 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
Sourceval mk_float_interval_query : ?prec:Lang.Ast.float_prec -> Ast.Expr.expr -> ('a, float_itv) Core.Query.query
Sourceval mk_float_maybenan_query : ?prec:Lang.Ast.float_prec -> Ast.Expr.expr -> ('a, bool) Core.Query.query
Sourceval pp_float_interval : Stdlib.Format.formatter -> F.t -> unit
Sourceval compare_float_interval : F.t -> F.t -> int

Fast assume on numeric conditions

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

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

Get the intervals of a numeric expression

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

Evaluate a numeric condition using intervals

Sourceval 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
Sourceval widening_thresholds_ctx_key : ('a, Mopsa.SetExt.ZSet.t) Core__Context.ctx_key

Key for accessing widening thresholds

Sourceval 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

Sourceval 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