CBMC
lambda_synthesis.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Java lambda code synthesis
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_JAVA_BYTECODE_LAMBDA_SYNTHESIS_H
13 #define CPROVER_JAVA_BYTECODE_LAMBDA_SYNTHESIS_H
14 
15 #include <java_bytecode/java_bytecode_parse_tree.h>
16 #include <java_bytecode/synthetic_methods_map.h>
17 #include <util/irep.h>
18 
19 class message_handlert;
20 class codet;
21 class symbol_table_baset;
22 
23 irep_idt lambda_synthetic_class_name(
24  const irep_idt &method_identifier,
25  std::size_t instruction_address);
26 
27 void create_invokedynamic_synthetic_classes(
28  const irep_idt &method_identifier,
29  const java_bytecode_parse_treet::methodt::instructionst &instructions,
30  symbol_table_baset &symbol_table,
31  synthetic_methods_mapt &synthetic_methods,
32  message_handlert &message_handler);
33 
35 codet invokedynamic_synthetic_constructor(
36  const irep_idt &function_id,
37  symbol_table_baset &symbol_table,
38  message_handlert &message_handler);
39 
41 codet invokedynamic_synthetic_method(
42  const irep_idt &function_id,
43  symbol_table_baset &symbol_table,
44  message_handlert &message_handler);
45 
46 #endif // CPROVER_JAVA_BYTECODE_LAMBDA_SYNTHESIS_H
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
message_handlert
Definition: message.h:28
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:23
java_bytecode_parse_tree.h
create_invokedynamic_synthetic_classes
void create_invokedynamic_synthetic_classes(const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt::instructionst &instructions, symbol_table_baset &symbol_table, synthetic_methods_mapt &synthetic_methods, message_handlert &message_handler)
Definition: lambda_synthesis.cpp:395
invokedynamic_synthetic_constructor
codet invokedynamic_synthetic_constructor(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Create invokedynamic synthetic constructor.
Definition: lambda_synthesis.cpp:471
invokedynamic_synthetic_method
codet invokedynamic_synthetic_method(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Create invokedynamic synthetic method.
Definition: lambda_synthesis.cpp:769
lambda_synthetic_class_name
irep_idt lambda_synthetic_class_name(const irep_idt &method_identifier, std::size_t instruction_address)
Definition: lambda_synthesis.cpp:37
java_bytecode_parse_treet::methodt::instructionst
std::vector< instructiont > instructionst
Definition: java_bytecode_parse_tree.h:91
synthetic_methods_map.h
Synthetic methods are particular methods internally generated by the Java frontend,...
synthetic_methods_mapt
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.
Definition: synthetic_methods_map.h:57