package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Interval semantics.
Misc.

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/Int_interval/index.html

Module `Frama_c_kernel.Int_interval`

Integer intervals with congruence. An interval defined by min, max, rem, modu represents all integers between the bounds min and max and congruent to rem modulo modu. A value of None for min (resp. max) represents -infinity (resp. +infinity). modu is > 0, and 0 <= rem < modu.

include Datatype.S_with_collections

include Datatype.S

include Datatype.S_no_copy

include Datatype.Ty

type t

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

module Set : Datatype.Set with type elt = t

module Map : Datatype.Map with type key = t

module Hashtbl : Datatype.Hashtbl with type key = t

include Eva_lattice_type.Full_AI_Lattice_with_cardinality
  with type t := t
   and type widen_hint = Integer.t * Datatype.Integer.Set.t

include Eva_lattice_type.AI_Lattice_with_cardinal_one
  with type t := t
  with type widen_hint = Integer.t * Datatype.Integer.Set.t

include Eva_lattice_type.Join_Semi_Lattice with type t := t

datatype of element of the lattice

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

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

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.(=).

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

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.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

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.

val join : t -> t -> t

over-approximation of union

val is_included : t -> t -> bool

is first argument included in the second?

include Eva_lattice_type.With_Top with type t := t

val top : t

largest element

include Eva_lattice_type.With_Widening
  with type t := t
  with type widen_hint = Integer.t * Datatype.Integer.Set.t

type widen_hint = Integer.t * Datatype.Integer.Set.t

hints for the widening

val widen : widen_hint -> t -> t -> t

widen h t1 t2 is an over-approximation of join t1 t2. Assumes is_included t1 t2

include Eva_lattice_type.With_Cardinal_One with type t := t

val cardinal_zero_or_one : t -> bool

include Eva_lattice_type.With_Narrow with type t := t

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

over-approximation of intersection

include Eva_lattice_type.With_Under_Approximation with type t := t

val link : t -> t -> t

under-approximation of union

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

under-approximation of intersection

include Eva_lattice_type.With_Intersects with type t := t

val intersects : t -> t -> bool

intersects t1 t2 returns true iff the intersection of t1 and t2 is non-empty.

include Eva_lattice_type.With_Diff with type t := t

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

diff t1 t2 is an over-approximation of t1-t2. t2 must be an under-approximation or exact.

include Eva_lattice_type.With_Diff_One with type t := t

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

diff_if_one t1 t2 is an over-approximation of t1-t2.

returns
t1 if t2 is not a singleton.

include Eva_lattice_type.With_Enumeration with type t := t

val fold_enum : (t -> 'a -> 'a) -> t -> 'a -> 'a

Fold on the elements of the value one by one if possible. Raises Abstract_interp.Not_less_than when there is an infinite number of elements to enumerate.

val cardinal_less_than : t -> int -> int

Raises Abstract_interp.Not_less_than whenever the cardinal of the given lattice is strictly higher than the given integer.

val check : 
  min:Integer.t option ->
  max:Integer.t option ->
  rem:Integer.t ->
  modu:Integer.t ->
  unit

Checks that the interval defined by min, max, rem, modu is well formed.

val make : 
  min:Integer.t option ->
  max:Integer.t option ->
  rem:Integer.t ->
  modu:Integer.t ->
  t

Makes the interval of all integers between min and max and congruent to rem modulo modu. Fails if these conditions does not hold:

min ≤ max
0 ≤ rem < modu
min ≅ rem modu ∧ max ≅ rem modu

val inject_range : Integer.t option -> Integer.t option -> t

Makes the interval of all integers between min and max.

val min_and_max : t -> Integer.t option * Integer.t option

Returns the bounds of the given interval. None means infinity.

val min_max_rem_modu : 
  t ->
  Integer.t option * Integer.t option * Integer.t * Integer.t

Returns the bounds and the modulo of the given interval.

val mem : Integer.t -> t -> bool

mem i t returns true iff the integer i is in the interval t.

val cardinal : t -> Integer.t option

Returns the number of integers represented by the given interval. Returns None if the interval represents an infinite number of integers.

val complement_under : 
  min:Integer.t ->
  max:Integer.t ->
  t ->
  t Lattice_bounds.or_bottom

Returns an under-approximation of the integers between min and max that are *not* represented by the given interval.

Interval semantics.

See Int_val for more details.

val add_singleton_int : Integer.t -> t -> t

val add : t -> t -> t

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

val neg : t -> t

val abs : t -> t

val scale : Integer.t -> t -> t

val scale_div : pos:bool -> Integer.t -> t -> t

val scale_div_under : pos:bool -> Integer.t -> t -> t Lattice_bounds.or_bottom

val scale_rem : pos:bool -> Integer.t -> t -> t

val mul : t -> t -> t

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

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

val cast : size:Integer.t -> signed:bool -> t -> t

Misc.

val subdivide : t -> t * t

val reduce_sign : t -> bool -> t Lattice_bounds.or_bottom

val reduce_bit : int -> t -> bool -> t Lattice_bounds.or_bottom

val fold_int : ?increasing:bool -> (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a

val to_seq : ?increasing:bool -> t -> Integer.t Seq.t