package mopsa

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

Module Numeric.Common

Common constructs for numeric abstractions.

Integer intervals

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

type int_itv = I.t_with_bot

Integer intervals

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

    Query to evaluate the integer interval of an expression

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

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

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

Creates var \in itv constraint

Integer intervals with congruence

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

type int_congr_itv = int_itv * C.t_with_bot

Integer step intervals

Query to evaluate the integer interval of an expression

val mk_int_congr_interval_query : Framework.Core.Ast.Expr.expr -> ('a, int_congr_itv) Framework.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 MopsaLib.avalue_kind +=
  1. | V_float_interval : Universal.Lang.Ast.float_prec -> float_itv MopsaLib.avalue_kind
    (*

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

    *)
  2. | V_float_maybenan : Universal.Lang.Ast.float_prec -> bool MopsaLib.avalue_kind
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 : MopsaLib.expr -> ('a, 'b) MopsaLib.man -> 'a Core.Flow.flow -> int_itv

Get the intervals of a numeric expression

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

Evaluate a numeric condition using intervals

val assume_num : Framework.Core.Ast.Expr.expr -> fthen:('a Core.Flow.flow -> ('a, 'b) Core.Cases.cases) -> felse:('a Core.Flow.flow -> ('a, 'b) Core.Cases.cases) -> ?route:MopsaLib.route -> ('a, 'c) MopsaLib.man -> 'a Core.Flow.flow -> ('a, 'b) Mopsa_analyzer.MopsaLib.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_utils.Containers.SetExt.ZSet.t) Mopsa_analyzer__Framework__Core__Context.ctx_key

Key for accessing widening thresholds

Add a constant to the widening thresholds of a variable

val remove_widening_thresholds : Framework.Core.All.var -> 'a Framework.Core.All.ctx -> 'a Framework.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