| 445 | |
| 446 | |
| 447 | static expr |
| 448 | encode_undef_refinement_per_elem(const Type &ty, const StateValue &sva, |
| 449 | expr &&a2, expr &&b, expr &&b2) { |
| 450 | const auto *aty = ty.getAsAggregateType(); |
| 451 | if (!aty) { |
| 452 | if (config::disallow_ub_exploitation) |
| 453 | return sva.non_poison && sva.value != a2; |
| 454 | return sva.non_poison && sva.value == a2 && b != b2; |
| 455 | } |
| 456 | |
| 457 | StateValue sva2{std::move(a2), expr()}; |
| 458 | StateValue svb{std::move(b), expr()}, svb2{std::move(b2), expr()}; |
| 459 | expr result = false; |
| 460 | |
| 461 | for (unsigned i = 0; i < aty->numElementsConst(); ++i) { |
| 462 | if (!aty->isPadding(i)) |
| 463 | result |= encode_undef_refinement_per_elem(aty->getChild(i), |
| 464 | aty->extract(sva, i), aty->extract(sva2, i).value, |
| 465 | aty->extract(svb, i).value, aty->extract(svb2, i).value); |
| 466 | } |
| 467 | return result; |
| 468 | } |
| 469 | |
| 470 | // Returns negation of refinement |
| 471 | static expr encode_undef_refinement(const State &src_state, |
no test coverage detected