Module `MemLoader.Make`Source

Generates Loader for Compound Values

Parameters

module M : Model

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

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

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

Sourceval 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

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