CBMC
lambda_synthesis.h File Reference

Java lambda code synthesis. More...

+ Include dependency graph for lambda_synthesis.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

irep_idt lambda_synthetic_class_name (const irep_idt &method_identifier, std::size_t instruction_address)
 
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. More...
 
codet invokedynamic_synthetic_method (const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
 Create invokedynamic synthetic method. More...
 

Detailed Description

Java lambda code synthesis.

Definition in file lambda_synthesis.h.

Function Documentation

◆ 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 at line 395 of file lambda_synthesis.cpp.

◆ 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 at line 471 of file lambda_synthesis.cpp.

◆ 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.

Create invokedynamic synthetic method.

For most lambdas this means creating a simple function body like TR new_synthetic_method(T1 param1, T2 param2, ...) { return target_method(capture1, capture2, ..., param1, param2, ...); }, where the first parameter might be a this parameter. For a constructor method, the generated code will be of the form TNew new_synthetic_method(T1 param1, T2 param2, ...) { return new TNew(capture1, capture2, ..., param1, param2, ...); } i.e. the TNew object will be both instantiated and constructed.

Parameters
function_idsynthetic method whose body should be generated; information about the lambda method to generate has already been stored in the symbol table by create_invokedynamic_synthetic_classes.
symbol_tablewill gain local variable symbols
message_handlerlog
Returns
the method body for function_id

Definition at line 769 of file lambda_synthesis.cpp.

◆ lambda_synthetic_class_name()

irep_idt lambda_synthetic_class_name ( const irep_idt method_identifier,
std::size_t  instruction_address 
)

Definition at line 37 of file lambda_synthesis.cpp.