cprover
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 #include <util/symbol_table.h>
12 #include <util/message.h>
13 
14 void convert_threadblock(symbol_tablet &symbol_table);
16  symbol_tablet &symbol_table,
18 
19 #endif
The symbol table.
Definition: symbol_table.h:19
Author: Diffblue Ltd.
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
void convert_synchronized_methods(symbol_tablet &symbol_table, message_handlert &message_handler)
Iterate through the symbol table to find and instrument synchronized methods.
void convert_threadblock(symbol_tablet &symbol_table)
Iterate through the symbol table to find and appropriately instrument thread-blocks.