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.