JBMC: CProver.getCurrentThreadID:()I conversion fix

Degiorgio · Degiorgio · commit 9059be7ec5da · 2018-07-08T18:15:23.000+01:00
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.
diff --git 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
@@ -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);
 
