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