#include <expr2java.h>

Inheritance diagram for expr2javat:

Collaboration diagram for expr2javat:

Public Member Functions
	expr2javat (const namespacet &_ns)

virtual std::string	convert (const typet &src) override

virtual std::string	convert (const exprt &src) override

Public Member Functions inherited from expr2ct
	expr2ct (const namespacet &_ns, const expr2c_configurationt &configuration=expr2c_configurationt::default_configuration)

virtual	~expr2ct ()

void	get_shorthands (const exprt &expr)

std::string	convert_with_identifier (const typet &src, const std::string &identifier)
	Build a declaration string, which requires converting both a type and putting an identifier in the syntactically correct position. More...

Protected Member Functions
virtual std::string	convert_with_precedence (const exprt &src, unsigned &precedence) override

std::string	convert_java_this ()

std::string	convert_java_instanceof (const exprt &src)

std::string	convert_java_new (const exprt &src)

std::string	convert_code_java_new (const exprt &src, unsigned precedence)

std::string	convert_code_java_delete (const exprt &src, unsigned precedence)

virtual std::string	convert_struct (const exprt &src, unsigned &precedence) override

virtual std::string	convert_code (const codet &src, unsigned indent) override

virtual std::string	convert_constant (const constant_exprt &src, unsigned &precedence) override

std::string	convert_code_function_call (const code_function_callt &src, unsigned indent)

virtual std::string	convert_rec (const typet &src, const c_qualifierst &qualifiers, const std::string &declarator) override

Protected Member Functions inherited from expr2ct
virtual std::string	convert_struct_type (const typet &src, const std::string &qualifiers_str, const std::string &declarator_str)
	To generate C-like string for defining the given struct. More...

std::string	convert_struct_type (const typet &src, const std::string &qualifer_str, const std::string &declarator_str, bool inc_struct_body, bool inc_padding_components)
	To generate C-like string for declaring (or defining) the given struct. More...

virtual std::string	convert_array_type (const typet &src, const c_qualifierst &qualifiers, const std::string &declarator_str)
	To generate a C-like type declaration of an array. More...

std::string	convert_array_type (const typet &src, const c_qualifierst &qualifiers, const std::string &declarator_str, bool inc_size_if_possible)
	To generate a C-like type declaration of an array. More...

irep_idt	id_shorthand (const irep_idt &identifier) const

std::string	convert_typecast (const typecast_exprt &src, unsigned &precedence)

std::string	convert_pointer_arithmetic (const exprt &src, unsigned &precedence)

std::string	convert_pointer_difference (const exprt &src, unsigned &precedence)

std::string	convert_binary (const binary_exprt &, const std::string &symbol, unsigned precedence, bool full_parentheses)

std::string	convert_multi_ary (const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses)

std::string	convert_cond (const exprt &src, unsigned precedence)

std::string	convert_struct_member_value (const exprt &src, unsigned precedence)

std::string	convert_array_member_value (const exprt &src, unsigned precedence)

std::string	convert_member (const member_exprt &src, unsigned precedence)

std::string	convert_array_of (const exprt &src, unsigned precedence)

std::string	convert_trinary (const ternary_exprt &src, const std::string &symbol1, const std::string &symbol2, unsigned precedence)

std::string	convert_rox (const shift_exprt &src, unsigned precedence)
	Conversion function from rol/ror expressions to C code strings Note that this constructs a complex expression to do bit twiddling since rol/ror operations are not native to ANSI-C. More...

std::string	convert_overflow (const exprt &src, unsigned &precedence)

std::string	convert_binding (const binding_exprt &, const std::string &symbol, unsigned precedence)

std::string	convert_with (const exprt &src, unsigned precedence)

std::string	convert_update (const update_exprt &, unsigned precedence)

std::string	convert_member_designator (const exprt &src)

std::string	convert_index_designator (const exprt &src)

std::string	convert_index (const binary_exprt &, unsigned precedence)

std::string	convert_byte_extract (const byte_extract_exprt &, unsigned precedence)

std::string	convert_byte_update (const byte_update_exprt &, unsigned precedence)

std::string	convert_extractbit (const extractbit_exprt &, unsigned precedence)

std::string	convert_extractbits (const extractbits_exprt &src, unsigned precedence)

std::string	convert_unary (const unary_exprt &, const std::string &symbol, unsigned precedence)

std::string	convert_unary_post (const exprt &src, const std::string &symbol, unsigned precedence)

std::optional< std::string >	convert_function (const exprt &src)
	Returns a string if `src` is a function with a known conversion, else returns nullopt. More...

