Frama-C API - `Make`

Generates Loader for Compound Values

Parameters

module M : Model

val domain : Ctypes.c_object -> M.loc -> Sigma.domain

val load : Sigma.sigma -> Ctypes.c_object -> M.loc -> M.loc Memory.value

val load_init : Sigma.sigma -> Ctypes.c_object -> M.loc -> Lang.F.term

val load_value : Sigma.sigma -> Ctypes.c_object -> M.loc -> Lang.F.term

val memcpy : Sigma.sigma Memory.sequence -> Ctypes.c_object -> ?lsrc:M.loc -> M.loc -> Memory.equation list

val memcpy_length : Sigma.sigma Memory.sequence -> Ctypes.c_object -> ?lsrc:M.loc -> M.loc -> Lang.F.term -> Memory.equation list

val stored : Sigma.sigma Memory.sequence -> Ctypes.c_object -> M.loc -> Lang.F.term -> Memory.equation list

val stored_init : Sigma.sigma Memory.sequence -> Ctypes.c_object -> M.loc -> Lang.F.term -> Memory.equation list

val copied : Sigma.sigma Memory.sequence -> Ctypes.c_object -> M.loc -> M.loc -> Memory.equation list

val copied_init : Sigma.sigma Memory.sequence -> Ctypes.c_object -> M.loc -> M.loc -> Memory.equation list

val assigned : Sigma.sigma Memory.sequence -> Ctypes.c_object -> M.loc Memory.sloc -> Memory.equation list

val initialized : Sigma.sigma -> M.loc Memory.rloc -> Lang.F.pred