Method implies

ir/state.cpp:941–957

}

expr State::FnCallInput::implies(const FnCallInput &rhs) const {
  if (noret != rhs.noret || willret != rhs.willret ||
      (rhs.memaccess.canReadSomething().isTrue() &&
        (fncall_ranges != rhs.fncall_ranges || is_neq(m <=> rhs.m))))
    return false;

  AndExpr eq;
  eq.add(memaccess.refinedBy(rhs.memaccess));
  for (unsigned i = 0, e = args_nonptr.size(); i != e; ++i) {
    eq.add(args_nonptr[i].implies(rhs.args_nonptr[i]));
  }

  for (unsigned i = 0, e = args_ptr.size(); i != e; ++i) {
    eq.add(args_ptr[i].implies(rhs.args_ptr[i]));
  }
  return eq();
}

expr State::FnCallInput::refinedBy(
  State &s, const string &callee, unsigned inaccessible_bid,