#include <jsil_typecheck.h>

Inheritance diagram for jsil_typecheckt:

Collaboration diagram for jsil_typecheckt:

Public Member Functions
	jsil_typecheckt (symbol_table_baset &_symbol_table, message_handlert &_message_handler)

virtual	~jsil_typecheckt ()

virtual void	typecheck ()

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 ()

	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`. More...

Protected Member Functions
void	update_expr_type (exprt &expr, const typet &type)

void	make_type_compatible (exprt &expr, const typet &type, bool must)

void	typecheck_type_symbol (symbolt &)

void	typecheck_non_type_symbol (symbolt &symbol)
	typechecking procedure declaration; any other symbols should have been typechecked during typechecking of procedure declaration More...

void	typecheck_symbol_expr (symbol_exprt &symbol_expr)

void	typecheck_expr_side_effect_throw (side_effect_expr_throwt &expr)

void	typecheck_expr_delete (exprt &expr)

void	typecheck_expr_index (exprt &expr)

void	typecheck_expr_proto_field (exprt &expr)

void	typecheck_expr_proto_obj (exprt &expr)

void	typecheck_expr_has_field (exprt &expr)

void	typecheck_expr_ref (exprt &expr)

void	typecheck_expr_field (exprt &expr)

void	typecheck_expr_base (exprt &expr)

void	typecheck_expr_constant (exprt &expr)

void	typecheck_expr_concatenation (exprt &expr)

void	typecheck_expr_subtype (exprt &expr)

void	typecheck_expr_binary_boolean (exprt &expr)

void	typecheck_expr_binary_arith (exprt &expr)

void	typecheck_exp_binary_equal (exprt &expr)

void	typecheck_expr_binary_compare (exprt &expr)

void	typecheck_expr_unary_boolean (exprt &expr)

void	typecheck_expr_unary_string (exprt &expr)

void	typecheck_expr_unary_num (exprt &expr)

void	typecheck_expr_operands (exprt &expr)

void	typecheck_expr_main (exprt &expr)

void	typecheck_code (codet &code)

void	typecheck_function_call (code_function_callt &function_call)

void	typecheck_return (code_frontend_returnt &)

void	typecheck_block (codet &code)

void	typecheck_ifthenelse (code_ifthenelset &code)

void	typecheck_assign (code_assignt &code)

void	typecheck_try_catch (code_try_catcht &code)

void	typecheck_type (typet &type)

irep_idt	add_prefix (const irep_idt &ds)
	Prefix parameters and variables with a procedure name. More...

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

irep_idt	proc_name

std::unordered_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. More...

static commandt	command (unsigned c)
	Create an ECMA-48 SGR (Select Graphic Rendition) command. More...

Static Public Attributes inherited from messaget
static eomt	eom

static const commandt	reset
	return to default formatting, as defined by the terminal More...

static const commandt	red
	render text with red foreground color More...

static const commandt	green
	render text with green foreground color More...

static const commandt	yellow
	render text with yellow foreground color More...

static const commandt	blue
	render text with blue foreground color More...

static const commandt	magenta
	render text with magenta foreground color More...

static const commandt	cyan
	render text with cyan foreground color More...

static const commandt	bright_red
	render text with bright red foreground color More...

static const commandt	bright_green
	render text with bright green foreground color More...

static const commandt	bright_yellow
	render text with bright yellow foreground color More...

static const commandt	bright_blue
	render text with bright blue foreground color More...

static const commandt	bright_magenta
	render text with bright magenta foreground color More...

static const commandt	bright_cyan
	render text with bright cyan foreground color More...

static const commandt	bold
	render text with bold font More...

static const commandt	faint
	render text with faint font More...

static const commandt	italic
	render italic text More...

static const commandt	underline
	render underlined text More...

Detailed Description

Definition at line 40 of file jsil_typecheck.h.

Constructor & Destructor Documentation

◆ jsil_typecheckt()

jsil_typecheckt::jsil_typecheckt	(	symbol_table_baset &	_symbol_table,
		message_handlert &	_message_handler
	)

inline

Definition at line 43 of file jsil_typecheck.h.

◆ ~jsil_typecheckt()

virtual jsil_typecheckt::~jsil_typecheckt ( )

inlinevirtual

Definition at line 53 of file jsil_typecheck.h.

Member Function Documentation

◆ add_prefix()

irep_idt jsil_typecheckt::add_prefix ( const irep_idt & ds )

protected

Prefix parameters and variables with a procedure name.

Definition at line 35 of file jsil_typecheck.cpp.

◆ make_type_compatible()

void jsil_typecheckt::make_type_compatible	(	exprt &	expr,
		const typet &	type,
		bool	must
	)

protected

Definition at line 63 of file jsil_typecheck.cpp.

◆ to_string() [1/2]

std::string jsil_typecheckt::to_string ( const exprt & expr )

protectedvirtual

Definition at line 24 of file jsil_typecheck.cpp.

◆ to_string() [2/2]

std::string jsil_typecheckt::to_string ( const typet & type )

protectedvirtual

Definition at line 29 of file jsil_typecheck.cpp.

◆ typecheck()

void jsil_typecheckt::typecheck ( )

virtual

Implements typecheckt.

Definition at line 870 of file jsil_typecheck.cpp.

◆ typecheck_assign()

void jsil_typecheckt::typecheck_assign ( code_assignt & code )

protected

Definition at line 827 of file jsil_typecheck.cpp.

◆ typecheck_block()

void jsil_typecheckt::typecheck_block ( codet & code )

protected

Definition at line 689 of file jsil_typecheck.cpp.

◆ typecheck_code()

void jsil_typecheckt::typecheck_code ( codet & code )

protected

Definition at line 635 of file jsil_typecheck.cpp.

◆ typecheck_exp_binary_equal()

void jsil_typecheckt::typecheck_exp_binary_equal ( exprt & expr )

protected

Definition at line 489 of file jsil_typecheck.cpp.

◆ typecheck_expr()

void jsil_typecheckt::typecheck_expr ( exprt & expr )

virtual

Definition at line 140 of file jsil_typecheck.cpp.

◆ typecheck_expr_base()

void jsil_typecheckt::typecheck_expr_base ( exprt & expr )

protected

Definition at line 386 of file jsil_typecheck.cpp.

◆ typecheck_expr_binary_arith()

void jsil_typecheckt::typecheck_expr_binary_arith ( exprt & expr )

protected

Definition at line 474 of file jsil_typecheck.cpp.

◆ typecheck_expr_binary_boolean()

void jsil_typecheckt::typecheck_expr_binary_boolean ( exprt & expr )

protected

Definition at line 459 of file jsil_typecheck.cpp.

◆ typecheck_expr_binary_compare()

void jsil_typecheckt::typecheck_expr_binary_compare ( exprt & expr )

protected

Definition at line 503 of file jsil_typecheck.cpp.

◆ typecheck_expr_concatenation()

void jsil_typecheckt::typecheck_expr_concatenation ( exprt & expr )

protected

Definition at line 429 of file jsil_typecheck.cpp.

◆ typecheck_expr_constant()

void jsil_typecheckt::typecheck_expr_constant ( exprt & expr )

protected

Definition at line 281 of file jsil_typecheck.cpp.

◆ typecheck_expr_delete()

void jsil_typecheckt::typecheck_expr_delete ( exprt & expr )

protected

Definition at line 321 of file jsil_typecheck.cpp.

◆ typecheck_expr_field()

void jsil_typecheckt::typecheck_expr_field ( exprt & expr )

protected

Definition at line 372 of file jsil_typecheck.cpp.

◆ typecheck_expr_has_field()

void jsil_typecheckt::typecheck_expr_has_field ( exprt & expr )

protected

Definition at line 357 of file jsil_typecheck.cpp.

◆ typecheck_expr_index()

void jsil_typecheckt::typecheck_expr_index ( exprt & expr )

protected

Definition at line 336 of file jsil_typecheck.cpp.

◆ typecheck_expr_main()

void jsil_typecheckt::typecheck_expr_main ( exprt & expr )

protected

Definition at line 155 of file jsil_typecheck.cpp.

◆ typecheck_expr_operands()

void jsil_typecheckt::typecheck_expr_operands ( exprt & expr )

protected

Definition at line 149 of file jsil_typecheck.cpp.

◆ typecheck_expr_proto_field()

void jsil_typecheckt::typecheck_expr_proto_field ( exprt & expr )

protected

Definition at line 291 of file jsil_typecheck.cpp.

◆ typecheck_expr_proto_obj()

void jsil_typecheckt::typecheck_expr_proto_obj ( exprt & expr )

protected

Definition at line 306 of file jsil_typecheck.cpp.

◆ typecheck_expr_ref()

void jsil_typecheckt::typecheck_expr_ref ( exprt & expr )

protected

Definition at line 400 of file jsil_typecheck.cpp.

◆ typecheck_expr_side_effect_throw()

void jsil_typecheckt::typecheck_expr_side_effect_throw ( side_effect_expr_throwt & expr )

protected

Definition at line 272 of file jsil_typecheck.cpp.

◆ typecheck_expr_subtype()

void jsil_typecheckt::typecheck_expr_subtype ( exprt & expr )

protected

Definition at line 444 of file jsil_typecheck.cpp.

◆ typecheck_expr_unary_boolean()

void jsil_typecheckt::typecheck_expr_unary_boolean ( exprt & expr )

protected

Definition at line 518 of file jsil_typecheck.cpp.

◆ typecheck_expr_unary_num()

void jsil_typecheckt::typecheck_expr_unary_num ( exprt & expr )

protected

Definition at line 546 of file jsil_typecheck.cpp.

◆ typecheck_expr_unary_string()

void jsil_typecheckt::typecheck_expr_unary_string ( exprt & expr )

protected

Definition at line 532 of file jsil_typecheck.cpp.

◆ typecheck_function_call()

void jsil_typecheckt::typecheck_function_call ( code_function_callt & function_call )

protected

Definition at line 713 of file jsil_typecheck.cpp.

◆ typecheck_ifthenelse()

void jsil_typecheckt::typecheck_ifthenelse ( code_ifthenelset & code )

protected

Definition at line 815 of file jsil_typecheck.cpp.

◆ typecheck_non_type_symbol()

void jsil_typecheckt::typecheck_non_type_symbol ( symbolt & symbol )

protected

typechecking procedure declaration; any other symbols should have been typechecked during typechecking of procedure declaration

parameters: any symbol

Definition at line 838 of file jsil_typecheck.cpp.

◆ typecheck_return()

void jsil_typecheckt::typecheck_return ( code_frontend_returnt & code )

protected

Definition at line 683 of file jsil_typecheck.cpp.

◆ typecheck_symbol_expr()

void jsil_typecheckt::typecheck_symbol_expr ( symbol_exprt & symbol_expr )

protected

Definition at line 558 of file jsil_typecheck.cpp.

◆ typecheck_try_catch()

void jsil_typecheckt::typecheck_try_catch ( code_try_catcht & code )

protected

Definition at line 695 of file jsil_typecheck.cpp.

◆ typecheck_type()

void jsil_typecheckt::typecheck_type ( typet & type )

protected

Definition at line 102 of file jsil_typecheck.cpp.

◆ typecheck_type_symbol()

void jsil_typecheckt::typecheck_type_symbol ( symbolt & )

inlineprotected

Definition at line 66 of file jsil_typecheck.h.

◆ update_expr_type()

void jsil_typecheckt::update_expr_type	(	exprt &	expr,
		const typet &	type
	)

protected

Definition at line 40 of file jsil_typecheck.cpp.

Member Data Documentation

◆ already_typechecked

std::unordered_set<irep_idt> jsil_typecheckt::already_typechecked

protected

Definition at line 104 of file jsil_typecheck.h.

◆ ns

const namespacet jsil_typecheckt::ns

protected

Definition at line 60 of file jsil_typecheck.h.

◆ proc_name

irep_idt jsil_typecheckt::proc_name

protected

Definition at line 62 of file jsil_typecheck.h.

◆ symbol_table

symbol_table_baset& jsil_typecheckt::symbol_table

protected

Definition at line 59 of file jsil_typecheck.h.

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

/home/runner/work/cbmc-documentation/cbmc-documentation/src/jsil/jsil_typecheck.h
/home/runner/work/cbmc-documentation/cbmc-documentation/src/jsil/jsil_typecheck.cpp

Public Member Functions

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ jsil_typecheckt()

◆ ~jsil_typecheckt()

Member Function Documentation

◆ add_prefix()

◆ make_type_compatible()

◆ to_string() [1/2]

◆ to_string() [2/2]

◆ typecheck()

◆ typecheck_assign()

◆ typecheck_block()

◆ typecheck_code()

◆ typecheck_exp_binary_equal()

◆ typecheck_expr()

◆ typecheck_expr_base()

◆ typecheck_expr_binary_arith()

◆ typecheck_expr_binary_boolean()

◆ typecheck_expr_binary_compare()

◆ typecheck_expr_concatenation()

◆ typecheck_expr_constant()

◆ typecheck_expr_delete()

◆ typecheck_expr_field()

◆ typecheck_expr_has_field()

◆ typecheck_expr_index()

◆ typecheck_expr_main()

◆ typecheck_expr_operands()

◆ typecheck_expr_proto_field()

◆ typecheck_expr_proto_obj()

◆ typecheck_expr_ref()

◆ typecheck_expr_side_effect_throw()

◆ typecheck_expr_subtype()

◆ typecheck_expr_unary_boolean()

◆ typecheck_expr_unary_num()

◆ typecheck_expr_unary_string()

◆ typecheck_function_call()

◆ typecheck_ifthenelse()

◆ typecheck_non_type_symbol()

◆ typecheck_return()

◆ typecheck_symbol_expr()

◆ typecheck_try_catch()

◆ typecheck_type()

◆ typecheck_type_symbol()

◆ update_expr_type()

Member Data Documentation

◆ already_typechecked

◆ ns

◆ proc_name

◆ symbol_table