package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Parameters
Signature

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-27.1-Cobalt.tar.gz

sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2

doc/frama-c.kernel/Frama_c_kernel/Float_interval/Make/index.html

Module `Float_interval.Make`

Builds a semantics of floating-point intervals for different precisions, from a module providing the floating-point numbers used for the bounds of the intervals. Supports NaN and infinite values.

Parameters

module Float : Float_sig.S

Signature

type t

Type of intervals.

val packed_descr : Structural_descr.pack

val compare : t -> t -> int

val equal : t -> t -> bool

val pretty : Format.formatter -> t -> unit

val hash : t -> int

val min_and_max : t -> (Float.t * Float.t) option * bool

Returns the bounds of the float interval, (or None if the argument is exactly NaN), and a boolean indicating the possibility that the value may be NaN.

val nan : t

The NaN singleton

val pos_infinity : Float_interval_sig.prec -> t

The infinities singleton

val neg_infinity : Float_interval_sig.prec -> t

val inject : ?nan:bool -> Float.t -> Float.t -> t

inject ~nan b e creates the floating-point interval b..e, plus NaN if nan is true. b and e must be ordered, and not NaN. They can be infinite.

val singleton : Float.t -> t

singleton f creates the singleton interval f, without NaN.

val top : Float_interval_sig.prec -> t

Top interval for a given precision, including infinite and NaN values.

val top_finite : Float_interval_sig.prec -> t

The interval of all finite values in the given precision.

Lattice operators.

val is_included : t -> t -> bool

val join : t -> t -> t

val widen : Float.widen_hints -> Float_interval_sig.prec -> t -> t -> t

val narrow : t -> t -> t Lattice_bounds.or_bottom

val contains_a_zero : t -> bool

val contains_pos_zero : t -> bool

val contains_neg_zero : t -> bool

val contains_non_zero : t -> bool

val contains_pos_infinity : t -> bool

val contains_neg_infinity : t -> bool

val contains_nan : t -> bool

val is_singleton : t -> bool

Returns true on NaN.

val is_negative : t -> Abstract_interp.Comp.result

is_negative f returns True iff all values in f are negative; False iff all values are positive; and Unknown otherwise. Note that we do not keep sign information for NaN, so if f may contain NaN, the result is always Unknown.

val is_finite : t -> Abstract_interp.Comp.result

val is_infinite : t -> Abstract_interp.Comp.result

val is_not_nan : t -> Abstract_interp.Comp.result

val backward_is_finite : 
  positive:bool ->
  Float_interval_sig.prec ->
  t ->
  t Lattice_bounds.or_bottom

val backward_is_infinite : 
  positive:bool ->
  Float_interval_sig.prec ->
  t ->
  t Lattice_bounds.or_bottom

val backward_is_nan : positive:bool -> t -> t Lattice_bounds.or_bottom

val has_greater_min_bound : t -> t -> int

has_greater_min_bound f1 f2 returns 1 if the interval f1 has a better minimum bound (i.e. greater) than the interval f2.

val has_smaller_max_bound : t -> t -> int

has_smaller_max_bound f1 f2 returns 1 if the interval f1 has a better maximum bound (i.e. lower) than the interval f2.

val forward_comp : 
  Abstract_interp.Comp.t ->
  t ->
  t ->
  Abstract_interp.Comp.result

val backward_comp_left_true : 
  Abstract_interp.Comp.t ->
  Float_interval_sig.prec ->
  t ->
  t ->
  t Lattice_bounds.or_bottom

backward_comp_left_true op prec f1 f2 attempts to reduce f1 into f1' so that the relation f1' op f2 holds. prec is the precision of f1 and f1', but not necessarily of f2.

val backward_comp_left_false : 
  Abstract_interp.Comp.t ->
  Float_interval_sig.prec ->
  t ->
  t ->
  t Lattice_bounds.or_bottom

backward_comp_left_false op prec f1 f2 attempts to reduce f1 into f1' so that the relation f1' op f2 doesn't holds. prec is the precision of f1 and f1', but not necessarily of f2.

val neg : t -> t

val abs : Float_interval_sig.prec -> t -> t

val add : Float_interval_sig.prec -> t -> t -> t

val sub : Float_interval_sig.prec -> t -> t -> t

val mul : Float_interval_sig.prec -> t -> t -> t

val div : Float_interval_sig.prec -> t -> t -> t

val floor : t -> t

val ceil : t -> t

val trunc : t -> t

val fround : t -> t

val exp : Float_interval_sig.prec -> t -> t

val log : Float_interval_sig.prec -> t -> t

val log10 : Float_interval_sig.prec -> t -> t

val sqrt : Float_interval_sig.prec -> t -> t

val pow : Float_interval_sig.prec -> t -> t -> t

val fmod : Float_interval_sig.prec -> t -> t -> t

val cos : Float_interval_sig.prec -> t -> t

val sin : Float_interval_sig.prec -> t -> t

val acos : Float_interval_sig.prec -> t -> t

val asin : Float_interval_sig.prec -> t -> t

val atan : Float_interval_sig.prec -> t -> t

val atan2 : Float_interval_sig.prec -> t -> t -> t

val backward_add : 
  Float_interval_sig.prec ->
  left:t ->
  right:t ->
  result:t ->
  (t * t) Lattice_bounds.or_bottom

val backward_sub : 
  Float_interval_sig.prec ->
  left:t ->
  right:t ->
  result:t ->
  (t * t) Lattice_bounds.or_bottom

val forward_cast : dst:Float_interval_sig.prec -> t -> t

val backward_cast : 
  src:Float_interval_sig.prec ->
  t ->
  t Lattice_bounds.or_bottom

val cast_int_to_float : 
  Float_interval_sig.prec ->
  Integer.t option ->
  Integer.t option ->
  t

val bits_of_float64_list : t -> (Integer.t * Integer.t) list

Bitwise reinterpretation of a floating-point interval of double precision into consecutive ranges of integers.

val bits_of_float32_list : t -> (Integer.t * Integer.t) list

Bitwise reinterpretation of a floating-point interval of single precision into consecutive ranges of integers.

val subdivide : Float_interval_sig.prec -> t -> t * t

Subdivides an interval of a given precision into two intervals. Raises Abstract_interp.Can_not_subdiv if it can't be subdivided. prec must be Single or Double.