void sanity_check()

in include/FiniteAbstractDomain.h [365:388]

• 22 lines of code
• 6 McCabe index (conditional complexity)

  void sanity_check(Element* index_to_element) {
    // We count the number of bit vectors that have all their bits set to one.
    size_t all_bits_are_set = 0;
    // We count the number of bit vectors that have only one bit set to one.
    size_t one_bit_is_set = 0;
    for (size_t i = 0; i < cardinality; ++i) {
      Encoding x = m_element_to_encoding[index_to_element[i]];
      if (x.all()) {
        ++all_bits_are_set;
      }
      if (x.count() == 1) {
        ++one_bit_is_set;
      }
      for (size_t j = 0; j < cardinality; ++j) {
        Encoding y = m_element_to_encoding[index_to_element[j]];
        RUNTIME_CHECK(m_encoding_to_element.find(x & y) !=
                          m_encoding_to_element.end(),
                      internal_error());
      }
    }
    RUNTIME_CHECK(all_bits_are_set == 1 && one_bit_is_set == 1,
                  internal_error()
                      << error_msg("Missing or duplicate extremal element"));
  }