Show an error message if the programs cant reach a return stmt
Nothing is verified in this case
MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -371,7 +371,8 @@ check_refinement(Errors &errs, Transform &t, State &src_state, State &tgt_state,
expr axioms_expr = axioms();
expr dom = dom_a && dom_b;
- pre_tgt &= !tgt_state.sinkDomain();
+ auto sink_tgt = tgt_state.sinkDomain();
+ pre_tgt &= !sink_tgt;
expr pre_src_exists = pre_src, pre_src_forall = true;
{
@@ -402,6 +403,18 @@ check_refinement(Errors &errs, Transform &t, State &src_state, State &tgt_state,
: value_cnstr && memory_cnstr0;
qvars.insert(mem_undef.begin(), mem_undef.end());
+ if (dom_a.isFalse()) {
+ errs.add("The source program doesn't reach a return instruction.\n"
+ "Consider increasing the unroll factor if it has loops", false);
+ return;
+ }
+
+ if (sink_tgt.isTrue()) {
+ errs.add("The target program doesn't reach a return instruction.\n"
+ "Consider increasing the unroll factor if it has loops", false);
+ return;
+ }
+
if (check_expr(axioms_expr && (pre_src && pre_tgt)).isUnsat()) {
errs.add("Precondition is always false", false);
return;

Show an error message if the programs cant reach a return stmt
Nothing is verified in this case