Module CostModels.JavaString
val substring_aux : begin_idx:IR.Exp.t -> end_v:BO.BufferOverrunDomain.Val.t -> BO.BufferOverrunUtils.ModelEnv.model_env -> BO.BufferOverrunDomain.Mem.t -> CostUtils.BasicCost.tval substring_no_end : IR.Exp.t -> IR.Exp.t -> CostUtils.CostModelEnv.cost_model_env -> ret:'a -> BO.BufferOverrunDomain.Mem.t -> CostUtils.BasicCost.tval substring : IR.Exp.t -> IR.Exp.t -> CostUtils.CostModelEnv.cost_model_env -> ret:'a -> BO.BufferOverrunDomain.Mem.t -> CostUtils.BasicCost.tval indexOf_char : IR.Exp.t -> CostUtils.CostModelEnv.cost_model_env -> ret:'a -> BO.BufferOverrunDomain.Mem.t -> CostUtils.BasicCost.tO(|m|) where m is the given string and |.| is the length function
val indexOf_char_starting_from : IR.Exp.t -> IR.Exp.t -> CostUtils.CostModelEnv.cost_model_env -> ret:'a -> BO.BufferOverrunDomain.Mem.t -> CostUtils.BasicCost.tO(|m|-|n|) where m is the given string and n is the index to start searching from
val indexOf_str : IR.Exp.t -> IR.Exp.t -> CostUtils.CostModelEnv.cost_model_env -> ret:'a -> BO.BufferOverrunDomain.Mem.t -> BasicCost.tO(|m|.|n|) where m and n are the given strings