package frama-c

  1. Overview
  2. Docs
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

  1. M
    Michele Alberti
  2. T
    Thibaud Antignac
  3. G
    Gergö Barany
  4. P
    Patrick Baudin
  5. T
    Thibaut Benjamin
  6. A
    Allan Blanchard
  7. L
    Lionel Blatter
  8. F
    François Bobot
  9. R
    Richard Bonichon
  10. Q
    Quentin Bouillaguet
  11. D
    David Bühler
  12. Z
    Zakaria Chihani
  13. L
    Loïc Correnson
  14. J
    Julien Crétin
  15. P
    Pascal Cuoq
  16. Z
    Zaynah Dargaye
  17. B
    Basile Desloges
  18. J
    Jean-Christophe Filliâtre
  19. P
    Philippe Herrmann
  20. M
    Maxime Jacquemin
  21. F
    Florent Kirchner
  22. A
    Alexander Kogtenkov
  23. T
    Tristan Le Gall
  24. J
    Jean-Christophe Léchenet
  25. M
    Matthieu Lemerre
  26. D
    Dara Ly
  27. D
    David Maison
  28. C
    Claude Marché
  29. A
    André Maroneze
  30. T
    Thibault Martin
  31. F
    Fonenantsoa Maurica
  32. M
    Melody Méaulle
  33. B
    Benjamin Monate
  34. Y
    Yannick Moy
  35. A
    Anne Pacalet
  36. V
    Valentin Perrelle
  37. G
    Guillaume Petiot
  38. D
    Dario Pinto
  39. V
    Virgile Prevosto
  40. A
    Armand Puccetti
  41. F
    Félix Ridoux
  42. V
    Virgile Robles
  43. M
    Muriel Roger
  44. J
    Julien Signoles
  45. N
    Nicolas Stouls
  46. K
    Kostyantyn Vorobyov
  47. B
    Boris Yakobowski

Maintainers

  1. F
    frama-ci-bot@frama-c.com

Sources

frama-c-27.0-beta-Cobalt.tar.gz
sha256=9c1b14a689ac8ccda9e827c2eede13bb8d781fb8e4e33c1b5360408e312127d2

doc/frama-c.kernel/Frama_c_kernel/Abstract_interp/Int/index.html

Module Abstract_interp.Int

include module type of Integer with type t = Integer.t
type 'a formatter = Format.formatter -> 'a -> unit
type t = Integer.t
val le : t -> t -> bool
val ge : t -> t -> bool
val lt : t -> t -> bool
val gt : t -> t -> bool
val add : t -> t -> t
val sub : t -> t -> t
val mul : t -> t -> t
val shift_left : t -> t -> t
val shift_right : t -> t -> t
val shift_right_logical : t -> t -> t
val logand : t -> t -> t
val logor : t -> t -> t
val logxor : t -> t -> t
val lognot : t -> t
val min : t -> t -> t
val max : t -> t -> t
val e_div : t -> t -> t

Euclidean division (that returns a positive rem). Implemented by Z.ediv

Equivalent to C division if both operands are positive. Equivalent to a floored division if b > 0 (rounds downwards), otherwise rounds upwards. Note: it is possible that e_div (-a) b <> e_div a (-b).

val e_rem : t -> t -> t

Remainder of the Euclidean division (always positive). Implemented by Z.erem

val e_div_rem : t -> t -> t * t

e_div_rem a b returns (e_div a b, e_rem a b). Implemented by Z.ediv_rem

val c_div : t -> t -> t

Truncated division towards 0 (like in C99). Implemented by Z.div

val c_rem : t -> t -> t

Remainder of the truncated division towards 0 (like in C99). Implemented by Z.rem

val c_div_rem : t -> t -> t * t

c_div_rem a b returns (c_div a b, c_rem a b). Implemented by Z.div_rem

val pgcd : t -> t -> t

pgcd v 0 == pgcd 0 v == abs v. Result is always positive

val ppcm : t -> t -> t

ppcm v 0 == ppcm 0 v == 0. Result is always positive

