CBMC: /home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/lambda_synthesis.h File Reference

CBMC

Loading...

Searching...

No Matches

lambda_synthesis.h File Reference

Java lambda code synthesis. More...

#include <java_bytecode/java_bytecode_parse_tree.h>
#include <java_bytecode/synthetic_methods_map.h>
#include <util/irep.h>

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

codet invokedynamic_synthetic_method (const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)

Create invokedynamic synthetic method.

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 475 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_id synthetic 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_table will gain local variable symbols

message_handler log

Returns: the method body for function_id

Definition at line 773 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.