docs: def _string_to_int(s, state, region, base, signed, read_length=None):
          """
          reads values from s and generates the symbolic number that it would equal
          the first char is either a number in the given base, or the result is 0
          expression indicates whether or not it was successful
          """
  
          # if length wasn't provided, read the maximum bytes
          length = state.libc.max_strtol_len if read_length is None else read_length
  
          # expression whether or not it was valid at all
          expression, _ = strtol._char_to_val(region.load(s, 1), base)
  
          cases = []
  
          # to detect overflows we keep it in a larger bv and extract it at the end
          num_bits = min(state.arch.bits*2, 128)
          current_val = state.solver.BVV(0, num_bits)
          num_bytes = state.solver.BVS("num_bytes", state.arch.bits)
          constraints_num_bytes = []
          conditions = []
  
          cutoff = False
          # we need all the conditions to hold except the last one to have found a value
          for i in range(length):
              char = region.load(s + i, 1)
              condition, value = strtol._char_to_val(char, base)
  
              # if it was the end we'll get the current val
              cases.append((num_bytes == i, current_val))
  
              # identify the constraints necessary to set num_bytes to the current value
              # the current char (i.e. the terminator if this is satisfied) should not be a char,
              # so `condition` should be false, plus all the previous conditions should be satisfied
              case_constraints = conditions + [state.solver.Not(condition)] + [num_bytes == i]
              constraints_num_bytes.append(state.solver.And(*case_constraints))
  
              # break the loop early if no value past this is viable
              if condition.is_false():
                  cutoff = True  # ???
                  break
  
              # add the value and the condition
              current_val = current_val*base + value.zero_extend(num_bits-8)
              conditions.append(condition)
  
          # the last one is unterminated, let's ignore it
          if not cutoff:
              cases.append((num_bytes == length, current_val))
              case_constraints = conditions + [num_bytes == length]
              constraints_num_bytes.append(state.solver.And(*case_constraints))
  
          # only one of the constraints need to hold
          # since the constraints look like (num_bytes == 2 and the first 2 chars are valid, and the 3rd isn't)
  
          final_constraint = state.solver.Or(*constraints_num_bytes)
          if final_constraint.op == '__eq__' and final_constraint.args[0] is num_bytes and not final_constraint.args[1].symbolic:
              # CONCRETE CASE
              result = cases[state.solver.eval(final_constraint.args[1])][1]
              num_bytes = final_constraint.args[1]
          else:
              # symbolic case
              state.add_constraints(final_constraint)
              result = state.solver.ite_cases(cases, 0)
  
          # overflow check
          max_bits = state.arch.bits-1 if signed else state.arch.bits
          max_val = 2**max_bits - 1
          result = state.solver.If(result < max_val, state.solver.Extract(state.arch.bits-1, 0, result),
                               state.solver.BVV(max_val, state.arch.bits))
  
          return expression, result, num_bytes