CBMC
java_bytecode_typecheck.cpp File Reference

JAVA Bytecode Conversion / Type Checking. More...

#include "java_bytecode_typecheck.h"
#include "expr2java.h"
+ Include dependency graph for java_bytecode_typecheck.cpp:

Go to the source code of this file.

Functions

bool java_bytecode_typecheck (symbol_table_baset &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
 
void java_bytecode_typecheck_updated_symbols (journalling_symbol_tablet &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
 
bool java_bytecode_typecheck (exprt &expr, message_handlert &message_handler, const namespacet &ns)
 

Detailed Description

JAVA Bytecode Conversion / Type Checking.

Definition in file java_bytecode_typecheck.cpp.

Function Documentation

◆ java_bytecode_typecheck() [1/2]

bool java_bytecode_typecheck ( exprt expr,
message_handlert message_handler,
const namespacet ns 
)

Definition at line 84 of file java_bytecode_typecheck.cpp.

◆ java_bytecode_typecheck() [2/2]

bool java_bytecode_typecheck ( symbol_table_baset symbol_table,
message_handlert message_handler,
bool  string_refinement_enabled 
)

Definition at line 64 of file java_bytecode_typecheck.cpp.

◆ java_bytecode_typecheck_updated_symbols()

void java_bytecode_typecheck_updated_symbols ( journalling_symbol_tablet symbol_table,
message_handlert message_handler,
bool  string_refinement_enabled 
)

Definition at line 74 of file java_bytecode_typecheck.cpp.