Skip to content

Commit 6eb0d2f

Browse files
author
Enrico Steffinlongo
committed
Improve goto_symex_state.cpp diagnostics
This commit changes the `INVARIANT_WITH_DIAGNOSTIC` in `goto_symex_statet::rename` to be more precise.
1 parent 5ff2fe0 commit 6eb0d2f

File tree

1 file changed

+17
-8
lines changed

1 file changed

+17
-8
lines changed

src/goto-symex/goto_symex_state.cpp

Lines changed: 17 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -280,14 +280,23 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
280280
expr.type() = to_with_expr(expr).old().type();
281281
}
282282
INVARIANT_WITH_DIAGNOSTICS(
283-
(expr.id() != ID_with ||
284-
c_expr.type() == to_with_expr(c_expr).old().type()) &&
285-
(expr.id() != ID_if ||
286-
(c_expr.type() == to_if_expr(c_expr).true_case().type() &&
287-
c_expr.type() == to_if_expr(c_expr).false_case().type())),
288-
"Type of renamed expr should be the same as operands for with_exprt and "
289-
"if_exprt",
290-
irep_pretty_diagnosticst{expr});
283+
expr.id() != ID_with ||
284+
c_expr.type() == to_with_expr(c_expr).old().type(),
285+
"Type of renamed expr should be the same as operands for with_exprt",
286+
c_expr.type().pretty(),
287+
to_with_expr(c_expr).old().type().pretty());
288+
INVARIANT_WITH_DIAGNOSTICS(
289+
expr.id() != ID_if ||
290+
c_expr.type() == to_if_expr(c_expr).true_case().type(),
291+
"Type of renamed expr should be the same as operands for if_exprt",
292+
c_expr.type().pretty(),
293+
to_if_expr(c_expr).true_case().type().pretty());
294+
INVARIANT_WITH_DIAGNOSTICS(
295+
expr.id() != ID_if ||
296+
c_expr.type() == to_if_expr(c_expr).false_case().type(),
297+
"Type of renamed expr should be the same as operands for if_exprt",
298+
c_expr.type().pretty(),
299+
to_if_expr(c_expr).false_case().type().pretty());
291300

292301
if(level == L2)
293302
expr = field_sensitivity.apply(ns, *this, std::move(expr), false);

0 commit comments

Comments
 (0)