minor simpl of SMT query for noreturn
MODIFY
tests/alive-tv/attrs/noreturn-fail-2.srctgt.ll
tests/alive-tv/attrs/noreturn-fail-2.srctgt.ll
@@ -10,4 +10,4 @@ define i8 @tgt() {
ret i8 0
}
-; ERROR: Target or source may never return
+; ERROR: Source and target don't have the same return domain

MODIFY
tests/alive-tv/attrs/noreturn-fail-4.srctgt.ll
tests/alive-tv/attrs/noreturn-fail-4.srctgt.ll
@@ -10,4 +10,4 @@ define i8 @tgt() {
ret i8 0
}
-; ERROR: Target or source may never return
+; ERROR: Source and target don't have the same return domain

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -363,10 +363,10 @@ check_refinement(Errors &errs, Transform &t, State &src_state, State &tgt_state,
err(r, [](ostream&, const Model&){},
"Source is more defined than target");
}},
- { mk_fml(fndom_a && ((!dom_a && dom_b) || (dom_a && !dom_b))),
+ { mk_fml((fndom_a && fndom_b) && dom_a != dom_b),
[&](const Result &r) {
err(r, [](ostream&, const Model&){},
- "Target or source may never return");
+ "Source and target don't have the same return domain");
}},
{ mk_fml(dom && !poison_cnstr),
[&](const Result &r) {

MODIFY
util/symexec.cpp
util/symexec.cpp
@@ -50,7 +50,8 @@ void sym_exec(State &s) {
}
if (config::symexec_print_each_value) {
- cout << "domain = " << s.returnDomain()
+ cout << "domain = " << s.functionDomain()
+ << "\nreturn domain = " << s.returnDomain()
<< "\nreturn = " << s.returnVal().first
<< s.returnMemory() << "\n\n";
}

minor simpl of SMT query for noreturn