docs: def _eval_target_jumptable(state, ip, limit):
          """
          A *very* fast method to evaluate symbolic jump targets if they are a) concrete targets, or b) targets coming
          from jump tables.
  
          :param state:   A SimState instance.
          :param ip:      The AST of the instruction pointer to evaluate.
          :param limit:   The maximum number of concrete IPs.
          :return:        A list of conditions and the corresponding concrete IPs, or None which indicates fallback is
                          necessary.
          :rtype:         list or None
          """
  
          if ip.symbolic is False:
              return [ (claripy.ast.bool.true, ip) ]  # concrete
  
          # Detect whether ip is in the form of "if a == 1 then addr_0 else if a == 2 then addr_1 else ..."
          cond_and_targets = [ ]  # tuple of (condition, target)
  
          ip_ = ip
          # Handle the outer Reverse
          outer_reverse = False
          if ip_.op == "Reverse":
              ip_ = ip_.args[0]
              outer_reverse = True
  
          fallback = False
          target_variable = None
          concretes = set()
          reached_sentinel = False
  
          for cond, target in claripy.reverse_ite_cases(ip_):
              # We must fully unpack the entire AST to make sure it indeed complies with the form above
              if reached_sentinel:
                  # We should not have any other value beyond the sentinel - maybe one of the possible targets happens to
                  # be the same as the sentinel value?
                  fallback = True
                  break
  
              if target.symbolic is False and state.solver.eval(target) == DUMMY_SYMBOLIC_READ_VALUE:
                  # Ignore the dummy value, which acts as the sentinel of this ITE tree
                  reached_sentinel = True
                  continue
  
              if cond.op != "__eq__":
                  # We only support equivalence right now. Fallback
                  fallback = True
                  break
  
              if cond.args[0].symbolic is True and cond.args[1].symbolic is False:
                  variable, value = cond.args
              elif cond.args[0].symbolic is False and cond.args[1].symbolic is True:
                  value, variable = cond.args
              else:
                  # Cannot determine variable and value. Fallback
                  fallback = True
                  break
  
              if target_variable is None:
                  target_variable = variable
              elif target_variable is not variable:
                  # it's checking a different variable. Fallback
                  fallback = True
                  break
  
              # Make sure the conditions are mutually exclusive
              value_concrete = state.solver.eval(value)
              if value_concrete in concretes:
                  # oops... the conditions are not mutually exclusive
                  fallback = True
                  break
              concretes.add(value_concrete)
  
              if target.symbolic is True:
                  # Cannot handle symbolic targets. Fallback
                  fallback = True
                  break
  
              cond_and_targets.append((cond, target if not outer_reverse else state.solver.Reverse(target)))
  
          if reached_sentinel is False:
              # huh?
              fallback = True
  
          if fallback:
              return None
          else:
              return cond_and_targets[ : limit]