Module Numerors_domain

module Numerors_domain: sig .. end

type value 
type location = Precise_locs.precise_location 
val value_key : value Structure.Key_Value.k
val ok : bool

True if the numerors domain is available; False if the MPFR library has not been found.

Functions used by the engine to build numerors abstractions.

val add_numerors_value : (module Abstract_value.Internal) -> (module Abstract_value.Internal)

Builds the product between a given value module and the numerors value module. If the given value module contains Cvalue, uses cvalues to reduce numerors values on casts from integer to floating-point values. Fails if numerors domain is not available.

val reduce_error : (module Abstract_value.External with type t = 'v) -> 'v -> 'v
val numerors_domain : unit ->
(module Abstract_domain.Internal with type location = location and type value =
value)

Returns the numerors domain module, if available. Fails otherwise.