sig
  type loc = M.loc
  type value = loc Memory.value
  type sigma = M.Sigma.t
  val cval : value -> Lang.F.term
  val cloc : value -> loc
  val cast : Cil_types.typ -> Cil_types.typ -> value -> value
  val equal_typ : Cil_types.typ -> value -> value -> Lang.F.pred
  val equal_obj : Ctypes.c_object -> value -> value -> Lang.F.pred
  val exp : sigma -> Cil_types.exp -> value
  val cond : sigma -> Cil_types.exp -> Lang.F.pred
  val lval : sigma -> Cil_types.lval -> loc
  val call : sigma -> Cil_types.exp -> loc
  val loc_of_exp : sigma -> Cil_types.exp -> loc
  val val_of_exp : sigma -> Cil_types.exp -> Lang.F.term
  val return : sigma -> Cil_types.typ -> Cil_types.exp -> Lang.F.term
  val is_zero : sigma -> Ctypes.c_object -> loc -> Lang.F.pred
  val is_zero_range :
    sigma ->
    loc -> Ctypes.c_object -> Lang.F.term -> Lang.F.term -> Lang.F.pred
  val instance_of : loc -> Cil_types.kernel_function -> Lang.F.pred
end