Make (frama-c-wp.Wp.MemLoader.Make)

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 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