Skip to content

Commit 4b6ed8e

Browse files
author
Owen Jones
committed
Only update goto program if it was changed
1 parent 283c4f8 commit 4b6ed8e

File tree

1 file changed

+19
-8
lines changed

1 file changed

+19
-8
lines changed

jbmc/src/java_bytecode/convert_java_nondet.cpp

Lines changed: 19 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -30,8 +30,9 @@ Author: Reuben Thomas, [email protected]
3030
/// \param symbol_table: The global symbol table.
3131
/// \param message_handler: Handles logging.
3232
/// \param max_nondet_array_length: Maximum size of new nondet arrays.
33-
/// \return The next instruction to process with this function.
34-
static goto_programt::targett insert_nondet_init_code(
33+
/// \return The next instruction to process with this function and a boolean
34+
/// indicating whether any changes were made to the goto program.
35+
static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
3536
goto_programt &goto_program,
3637
const goto_programt::targett &target,
3738
symbol_table_baset &symbol_table,
@@ -40,6 +41,7 @@ static goto_programt::targett insert_nondet_init_code(
4041
const irep_idt &mode)
4142
{
4243
const auto next_instr = std::next(target);
44+
bool changed = false;
4345

4446
// We only expect to find nondets in the rhs of an assignments or in return
4547
// statements
@@ -132,9 +134,11 @@ static goto_programt::targett insert_nondet_init_code(
132134
// Finally insert the dead instruction for aux_symbol after target
133135
goto_program.insert_after(target)->swap(
134136
aux_instructions.instructions.back());
137+
138+
changed = true;
135139
}
136140

137-
return next_instr;
141+
return std::make_pair(next_instr, changed);
138142
}
139143

140144
/// For each instruction in the goto program, checks if it is an assignment from
@@ -151,20 +155,27 @@ void convert_nondet(
151155
const object_factory_parameterst &object_factory_parameters,
152156
const irep_idt &mode)
153157
{
154-
for(auto instruction_iterator=goto_program.instructions.begin(),
155-
end=goto_program.instructions.end();
156-
instruction_iterator!=end;)
158+
bool changed = false;
159+
auto instruction_iterator = goto_program.instructions.begin();
160+
auto end = goto_program.instructions.end();
161+
162+
while(instruction_iterator != end)
157163
{
158-
instruction_iterator = insert_nondet_init_code(
164+
auto ret = insert_nondet_init_code(
159165
goto_program,
160166
instruction_iterator,
161167
symbol_table,
162168
message_handler,
163169
object_factory_parameters,
164170
mode);
171+
instruction_iterator = ret.first;
172+
changed |= ret.second;
165173
}
166174

167-
goto_program.update();
175+
if(changed)
176+
{
177+
goto_program.update();
178+
}
168179
}
169180

170181
void convert_nondet(

0 commit comments

Comments
 (0)