Module `MemLoader.Make`Source

Generates Loader for Compound Values

Parameters

module M : Model

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

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

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

Sourceval 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

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