Skip to content

Commit e66ccc6

Browse files
Replace asserts by invariants
1 parent 1871331 commit e66ccc6

File tree

1 file changed

+4
-3
lines changed

1 file changed

+4
-3
lines changed

src/java_bytecode/replace_java_nondet.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ Author: Reuben Thomas, [email protected]
1919
#include <goto-programs/remove_skip.h>
2020

2121
#include <util/irep_ids.h>
22+
#include <util/invariant.h>
2223

2324
/// Holds information about any discovered nondet methods, with extreme type-
2425
/// safety.
@@ -176,7 +177,7 @@ static goto_programt::targett check_and_replace_target(
176177
}
177178

178179
// Look at the next instruction, ensure that it is an assignment
179-
assert(next_instr->is_assign());
180+
INVARIANT(next_instr->is_assign(), "expected assign instruction");
180181
// Get the name of the LHS of the assignment
181182
const auto &next_instr_assign_lhs = to_code_assign(next_instr->code).lhs();
182183
if(
@@ -200,7 +201,7 @@ static goto_programt::targett check_and_replace_target(
200201
return is_assignment_from(instr, return_identifier);
201202
});
202203

203-
assert(matching_assignment != end);
204+
CHECK_RETURN(matching_assignment != end);
204205

205206
// Assume that the LHS of *this* assignment is the actual nondet variable
206207
const auto &code_assign = to_code_assign(matching_assignment->code);
@@ -209,7 +210,7 @@ static goto_programt::targett check_and_replace_target(
209210

210211
// Erase from the nondet function call to the assignment
211212
const auto after_matching_assignment = std::next(matching_assignment);
212-
assert(after_matching_assignment != end);
213+
CHECK_RETURN(after_matching_assignment != end);
213214

214215
std::for_each(
215216
target,

0 commit comments

Comments
 (0)