Frama-C:
Plug-ins:
Libraries:

Frama-C API - Make

Generates Loader for Compound Values

Parameters

module M : Model

Signature

val load_init : M.Sigma.t -> Ctypes.c_object -> M.loc -> Lang.F.term
val load_value : M.Sigma.t -> Ctypes.c_object -> M.loc -> Lang.F.term
val copied_init : M.Sigma.t Sigs.sequence -> Ctypes.c_object -> M.loc -> M.loc -> Sigs.equation list
val initialized : M.Sigma.t -> M.loc Sigs.rloc -> Lang.F.pred