package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Some bit manipulations.

val sizeofchar : unit -> Integer.t

sizeof(char) in bits

val sizeofpointer : unit -> int

sizeof(char* ) in bits

val sizeof : Cil_types.typ -> Int_Base.t

sizeof ty is the size of ty in bits. This function may return Int_Base.top.

val osizeof : Cil_types.typ -> Int_Base.t

osizeof ty is the size of ty in bytes. This function may return Int_Base.top.

exception Neither_Int_Nor_Enum_Nor_Pointer
val is_signed_int_enum_pointer : Cil_types.typ -> bool

true means that the type is signed.

val signof_typeof_lval : Cil_types.lval -> bool
  • returns

    the sign of type of the lval. true means that the type is signed.

val sizeof_vid : Cil_types.varinfo -> Int_Base.t
  • returns

    the size of the type of the variable in bits.

val sizeof_lval : Cil_types.lval -> Int_Base.t
  • returns

    the size of the type of the left value in bits.

val sizeof_pointed : Cil_types.typ -> Int_Base.t
  • returns

    the size of the type pointed by a pointer or array type in bits. Never call it on a non pointer or non array type .

val osizeof_pointed : Cil_types.typ -> Int_Base.t
  • returns

    the size of the type pointed by a pointer or array type in bytes. Never call it on a non pointer or array type.

val sizeof_pointed_lval : Cil_types.lval -> Int_Base.t
  • returns

    the size of the type pointed by a pointer type of the lval in bits. Never call it on a non pointer type lval.

val max_bit_address : unit -> Integer.t
  • returns

    the maximal possible offset in bits of a memory base.

val max_bit_size : unit -> Integer.t
  • returns

    the maximal possible size in bits of a memory base.

val max_byte_address : unit -> Integer.t
  • returns

    the maximal possible offset in bytes of a memory base.

  • since Aluminium-20160501
val max_byte_size : unit -> Integer.t
  • returns

    the maximal possible size in bytes of a memory base.

  • since Aluminium-20160501

Pretty printing

val pretty_bits : Cil_types.typ -> use_align:bool -> align:Abstract_interp.Rel.t -> rh_size:Integer.t -> start:Integer.t -> stop:Integer.t -> Format.formatter -> bool * Cil_types.typ option

Pretty prints a range of bits in a type for the user. Tries to find field names and array indexes, whenever possible.

Mapping from numeric offsets to symbolic ones.

val type_compatible : Cil_types.typ -> Cil_types.typ -> bool

Comparison of the shape of two types. Attributes are completely ignored.

type offset_match =
  1. | MatchType of Cil_types.typ
    (*

    Offset that has this type (modulo attributes)

    *)
  2. | MatchSize of Integer.t
    (*

    Offset that has a type of this size

    *)
  3. | MatchFirst
    (*

    Return first symbolic offset that matches

    *)

We want to find a symbolic offset that corresponds to a numeric one, with one additional criterion:

exception NoMatchingOffset

find_offset typ ~offset ~size finds a subtype t of typ that describes the type of the bits offset..offset+size-1 in typ. May return a subtype of typ, or a type that is a sub-array of an array type in typ. Also returns a Cil_types.offset off that corresponds to offset. (But we do not have the guarantee that typeof(off) == typ, because of sub-arrays.)

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct