Skip to content

Commit 1f6ca60

Browse files
Make locality a static function
locality is only used in symex_function_call.cpp, it can be made static. This simplifies the symex interface and is potentially more efficient.
1 parent b5986a7 commit 1f6ca60

File tree

2 files changed

+11
-9
lines changed

2 files changed

+11
-9
lines changed

src/goto-symex/goto_symex.h

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -310,11 +310,6 @@ class goto_symext
310310
statet &,
311311
const exprt::operandst &arguments);
312312

313-
void locality(
314-
const irep_idt &function_identifier,
315-
statet &,
316-
const goto_functionst::goto_functiont &);
317-
318313
// exceptions
319314
void symex_throw(statet &);
320315
void symex_catch(statet &);

src/goto-symex/symex_function_call.cpp

Lines changed: 11 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,12 @@ Author: Daniel Kroening, kroening@kroening.com
1818
#include <util/exception_utils.h>
1919
#include <util/invariant.h>
2020

21+
static void locality(
22+
const irep_idt &function_identifier,
23+
goto_symext::statet &state,
24+
const goto_functionst::goto_functiont &goto_function,
25+
const namespacet &ns);
26+
2127
bool goto_symext::get_unwind_recursion(const irep_idt &, unsigned, unsigned)
2228
{
2329
return false;
@@ -300,7 +306,7 @@ void goto_symext::symex_function_call_code(
300306
framet &frame = state.new_frame();
301307

302308
// preserve locality of local variables
303-
locality(identifier, state, goto_function);
309+
locality(identifier, state, goto_function, ns);
304310

305311
// assign actuals to formal parameters
306312
parameter_assignments(identifier, goto_function, state, arguments);
@@ -378,10 +384,11 @@ void goto_symext::symex_end_of_function(statet &state)
378384

379385
/// preserves locality of local variables of a given function by applying L1
380386
/// renaming to the local identifiers
381-
void goto_symext::locality(
387+
static void locality(
382388
const irep_idt &function_identifier,
383-
statet &state,
384-
const goto_functionst::goto_functiont &goto_function)
389+
goto_symext::statet &state,
390+
const goto_functionst::goto_functiont &goto_function,
391+
const namespacet &ns)
385392
{
386393
unsigned &frame_nr=
387394
state.threads[state.source.thread_nr].function_frame[function_identifier];

0 commit comments

Comments
 (0)