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

Parameters

module M : Model

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

val load : M.Sigma.t -> Ctypes.c_object -> M.loc -> M.loc Sigs.value

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 havoc : 
  M.Sigma.t Sigs.sequence ->
  Ctypes.c_object ->
  M.loc ->
  Sigs.equation list

val havoc_length : 
  M.Sigma.t Sigs.sequence ->
  Ctypes.c_object ->
  M.loc ->
  Lang.F.term ->
  Sigs.equation list

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

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

val copied : 
  M.Sigma.t Sigs.sequence ->
  Ctypes.c_object ->
  M.loc ->
  M.loc ->
  Sigs.equation list

val copied_init : 
  M.Sigma.t Sigs.sequence ->
  Ctypes.c_object ->
  M.loc ->
  M.loc ->
  Sigs.equation list

val assigned : 
  M.Sigma.t Sigs.sequence ->
  Ctypes.c_object ->
  M.loc Sigs.sloc ->
  Sigs.equation list

val initialized : M.Sigma.t -> M.loc Sigs.rloc -> Lang.F.pred