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