Skip to content

Commit e2ee53b

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 e2ee53b

File tree

1 file changed

+7
-1
lines changed

1 file changed

+7
-1
lines changed

src/goto-programs/lazy_goto_model.h

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

246+
goto_functionst::goto_functiont &get_goto_function_writable(
247+
const irep_idt &id)
248+
{
249+
return goto_functions.at(id);
250+
}
251+
246252
/// Check that the goto model is well-formed
247253
///
248254
/// The validation mode indicates whether well-formedness check failures are
@@ -263,7 +269,7 @@ class lazy_goto_modelt : public abstract_goto_modelt
263269
symbol_tablet &symbol_table;
264270

265271
private:
266-
const lazy_goto_functions_mapt goto_functions;
272+
lazy_goto_functions_mapt goto_functions;
267273
language_filest language_files;
268274

269275
// Function/module processing functions

0 commit comments

Comments
 (0)