Frama-C API - Bitvector
Bitvectors.
val create : int -> tCreate a vector of n bits, with all bits unset.
val create_set : int -> tCreate a vector of n bits, with all bits set.
val capacity : t -> intMaximum number of bits in the bitvector.
A copy of the bitvector up-to or down-to n bits. Extra bits up to final bitvector capacity are set to zero.
val mem : t -> int -> boolval set : t -> int -> unitval clear : t -> int -> unitval once : t -> int -> boolreturn true if unset, then set the bit.
val set_range : t -> int -> int -> unitval is_empty : t -> boolval hash : t -> intBitwise Binary Operations
The first argument is the size of the vectors.
Generic Bitwise Operations
Prefer using these rather than create intermediary bitvectors.
Sized Concatenation
concat b1 s1 b2 s2 concatenates the s1 first bits of b1 with the s2 first bits of b2.
Misc
val iter_true : (int -> unit) -> t -> unitIterates on all indexes of the bitvector with their bit set.
val fold_true : ('a -> int -> 'a) -> 'a -> t -> 'aIterates on all indexes of the bitvector with their bit set.
val find_next_true : t -> int -> intfind_next_true i a returns the first index greater or equal to i with its bit set. To find the first true element, call find_next_true -1 a. If no next true element exists, or i is larger than the array, then raise Not_found.
val pretty : Stdlib.Format.formatter -> t -> unitBit vector, as blocs of 8-bits separated by space, first bits to last bits from left to right.