std::string	convert_function (const exprt &src, const std::string &symbol)

std::string	convert_complex (const exprt &src, unsigned precedence)

std::string	convert_comma (const exprt &src, unsigned precedence)

std::string	convert_Hoare (const exprt &src)

std::string	convert_code (const codet &src)

std::string	convert_code_label (const code_labelt &src, unsigned indent)

std::string	convert_code_switch_case (const code_switch_caset &src, unsigned indent)

std::string	convert_code_asm (const code_asmt &src, unsigned indent)

std::string	convert_code_frontend_assign (const code_frontend_assignt &, unsigned indent)

std::string	convert_code_ifthenelse (const code_ifthenelset &src, unsigned indent)

std::string	convert_code_for (const code_fort &src, unsigned indent)

std::string	convert_code_while (const code_whilet &src, unsigned indent)

std::string	convert_code_dowhile (const code_dowhilet &src, unsigned indent)

std::string	convert_code_block (const code_blockt &src, unsigned indent)

std::string	convert_code_expression (const codet &src, unsigned indent)

std::string	convert_code_return (const codet &src, unsigned indent)

std::string	convert_code_goto (const codet &src, unsigned indent)

std::string	convert_code_assume (const codet &src, unsigned indent)

std::string	convert_code_assert (const codet &src, unsigned indent)

std::string	convert_code_break (unsigned indent)

std::string	convert_code_switch (const codet &src, unsigned indent)

std::string	convert_code_continue (unsigned indent)

std::string	convert_code_frontend_decl (const codet &, unsigned indent)

std::string	convert_code_decl_block (const codet &src, unsigned indent)

std::string	convert_code_dead (const codet &src, unsigned indent)

std::string	convert_code_function_call (const code_function_callt &src, unsigned indent)

std::string	convert_code_lock (const codet &src, unsigned indent)

std::string	convert_code_unlock (const codet &src, unsigned indent)

std::string	convert_code_printf (const codet &src, unsigned indent)

std::string	convert_code_fence (const codet &src, unsigned indent)

std::string	convert_code_input (const codet &src, unsigned indent)

std::string	convert_code_output (const codet &src, unsigned indent)

std::string	convert_code_array_set (const codet &src, unsigned indent)

std::string	convert_code_array_copy (const codet &src, unsigned indent)

std::string	convert_code_array_replace (const codet &src, unsigned indent)

std::string	convert_function_application (const function_application_exprt &src)

std::string	convert_side_effect_expr_function_call (const side_effect_expr_function_callt &src)

std::string	convert_allocate (const exprt &src, unsigned &precedence)

std::string	convert_nondet (const exprt &src, unsigned &precedence)

std::string	convert_prob_coin (const exprt &src, unsigned &precedence)

std::string	convert_prob_uniform (const exprt &src, unsigned &precedence)

std::string	convert_statement_expression (const exprt &src, unsigned &precendence)

virtual std::string	convert_symbol (const exprt &src)

std::string	convert_predicate_symbol (const exprt &src)

std::string	convert_predicate_next_symbol (const exprt &src)

std::string	convert_predicate_passive_symbol (const exprt &src)

std::string	convert_nondet_symbol (const nondet_symbol_exprt &)

std::string	convert_quantified_symbol (const exprt &src)

std::string	convert_nondet_bool ()

std::string	convert_object_descriptor (const exprt &src, unsigned &precedence)

std::string	convert_literal (const exprt &src)

virtual std::string	convert_constant_bool (bool boolean_value)
	To get the C-like representation of a given boolean value. More...

virtual std::string	convert_annotated_pointer_constant (const annotated_pointer_constant_exprt &src, unsigned &precedence)

std::string	convert_norep (const exprt &src, unsigned &precedence)

std::string	convert_union (const exprt &src, unsigned &precedence)

std::string	convert_vector (const exprt &src, unsigned &precedence)

std::string	convert_array (const exprt &src)

std::string	convert_array_list (const exprt &src, unsigned &precedence)

std::string	convert_initializer_list (const exprt &src)

std::string	convert_designated_initializer (const exprt &src)

std::string	convert_concatenation (const exprt &src, unsigned &precedence)

std::string	convert_sizeof (const exprt &src, unsigned &precedence)

std::string	convert_let (const let_exprt &, unsigned precedence)

std::string	convert_struct (const exprt &src, unsigned &precedence, bool include_padding_components)
	To generate a C-like string representing a struct. More...

std::string	convert_conditional_target_group (const exprt &src)

