package mopsa
Install
dune-project
Dependency
Authors
Maintainers
Sources
md5=37966e98ffeebcedc09bd6e9b2b81f69
sha512=40d4d826c25f680766c07eccbabdf5e8a4fa023016e8a164e4e4f6b3781c8484dc4df437055721dfd19b9db8fb7fe3b61236c4833186d346fc7204a68d01eaaa
doc/mopsa.mopsa_analyzer/Mopsa_analyzer/Languages/Universal/Numeric/Common/index.html
Module Numeric.Common
Common constructs for numeric abstractions.
module I = Mopsa_analyzer.MopsaLib.ItvUtils.IntItvmodule C = Mopsa_analyzer.MopsaLib.CongUtils.IntCongInteger intervals
*********************
type int_itv = I.t_with_botInteger intervals
type MopsaLib.avalue_kind += | V_int_interval : int_itv MopsaLib.avalue_kind(*Query to evaluate the integer interval of an expression
*)
type MopsaLib.avalue_kind += | V_int_interval_fast : int_itv MopsaLib.avalue_kind(*Same as
*)V_int_intervalbut 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.queryval pp_int_interval :
Format.formatter ->
I.t Mopsa_utils.Core.Bot.with_bot ->
unitval compare_int_interval :
I.t Mopsa_utils.Core.Bot.with_bot ->
I.t Mopsa_utils.Core.Bot.with_bot ->
intval constraints_of_itv :
MopsaLib.expr ->
int_itv ->
Mopsa_utils.Core.Location.range ->
MopsaLib.exprCreates var \in itv constraint
Integer intervals with congruence
*************************************
type int_congr_itv = int_itv * C.t_with_botInteger 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.queryRounding mode of floats
***************************
val opt_float_rounding : Apron.Texpr1.round refFloat intervals
*******************
module F = Mopsa_analyzer.MopsaLib.ItvUtils.FloatItvNantype float_itv = F.tFloat intervals
type MopsaLib.avalue_kind += | 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
*)| V_float_maybenan : Universal.Lang.Ast.float_prec -> bool MopsaLib.avalue_kind
val mk_float_interval_query :
?prec:Universal.Lang.Ast.float_prec ->
Framework.Core.Ast.Expr.expr ->
('a, float_itv) Framework.Core.Query.queryval mk_float_maybenan_query :
?prec:Universal.Lang.Ast.float_prec ->
Framework.Core.Ast.Expr.expr ->
('a, bool) Framework.Core.Query.queryval pp_float_interval : Format.formatter -> F.t -> unitval round : unit -> Mopsa_analyzer.MopsaLib.ItvUtils.FloatItvNan.roundFast assume on numeric conditions
*************************************
val interval_of_num_expr :
MopsaLib.expr ->
('a, 'b) MopsaLib.man ->
'a Core.Flow.flow ->
int_itvGet the intervals of a numeric expression
val eval_num_cond :
Framework.Core.Ast.Expr.expr ->
('a, 'b) MopsaLib.man ->
'a Core.Flow.flow ->
bool optionEvaluate 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.casesOptimized assume function that uses intervals to check a condition or falls back to classic assume
Widening thresholds
***********************
module K : sig ... endval widening_thresholds_ctx_key :
('a, Mopsa_utils.Containers.SetExt.ZSet.t)
Mopsa_analyzer__Framework__Core__Context.ctx_keyKey for accessing widening thresholds
val add_widening_threshold :
Framework.Core.All.var ->
Mopsa_utils.Containers.SetExt.ZSet.elt ->
'a Framework.Core.All.ctx ->
'a Framework.Core.All.ctxAdd 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.ctxRemove all widening thresholds of a variable