MemLoader.Make
Generates Loader for Compound Values
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 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