CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
lambda_synthesis.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Java lambda code synthesis
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_JAVA_BYTECODE_LAMBDA_SYNTHESIS_H
13#define CPROVER_JAVA_BYTECODE_LAMBDA_SYNTHESIS_H
14
17#include <util/irep.h>
18
20class codet;
22
25 std::size_t instruction_address);
26
30 symbol_table_baset &symbol_table,
31 synthetic_methods_mapt &synthetic_methods,
32 message_handlert &message_handler);
33
36 const irep_idt &function_id,
37 symbol_table_baset &symbol_table,
38 message_handlert &message_handler);
39
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Data structure for representing an arbitrary statement in a program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
The symbol table base class interface.
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)
codet invokedynamic_synthetic_constructor(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Create invokedynamic synthetic constructor.
codet invokedynamic_synthetic_method(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Create invokedynamic synthetic method.
irep_idt lambda_synthetic_class_name(const irep_idt &method_identifier, std::size_t instruction_address)
std::vector< instructiont > instructionst
Synthetic methods are particular methods internally generated by the Java frontend,...
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.