cprover
Loading...
Searching...
No Matches
java_bytecode_typecheckt Class Reference

#include <java_bytecode_typecheck.h>

Inheritance diagram for java_bytecode_typecheckt:
Collaboration diagram for java_bytecode_typecheckt:

Public Member Functions

 java_bytecode_typecheckt (symbol_table_baset &_symbol_table, message_handlert &_message_handler, bool _string_refinement_enabled)
virtual ~java_bytecode_typecheckt ()
virtual void typecheck ()
void typecheck (const journalling_symbol_tablet::changesett &identifiers)
virtual void typecheck_expr (exprt &expr)
Public Member Functions inherited from typecheckt
 typecheckt (message_handlert &_message_handler)
virtual ~typecheckt ()
virtual bool typecheck_main ()
Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
message_handlert & get_message_handler ()
 messaget (const messaget &other)
messaget & operator= (const messaget &other)
 messaget (message_handlert &_message_handler)
virtual ~messaget ()
mstreamt & get_mstream (unsigned message_level) const
mstreamt & error () const
mstreamt & warning () const
mstreamt & result () const
mstreamt & status () const
mstreamt & statistics () const
mstreamt & progress () const
mstreamt & debug () const
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to message_stream using output_generator if the configured verbosity is at least as high as that of message_stream.

Protected Member Functions

void typecheck_type_symbol (symbolt &)
void typecheck_non_type_symbol (symbolt &)
void typecheck_code (codet &)
void typecheck_type (typet &)
void typecheck_expr_symbol (symbol_exprt &)
void typecheck_expr_java_new (side_effect_exprt &)
void typecheck_expr_java_new_array (side_effect_exprt &)
virtual std::string to_string (const exprt &expr)
virtual std::string to_string (const typet &type)

Protected Attributes

symbol_table_baset & symbol_table
const namespacet ns
bool string_refinement_enabled
std::set< irep_idt > already_typechecked
Protected Attributes inherited from messaget
message_handlert * message_handler
mstreamt mstream

Additional Inherited Members

Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1 , M_WARNING =2 , M_RESULT =4 , M_STATUS =6 ,
  M_STATISTICS =8 , M_PROGRESS =9 , M_DEBUG =10
}
Static Public Member Functions inherited from messaget
static unsigned eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
 Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest.
static commandt command (unsigned c)
 Create an ECMA-48 SGR (Select Graphic Rendition) command.
Static Public Attributes inherited from messaget
static eomt eom
static const commandt reset
 return to default formatting, as defined by the terminal
static const commandt red
 render text with red foreground color
static const commandt green
 render text with green foreground color
static const commandt yellow
 render text with yellow foreground color
static const commandt blue
 render text with blue foreground color
static const commandt magenta
 render text with magenta foreground color
static const commandt cyan
 render text with cyan foreground color
static const commandt bright_red
 render text with bright red foreground color
static const commandt bright_green
 render text with bright green foreground color
static const commandt bright_yellow
 render text with bright yellow foreground color
static const commandt bright_blue
 render text with bright blue foreground color
static const commandt bright_magenta
 render text with bright magenta foreground color
static const commandt bright_cyan
 render text with bright cyan foreground color
static const commandt bold
 render text with bold font
static const commandt faint
 render text with faint font
static const commandt italic
 render italic text
static const commandt underline
 render underlined text

Detailed Description

Definition at line 39 of file java_bytecode_typecheck.h.

Constructor & Destructor Documentation

◆ java_bytecode_typecheckt()

java_bytecode_typecheckt::java_bytecode_typecheckt ( symbol_table_baset & _symbol_table,
message_handlert & _message_handler,
bool _string_refinement_enabled )
inline

Definition at line 42 of file java_bytecode_typecheck.h.

◆ ~java_bytecode_typecheckt()

virtual java_bytecode_typecheckt::~java_bytecode_typecheckt ( )
inlinevirtual

Definition at line 53 of file java_bytecode_typecheck.h.

Member Function Documentation

◆ to_string() [1/2]

std::string java_bytecode_typecheckt::to_string ( const exprt & expr)
protectedvirtual

Definition at line 16 of file java_bytecode_typecheck.cpp.

◆ to_string() [2/2]

std::string java_bytecode_typecheckt::to_string ( const typet & type)
protectedvirtual

Definition at line 21 of file java_bytecode_typecheck.cpp.

◆ typecheck() [1/2]

void java_bytecode_typecheckt::typecheck ( )
virtual

Implements typecheckt.

Definition at line 33 of file java_bytecode_typecheck.cpp.

◆ typecheck() [2/2]

void java_bytecode_typecheckt::typecheck ( const journalling_symbol_tablet::changesett & identifiers)

Definition at line 44 of file java_bytecode_typecheck.cpp.

◆ typecheck_code()

void java_bytecode_typecheckt::typecheck_code ( codet & code)
protected

Definition at line 18 of file java_bytecode_typecheck_code.cpp.

◆ typecheck_expr()

void java_bytecode_typecheckt::typecheck_expr ( exprt & expr)
virtual

Definition at line 20 of file java_bytecode_typecheck_expr.cpp.

◆ typecheck_expr_java_new()

void java_bytecode_typecheckt::typecheck_expr_java_new ( side_effect_exprt & expr)
protected

Definition at line 53 of file java_bytecode_typecheck_expr.cpp.

◆ typecheck_expr_java_new_array()

void java_bytecode_typecheckt::typecheck_expr_java_new_array ( side_effect_exprt & expr)
protected

Definition at line 60 of file java_bytecode_typecheck_expr.cpp.

◆ typecheck_expr_symbol()

void java_bytecode_typecheckt::typecheck_expr_symbol ( symbol_exprt & expr)
protected

Definition at line 68 of file java_bytecode_typecheck_expr.cpp.

◆ typecheck_non_type_symbol()

void java_bytecode_typecheckt::typecheck_non_type_symbol ( symbolt & symbol)
protected

Definition at line 26 of file java_bytecode_typecheck.cpp.

◆ typecheck_type()

void java_bytecode_typecheckt::typecheck_type ( typet & type)
protected

Definition at line 19 of file java_bytecode_typecheck_type.cpp.

◆ typecheck_type_symbol()

void java_bytecode_typecheckt::typecheck_type_symbol ( symbolt & symbol)
protected

Definition at line 55 of file java_bytecode_typecheck_type.cpp.

Member Data Documentation

◆ already_typechecked

std::set<irep_idt> java_bytecode_typecheckt::already_typechecked
protected

Definition at line 76 of file java_bytecode_typecheck.h.

◆ ns

const namespacet java_bytecode_typecheckt::ns
protected

Definition at line 61 of file java_bytecode_typecheck.h.

◆ string_refinement_enabled

bool java_bytecode_typecheckt::string_refinement_enabled
protected

Definition at line 62 of file java_bytecode_typecheck.h.

◆ symbol_table

symbol_table_baset& java_bytecode_typecheckt::symbol_table
protected

Definition at line 60 of file java_bytecode_typecheck.h.

The documentation for this class was generated from the following files: