Skip to content

Commit d5b5aee

Browse files
committed
Constant-time compute a goto_programt::targett from const_targett
This enables use of const_targett is almost all cases, with actual modification using this on-demand conversion.
1 parent 4e97468 commit d5b5aee

File tree

1 file changed

+13
-0
lines changed

1 file changed

+13
-0
lines changed

src/goto-programs/goto_program_template.h

+13
Original file line numberDiff line numberDiff line change
@@ -248,6 +248,19 @@ class goto_program_templatet
248248
//! The list of instructions in the goto program
249249
instructionst instructions;
250250

251+
// Convert a const_targett to a targett - use with care and avoid
252+
// whenever possible
253+
targett const_cast_target(const_targett t)
254+
{
255+
return instructions.erase(t, t);
256+
}
257+
258+
// Dummy for templates with possible const contexts
259+
const_targett const_cast_target(const_targett t) const
260+
{
261+
return t;
262+
}
263+
251264
void get_successors(
252265
targett target,
253266
targetst &successors);

0 commit comments

Comments
 (0)