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