val cast : size:t -> signed:bool -> value:t -> t
val abs : t -> t
val neg : t -> t
val succ : t -> t
val pred : t -> t
val is_zero : t -> bool
val is_one : t -> bool
val is_even : t -> bool
val zero : t
val one : t
val two : t
val four : t
val eight : t
val sixteen : t
val thirtytwo : t
val onethousand : t
val billion_one : t
val minus_one : t
val max_int64 : t
val min_int64 : t
val two_power_32 : t
val two_power_64 : t
val length : t -> t -> t

b - a + 1

val of_int : int -> t
val of_int64 : Int64.t -> t
val of_int32 : Int32.t -> t
val to_int : t -> int
  • deprecated

    24.0-Chromium Renamed to to_int_exn. Also consider using to_int_opt.

val to_int64 : t -> int64
  • deprecated

    24.0-Chromium Renamed to to_int64_exn. Also consider using to_int64_opt.

val to_int32 : t -> int32
  • deprecated

    24.0-Chromium Renamed to to_int32_exn. Also consider using to_int32_opt.

val to_int_exn : t -> int
  • since 24.0-Chromium
val to_int64_exn : t -> int64
  • since 24.0-Chromium
val to_int32_exn : t -> int32
  • since 24.0-Chromium
val to_int_opt : t -> int option

Returns Some i if the number can be converted to an int, or None otherwise.

  • since 24.0-Chromium
val to_int64_opt : t -> int64 option

Returns Some i if the number can be converted to an int64, or None otherwise.

  • since 24.0-Chromium
val to_int32_opt : t -> int32 option

Returns Some i if the number can be converted to an int32, or None otherwise.

  • since 24.0-Chromium
val to_float : t -> float
val of_float : float -> t
val round_up_to_r : min:t -> r:t -> modu:t -> t

round_up_to_r m r modu is the smallest number n such that n>=m and n = r modulo modu

val round_down_to_r : max:t -> r:t -> modu:t -> t

round_down_to_r m r modu is the largest number n such that n<=m and n = r modulo modu

val two_power : t -> t

Computes 2^n

val two_power_of_int : int -> t

Computes 2^n

val power_int_positive_int : int -> int -> t

Exponentiation

val extract_bits : start:t -> stop:t -> t -> t
val popcount : t -> int
val to_string : t -> string
val of_string : string -> t
val pretty_hex : t formatter

Prints the integer in hexadecimal format (replaces hexa optional argument of pretty from older versions).

  • since 25.0-Manganese
val pp_bin : ?nbits:int -> ?sep:string -> t formatter

Print binary format. Digits are output by blocs of 4 bits separated by ~sep with at least ~nbits total bits. If nbits is non positive, it will be ignored.

Positive values are prefixed with "0b" and negative values are printed as their 2-complement (lnot) with prefix "1b".

val pp_hex : ?nbits:int -> ?sep:string -> t formatter

Print hexadecimal format. Digits are output by blocs of 16 bits (4 hex digits) separated by ~sep with at least ~nbits total bits. If nbits is non positive, it will be ignored.

Positive values are preffixed with "0x" and negative values are printed as their 2-complement (lnot) with prefix "1x".

include Lattice_type.Lattice_Value with type t := t
include Datatype.S with type t := t
include Datatype.S_no_copy with type t := t
include Datatype.Ty with type t := t
val ty : t Type.t
val name : string

Unique name of the datatype.

val descr : t Descr.t

Datatype descriptor.

val packed_descr : Structural_descr.pack

Packed version of the descriptor.

val reprs : t list

List of representants of the descriptor.

val equal : t -> t -> bool

Equality: same spec than Stdlib.(=).

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

val hash : t -> int

Hash function: same spec than Hashtbl.hash.

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

Pretty print each value in an user-friendly way.

val mem_project : (Project_skeleton.t -> bool) -> t -> bool

mem_project f x must return true iff there is a value p of type Project.t in x such that f p returns true.

val copy : t -> t

Deep copy: no possible sharing between x and copy x.

module Set : Datatype.Set with type elt = t
module Map : Datatype.Map with type key = t
module Hashtbl : Datatype.Hashtbl with type key = t
val fold : (t -> 'a -> 'a) -> inf:t -> sup:t -> step:t -> 'a -> 'a

Fold the function on the value between inf and sup at every step. If step is positive the first value is inf and values go increasing, if step is negative the first value is sup and values go decreasing