Skip to content

Commit

Permalink
JBMC: CProver.getCurrentThreadID:()I conversion fix
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
Degiorgio committed Jul 8, 2018
1 parent c6f9231 commit 9059be7
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 3 deletions.
Original file line number Diff line number Diff line change
@@ -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
Original file line number Diff line number Diff line change
Expand Up @@ -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);

Expand Down Expand Up @@ -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);

Expand Down

0 comments on commit 9059be7

Please sign in to comment.