Skip to content

Commit 74aa09b

Browse files
smowtonthomasspriggs
authored andcommitted
Lazy goto model: allow access to mutable goto_functiont
This was previously forbidden because with symex-driven loading it's always a mistake to edit a function after symex has begun executing it, but with any load strategy which takes place entirely before symex it's ok if you're careful.
1 parent 22dc0f5 commit 74aa09b

File tree

1 file changed

+11
-1
lines changed

1 file changed

+11
-1
lines changed

src/goto-programs/lazy_goto_model.h

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -243,6 +243,16 @@ class lazy_goto_modelt : public abstract_goto_modelt
243243
return goto_functions.at(id);
244244
}
245245

246+
/// Get a goto_function_body, for the the purpose of updating it.
247+
/// With symex-driven loading it's a mistake to update a function after symex
248+
/// has begun executing it. However with any load strategy which takes place
249+
/// entirely before symex it is not a problem.
250+
goto_functionst::goto_functiont &
251+
get_goto_function_writable(const irep_idt &id)
252+
{
253+
return goto_functions.at(id);
254+
}
255+
246256
/// Check that the goto model is well-formed
247257
///
248258
/// The validation mode indicates whether well-formedness check failures are
@@ -263,7 +273,7 @@ class lazy_goto_modelt : public abstract_goto_modelt
263273
symbol_tablet &symbol_table;
264274

265275
private:
266-
const lazy_goto_functions_mapt goto_functions;
276+
lazy_goto_functions_mapt goto_functions;
267277
language_filest language_files;
268278

269279
// Function/module processing functions

0 commit comments

Comments
 (0)