| 1374 | } |
| 1375 | |
| 1376 | pair<unique_ptr<State>, unique_ptr<State>> TransformVerify::exec() const { |
| 1377 | ScopedWatch symexec_watch([](auto &w) { |
| 1378 | if (w.seconds() > 5) |
| 1379 | dbg() << "WARNING: slow vcgen! Took " << w << '\n'; |
| 1380 | }); |
| 1381 | |
| 1382 | t.tgt.syncDataWithSrc(t.src); |
| 1383 | calculateAndInitConstants(t); |
| 1384 | State::resetGlobals(); |
| 1385 | |
| 1386 | auto src_state = make_unique<State>(t.src, true); |
| 1387 | auto tgt_state = make_unique<State>(t.tgt, false); |
| 1388 | sym_exec(*src_state); |
| 1389 | tgt_state->syncSEdataWithSrc(*src_state); |
| 1390 | src_state->cleanup(); |
| 1391 | sym_exec(*tgt_state); |
| 1392 | tgt_state->cleanup(); |
| 1393 | src_state->mkAxioms(*tgt_state); |
| 1394 | |
| 1395 | return { std::move(src_state), std::move(tgt_state) }; |
| 1396 | } |
| 1397 | |
| 1398 | Errors TransformVerify::verify() const { |
| 1399 | if (!t.src.getFnAttrs().refinedBy(t.tgt.getFnAttrs())) |
no test coverage detected