cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
message_handlert
Definition
message.h:27
symbol_table_baset
The symbol table base class interface.
Definition
symbol_table_base.h:23
irep.h
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:475
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:773
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
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
jbmc
src
java_bytecode
lambda_synthesis.h
Generated by
1.17.0