std::string	convert_bitreverse (const bitreverse_exprt &src)

std::string	convert_r_or_w_ok (const r_or_w_ok_exprt &src)

std::string	convert_prophecy_r_or_w_ok (const prophecy_r_or_w_ok_exprt &src)

std::string	convert_pointer_in_range (const pointer_in_range_exprt &src)

std::string	convert_prophecy_pointer_in_range (const prophecy_pointer_in_range_exprt &src)

Protected Attributes
const std::size_t	char_representation_length =8

Protected Attributes inherited from expr2ct
const namespacet &	ns

const expr2c_configurationt &	configuration

std::unordered_map< irep_idt, std::unordered_set< irep_idt > >	ns_collision

std::unordered_map< irep_idt, irep_idt >	shorthands

unsigned	sizeof_nesting

Additional Inherited Members
Static Protected Member Functions inherited from expr2ct
static std::string	indent_str (unsigned indent)

Detailed Description

Definition at line 19 of file expr2java.h.

Constructor & Destructor Documentation

◆ expr2javat()

expr2javat::expr2javat ( const namespacet & _ns )

inlineexplicit

Definition at line 22 of file expr2java.h.

Member Function Documentation

◆ convert() [1/2]

std::string expr2javat::convert ( const exprt & src )

overridevirtual

Reimplemented from expr2ct.

Definition at line 30 of file expr2java.cpp.

◆ convert() [2/2]

std::string expr2javat::convert ( const typet & src )

overridevirtual

Reimplemented from expr2ct.

Definition at line 25 of file expr2java.cpp.

◆ convert_code()

std::string expr2javat::convert_code	(	const codet &	src,
		unsigned	indent
	)

overrideprotectedvirtual

Reimplemented from expr2ct.

Definition at line 438 of file expr2java.cpp.

◆ convert_code_function_call()

std::string expr2javat::convert_code_function_call	(	const code_function_callt &	src,
		unsigned	indent
	)

protected

Definition at line 35 of file expr2java.cpp.

◆ convert_code_java_delete()

std::string expr2javat::convert_code_java_delete	(	const exprt &	src,
		unsigned	precedence
	)

protected

Definition at line 358 of file expr2java.cpp.

◆ convert_code_java_new()

std::string expr2javat::convert_code_java_new	(	const exprt &	src,
		unsigned	precedence
	)

protected

Definition at line 329 of file expr2java.cpp.

◆ convert_constant()

std::string expr2javat::convert_constant	(	const constant_exprt &	src,
		unsigned &	precedence
	)

overrideprotectedvirtual

Reimplemented from expr2ct.

Definition at line 169 of file expr2java.cpp.

◆ convert_java_instanceof()

std::string expr2javat::convert_java_instanceof ( const exprt & src )

protected

Definition at line 321 of file expr2java.cpp.

◆ convert_java_new()

std::string expr2javat::convert_java_new ( const exprt & src )

protected

Definition at line 334 of file expr2java.cpp.

◆ convert_java_this()

std::string expr2javat::convert_java_this ( )

protected

Definition at line 316 of file expr2java.cpp.

◆ convert_rec()

std::string expr2javat::convert_rec	(	const typet &	src,
		const c_qualifierst &	qualifiers,
		const std::string &	declarator
	)

overrideprotectedvirtual

Reimplemented from expr2ct.

Definition at line 243 of file expr2java.cpp.

◆ convert_struct()

std::string expr2javat::convert_struct	(	const exprt &	src,
		unsigned &	precedence
	)

overrideprotectedvirtual

Reimplemented from expr2ct.

Definition at line 104 of file expr2java.cpp.

◆ convert_with_precedence()

std::string expr2javat::convert_with_precedence	(	const exprt &	src,
		unsigned &	precedence
	)

overrideprotectedvirtual

Reimplemented from expr2ct.

Definition at line 377 of file expr2java.cpp.

Member Data Documentation

◆ char_representation_length

const std::size_t expr2javat::char_representation_length =8

protected

Definition at line 50 of file expr2java.h.

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

/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/expr2java.h
/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/expr2java.cpp

Public Member Functions

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ expr2javat()

Member Function Documentation

◆ convert() [1/2]

◆ convert() [2/2]

◆ convert_code()

◆ convert_code_function_call()

◆ convert_code_java_delete()

◆ convert_code_java_new()

◆ convert_constant()

◆ convert_java_instanceof()

◆ convert_java_new()

◆ convert_java_this()

◆ convert_rec()

◆ convert_struct()

◆ convert_with_precedence()

Member Data Documentation

◆ char_representation_length