Skip to content

Commit 9059be7

Browse files
committed
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.
1 parent c6f9231 commit 9059be7

File tree

2 files changed

+3
-3
lines changed

2 files changed

+3
-3
lines changed
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A.class
3-
--function 'A.me:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
3+
--function 'A.me:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -354,7 +354,7 @@ static void instrument_start_thread(
354354
static void instrument_endThread(
355355
const code_function_callt &f_code,
356356
codet &code,
357-
symbol_tablet symbol_table)
357+
const symbol_tablet &symbol_table)
358358
{
359359
PRECONDITION(f_code.arguments().size() == 1);
360360

@@ -391,7 +391,7 @@ static void instrument_endThread(
391391
static void instrument_getCurrentThreadID(
392392
const code_function_callt &f_code,
393393
codet &code,
394-
symbol_tablet symbol_table)
394+
symbol_tablet &symbol_table)
395395
{
396396
PRECONDITION(f_code.arguments().size() == 0);
397397

0 commit comments

Comments
 (0)