package codex

  1. Overview
  2. Docs
The Codex library for building static analysers based on abstract interpretation

Install 

dune-project
 Dependency

codex.top Edit opam file Versions (1)

Authors

  1. M
    Matthieu Lemerre
  2. J
    Julien Simonnet
  3. O
    Olivier Nicole
  4. P
    Paul Robert
  5. D
    Dorian Lesbre
  6. I
    Iker Canut
  7. C
    Corentin Gendreau
  8. G
    Guillaume Girol
  9. C
    Charles Babu
  10. J
    Jérôme Faucheux

Maintainers

  1. M
    Matthieu Lemerre <matthieu.lemerre@cea.fr>

Sources

1.0-rc4.tar.gz
md5=bc7266a140c6886add673ede90e335d3
sha512=8da42c0ff2c1098c5f9cb2b5b43b306faf7ac93b8f5ae00c176918cee761f249ff45b29309f31a05bbcf6312304f86a0d5a000eb3f1094d3d3c2b9b4c7f5c386

doc/codex.framac_ival/Framac_ival/Fval/index.html

Module Framac_ival.FvalSource

Floating-point intervals, used to construct arithmetic lattices. The interfaces of this module may change between Frama-C versions. Contact us if you need stable APIs.

Sourcetype kind = Float_sig.prec =
  1. | Single
    (*

    32 bits float (a.k.a 'float' C type)

    *)
  2. | Double
    (*

    64 bits float (a.k.a 'double' C type)

    *)
  3. | Long_Double
  4. | Real
    (*

    set of real

    *)
Sourceval pretty_kind : Format.formatter -> kind -> unit
Sourcemodule F : sig ... end
include Float_interval_sig.S with type float := F.t
Sourcetype t

Type of the interval bounds.

Type of intervals.

Sourceval compare : t -> t -> int
Sourceval equal : t -> t -> bool
Sourceval pretty : Format.formatter -> t -> unit
Sourceval hash : t -> int
Sourceval min_and_max : t -> (F.t * F.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.

Sourceval nan : t

The NaN singleton

Sourceval singleton : F.t -> t

singleton f creates the singleton interval f, without NaN.

Sourceval top_finite : Float_interval_sig.prec -> t

The interval of all finite values in the given precision.

Lattice operators.

Sourceval is_included : t -> t -> bool
Sourceval join : t -> t -> t
Sourceval widen : t -> t -> t
Sourceval narrow : t -> t -> t Bottom.Type.or_bottom
Sourceval contains_a_zero : t -> bool
Sourceval contains_pos_zero : t -> bool
Sourceval contains_neg_zero : t -> bool
Sourceval contains_non_zero : t -> bool
Sourceval contains_pos_infinity : t -> bool
Sourceval contains_neg_infinity : t -> bool
Sourceval contains_nan : t -> bool

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.

Sourceval backward_is_not_nan : t -> t Bottom.Type.or_bottom
Sourceval 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.

Sourceval 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.

Sourceval backward_comp_left_true : Abstract_interp.Comp.t -> Float_interval_sig.prec -> t -> t -> t Bottom.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.

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.

Sourceval neg : t -> t
Sourceval add : Float_interval_sig.prec -> t -> t -> t
Sourceval sub : Float_interval_sig.prec -> t -> t -> t
Sourceval mul : Float_interval_sig.prec -> t -> t -> t
Sourceval div : Float_interval_sig.prec -> t -> t -> t
Sourceval pow : Float_interval_sig.prec -> t -> t -> t
Sourceval fmod : Float_interval_sig.prec -> t -> t -> t
Sourceval atan2 : Float_interval_sig.prec -> t -> t -> t
Sourceval backward_add : Float_interval_sig.prec -> left:t -> right:t -> result:t -> (t * t) Bottom.Type.or_bottom
Sourceval backward_sub : Float_interval_sig.prec -> left:t -> right:t -> result:t -> (t * t) Bottom.Type.or_bottom
Sourceval forward_cast : dst:Float_interval_sig.prec -> t -> t
Sourceval cast_int_to_float : Float_interval_sig.prec -> Z.t option -> Z.t option -> t
Sourceval bits_of_float64_list : t -> (Z.t * Z.t) list

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

Sourceval bits_of_float32_list : t -> (Z.t * Z.t) list

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

Sourceval 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.

Sourceval round_to_single_precision_float : t -> t
Sourceval inject : ?nan:bool -> kind -> F.t -> F.t -> t

inject creates an abstract float interval. It handles infinities, flush-to-zero (rounding subnormals if needed) and NaN. Inputs must be compatible with float_kind. Raises no exceptions (unless values are not compatible with float_kind, in which case execution is aborted). The two floating point numbers must be ordered (so not NaN). ~nan indicates if NaN is present.

Sourceval inject_singleton : F.t -> t
Sourceval top : t
Sourceval plus_zero : t
Sourceval minus_zero : t
Sourceval zeros : t

Both positive and negative zero

Sourceval pi : t

Real representation of \pi.

Sourceval e : t

Real representation of \pi.

Real representation of \e.

Sourceval contains_plus_zero : t -> bool
Sourceval meet : t -> t -> t Bottom.or_bottom
Sourceval is_singleton : t -> bool

Returns true on NaN. We expect this function to be e.g. to perform subdivisions/enumerations. The size of the concretization is less interesting to us. (And it is also possible to consider that there is only one NaN value in the concrete anyway.)

Sourceexception Not_Singleton_Float
Sourceval project_float : t -> F.t
Sourceval subdiv_float_interval : kind -> t -> t * t

Raise Can_not_subdiv if it can't be subdivided

Discussion regarding kind and the 3 functions below.

Support for fesetround(FE_UPWARD) and fesetround(FE_DOWNWARD) seems to be especially poor, including in not-so-old versions of Glibc (https://sourceware.org/bugzilla/show_bug.cgi?id=3976). The code for exp, log and log10 is correct wrt. kind=Reak ONLY if the C implementation of these functions is correct in directed rounding modes. Otherwise, anything could happen, including crashes. For now, unless the Libc is known to be reliable, these functions should be called with rounding_mode=Nearest_Even only. Also note that there the Glibc does not guarantee that f(FE_DOWNWARD) <= f(FE_TONEAREST) <= f(FE_UPWARD), which implies that using different rounding modes to bound the final result does not ensure correct bounds. Here's an example where it does not hold (glibc 2.21): log10f(3, FE_TONEAREST) < log10f(3, FE_DOWNWARD).

Also, we have observed bugs in powf, which is called when kind=Float32.

Sourceval exp : kind -> t -> t
Sourceval log : kind -> t -> t
Sourceval log10 : kind -> t -> t
Sourceval floor : kind -> t -> t
Sourceval ceil : kind -> t -> t
Sourceval trunc : kind -> t -> t
Sourceval fround : kind -> t -> t
Sourceval backward_cast_float_to_double : t -> t Bottom.or_bottom

backward_cast_float_to_double d return all possible float32 f such that (double)f = d. The double of d that have no float32 equivalent are discarded.

Sourceval backward_cast_double_to_real : t -> t

Classify a Cil_types.fkind as either a 32 or 64 floating-point type. Long double are over approximated by Reals