sig
  type cst = C_str of string | W_str of int64 list
  val pretty : Format.formatter -> Wp.Cstring.cst -> unit
  val str_len : Wp.Cstring.cst -> Wp.Lang.F.term -> Wp.Lang.F.pred
  val str_val : Wp.Cstring.cst -> Wp.Lang.F.term
  val str_id : Wp.Cstring.cst -> int
  val char_at : Wp.Cstring.cst -> Wp.Lang.F.term -> Wp.Lang.F.term
  val cluster : unit -> Wp.Definitions.cluster
end