sig
  module M : Model
  type loc = M.loc
  type nonrec value = Wp.Sigs.CodeSemantics.loc Wp.Sigs.value
  type nonrec result = Wp.Sigs.CodeSemantics.loc Wp.Sigs.result
  type sigma = M.Sigma.t
  val pp_value : Format.formatter -> Wp.Sigs.CodeSemantics.value -> unit
  val cval : Wp.Sigs.CodeSemantics.value -> Wp.Lang.F.term
  val cloc : Wp.Sigs.CodeSemantics.value -> Wp.Sigs.CodeSemantics.loc
  val cast :
    Cil_types.typ ->
    Cil_types.typ ->
    Wp.Sigs.CodeSemantics.value -> Wp.Sigs.CodeSemantics.value
  val equal_typ :
    Cil_types.typ ->
    Wp.Sigs.CodeSemantics.value ->
    Wp.Sigs.CodeSemantics.value -> Wp.Lang.F.pred
  val not_equal_typ :
    Cil_types.typ ->
    Wp.Sigs.CodeSemantics.value ->
    Wp.Sigs.CodeSemantics.value -> Wp.Lang.F.pred
  val equal_obj :
    Wp.Ctypes.c_object ->
    Wp.Sigs.CodeSemantics.value ->
    Wp.Sigs.CodeSemantics.value -> Wp.Lang.F.pred
  val not_equal_obj :
    Wp.Ctypes.c_object ->
    Wp.Sigs.CodeSemantics.value ->
    Wp.Sigs.CodeSemantics.value -> Wp.Lang.F.pred
  val exp :
    Wp.Sigs.CodeSemantics.sigma ->
    Cil_types.exp -> Wp.Sigs.CodeSemantics.value
  val cond : Wp.Sigs.CodeSemantics.sigma -> Cil_types.exp -> Wp.Lang.F.pred
  val lval :
    Wp.Sigs.CodeSemantics.sigma ->
    Cil_types.lval -> Wp.Sigs.CodeSemantics.loc
  val call :
    Wp.Sigs.CodeSemantics.sigma -> Cil_types.exp -> Wp.Sigs.CodeSemantics.loc
  val instance_of :
    Wp.Sigs.CodeSemantics.loc -> Cil_types.kernel_function -> Wp.Lang.F.pred
  val loc_of_exp :
    Wp.Sigs.CodeSemantics.sigma -> Cil_types.exp -> Wp.Sigs.CodeSemantics.loc
  val val_of_exp :
    Wp.Sigs.CodeSemantics.sigma -> Cil_types.exp -> Wp.Lang.F.term
  val result :
    Wp.Sigs.CodeSemantics.sigma ->
    Cil_types.typ -> Wp.Sigs.CodeSemantics.result -> Wp.Lang.F.term
  val return :
    Wp.Sigs.CodeSemantics.sigma ->
    Cil_types.typ -> Cil_types.exp -> Wp.Lang.F.term
  val is_zero :
    Wp.Sigs.CodeSemantics.sigma ->
    Wp.Ctypes.c_object -> Wp.Sigs.CodeSemantics.loc -> Wp.Lang.F.pred
  val is_exp_range :
    Wp.Sigs.CodeSemantics.sigma ->
    Wp.Sigs.CodeSemantics.loc ->
    Wp.Ctypes.c_object ->
    Wp.Lang.F.term ->
    Wp.Lang.F.term -> Wp.Sigs.CodeSemantics.value option -> Wp.Lang.F.pred
  val unchanged : M.sigma -> M.sigma -> Cil_types.varinfo -> Wp.Lang.F.pred
  type warned_hyp = Wp.Warning.Set.t * Wp.Lang.F.pred
  val init :
    sigma:M.sigma ->
    Cil_types.varinfo ->
    Cil_types.init option -> Wp.Sigs.CodeSemantics.warned_hyp list
end