Skip to content

Commit 782090c

Browse files
committed
replace usage of assert()
This replaces two uses of the assert() macro by DATA_INVARIANT.
1 parent d44c808 commit 782090c

File tree

1 file changed

+4
-2
lines changed

1 file changed

+4
-2
lines changed

src/analyses/goto_check_c.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -314,7 +314,9 @@ void goto_check_ct::collect_allocations(const goto_functionst &goto_functions)
314314
throw "expected two unsigned arguments to " CPROVER_PREFIX
315315
"allocated_memory";
316316

317-
assert(args[0].type() == args[1].type());
317+
DATA_INVARIANT(
318+
args[0].type() == args[1].type(),
319+
"arguments of allocated_memory must have same type");
318320
allocations.push_back({args[0], args[1]});
319321
}
320322
}
@@ -1028,7 +1030,7 @@ void goto_check_ct::float_overflow_check(const exprt &expr, const guardt &guard)
10281030
}
10291031
else if(expr.operands().size() >= 3)
10301032
{
1031-
assert(expr.id() != ID_minus);
1033+
DATA_INVARIANT(expr.id() != ID_minus, "minus expression must be binary");
10321034

10331035
// break up
10341036
float_overflow_check(make_binary(expr), guard);

0 commit comments

Comments
 (0)