| 831 | } |
| 832 | |
| 833 | void State::addJump(expr &&cond, const BasicBlock &dst0, bool always_jump) { |
| 834 | always_jump = always_jump || cond.isTrue(); |
| 835 | |
| 836 | cond &= domain.path; |
| 837 | if (cond.isFalse() || !domain) |
| 838 | return; |
| 839 | |
| 840 | auto dst = &dst0; |
| 841 | if (seen_bbs.count(dst)) { |
| 842 | dst = &f.getSinkBB(); |
| 843 | } |
| 844 | |
| 845 | auto &data = predecessor_data[dst][current_bb]; |
| 846 | if (always_jump) { |
| 847 | data.mem.add(std::move(memory), cond); |
| 848 | data.analysis = std::move(analysis); |
| 849 | data.var_args = std::move(var_args_data); |
| 850 | } else { |
| 851 | data.mem.add(memory.dup(), cond); |
| 852 | data.analysis = analysis; |
| 853 | data.var_args = var_args_data; |
| 854 | } |
| 855 | data.UB.add(domain.UB, cond); |
| 856 | data.path.add(std::move(cond)); |
| 857 | data.undef_vars.insert(undef_vars.begin(), undef_vars.end()); |
| 858 | data.undef_vars.insert(domain.undef_vars.begin(), domain.undef_vars.end()); |
| 859 | |
| 860 | if (always_jump) |
| 861 | domain.path = false; |
| 862 | } |
| 863 | |
| 864 | void State::addJump(const BasicBlock &dst) { |
| 865 | addJump(true, dst, true); |