From 9059be7ec5da411f7b880bb84dffeed2461394ed Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Sun, 8 Jul 2018 13:01:33 +0100 Subject: [PATCH] JBMC: CProver.getCurrentThreadID:()I conversion fix The symbol table was being passed by-value instead of by-reference to 'instrument_getCurrentThreadID', causing an assertion violation in symex due to missing symbols. This function is responsible for converting calls to 'CProver.getCurrentThreadID:()I' into the appropriate codet. This bug was not detected by existing regression tests as in typical scenarios the aforementioned function does not add new symbols. --- jbmc/regression/jbmc-concurrency/get-current-thread/test.desc | 2 +- .../java_bytecode_concurrency_instrumentation.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc index 500630ed419..ff0c14e3779 100644 --- a/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc +++ b/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc @@ -1,6 +1,6 @@ CORE A.class ---function 'A.me:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +--function 'A.me:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL diff --git a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp index 7f37854913f..5c2a590d34d 100644 --- a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp @@ -354,7 +354,7 @@ static void instrument_start_thread( static void instrument_endThread( const code_function_callt &f_code, codet &code, - symbol_tablet symbol_table) + const symbol_tablet &symbol_table) { PRECONDITION(f_code.arguments().size() == 1); @@ -391,7 +391,7 @@ static void instrument_endThread( static void instrument_getCurrentThreadID( const code_function_callt &f_code, codet &code, - symbol_tablet symbol_table) + symbol_tablet &symbol_table) { PRECONDITION(f_code.arguments().size() == 0);