Method compareFunctions

llvm_util/compare.cpp:99–176

} // namespace

bool Verifier::compareFunctions(llvm::Function &F1, llvm::Function &F2) {
  auto r = verify(F1, F2, TLI, smt_init, out, !config::quiet, always_verify);
  if (r.status == Results::ERROR) {
    out << "ERROR: " << r.error;
    ++num_errors;
    return true;
  }

  if (print_dot) {
    r.t.src.writeDot("src");
    r.t.tgt.writeDot("tgt");
  }

  if (r.errs.hasWarnings())
    r.errs.printWarnings(out);

  switch (r.status) {
  case Results::ERROR:
    UNREACHABLE();
    break;

  case Results::SYNTACTIC_EQ:
    out << "Transformation seems to be correct! (syntactically equal)\n\n";
    ++num_correct;
    break;

  case Results::CORRECT:
    out << "Transformation seems to be correct!\n\n";
    ++num_correct;
    break;

  case Results::TYPE_CHECKER_FAILED:
    out << "Transformation doesn't verify!\n"
            "ERROR: program doesn't type check!\n\n";
    ++num_errors;
    return true;

  case Results::UNSOUND:
    out << "Transformation doesn't verify!\n\n";
    if (!config::quiet)
      out << r.errs << endl;
    ++num_unsound;
    return false;

  case Results::FAILED_TO_PROVE:
    out << r.errs << endl;
    ++num_failed;
    return true;
  }

  if (bidirectional) {
    r = verify(F2, F1, TLI, smt_init, out, false, always_verify);
    switch (r.status) {
    case Results::ERROR:
    case Results::TYPE_CHECKER_FAILED:
      UNREACHABLE();
      break;