CBMC
java_bytecode_concurrency_instrumentation.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Java Convert Thread blocks
4 
5 Author: Kurt Degiogrio, kurt.degiorgio@diffblue.com
6 
7 \*******************************************************************/
8 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONCURRENCY_INSTRUMENTATION_H
9 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONCURRENCY_INSTRUMENTATION_H
10 
11 class message_handlert;
12 class symbol_tablet;
13 
14 void convert_threadblock(symbol_tablet &symbol_table);
15 void convert_synchronized_methods(
16  symbol_tablet &symbol_table,
17  message_handlert &message_handler);
18 
19 #endif
symbol_tablet
The symbol table.
Definition: symbol_table.h:13
message_handlert
Definition: message.h:27
convert_synchronized_methods
void convert_synchronized_methods(symbol_tablet &symbol_table, message_handlert &message_handler)
Iterate through the symbol table to find and instrument synchronized methods.
Definition: java_bytecode_concurrency_instrumentation.cpp:605
convert_threadblock
void convert_threadblock(symbol_tablet &symbol_table)
Iterate through the symbol table to find and appropriately instrument thread-blocks.
Definition: java_bytecode_concurrency_instrumentation.cpp:487