cprover
expr2ct Class Reference

#include <expr2c_class.h>

Inheritance diagram for expr2ct:
[legend]
Collaboration diagram for expr2ct:
[legend]

Public Member Functions

 expr2ct (const namespacet &_ns)
 
virtual ~expr2ct ()
 
virtual std::string convert (const typet &src)
 
virtual std::string convert (const exprt &src)
 
void get_shorthands (const exprt &expr)
 

Protected Member Functions

virtual std::string convert_rec (const typet &src, const c_qualifierst &qualifiers, const std::string &declarator)
 
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 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_pointer_object_has_type (const exprt &src, unsigned precedence)
 
std::string convert_array_of (const exprt &src, unsigned precedence)
 
std::string convert_trinary (const exprt &src, const std::string &symbol1, const std::string &symbol2, unsigned precedence)
 
std::string convert_overflow (const exprt &src, unsigned &precedence)
 
std::string convert_quantifier (const exprt &src, const std::string &symbol, unsigned precedence)
 
std::string convert_with (const exprt &src, unsigned precedence)
 
std::string convert_update (const exprt &src, unsigned precedence)
 
std::string convert_member_designator (const exprt &src)
 
std::string convert_index_designator (const exprt &src)
 
std::string convert_index (const exprt &src, unsigned precedence)
 
std::string convert_byte_extract (const exprt &src, unsigned precedence)
 
std::string convert_byte_update (const exprt &src, unsigned precedence)
 
std::string convert_extractbit (const exprt &src, unsigned precedence)
 
std::string convert_extractbits (const exprt &src, unsigned precedence)
 
std::string convert_unary (const exprt &src, const std::string &symbol, unsigned precedence)
 
std::string convert_unary_post (const exprt &src, const std::string &symbol, unsigned precedence)
 
std::string convert_function (const exprt &src, const std::string &symbol, unsigned precedence)
 
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)
 
virtual std::string convert_code (const codet &src, unsigned indent)
 
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_assign (const code_assignt &src, unsigned indent)
 
std::string convert_code_free (const codet &src, unsigned indent)
 
std::string convert_code_init (const codet &src, 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 (const codet &src, unsigned indent)
 
std::string convert_code_switch (const codet &src, unsigned indent)
 
std::string convert_code_continue (const codet &src, unsigned indent)
 
std::string convert_code_decl (const codet &src, 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)
 
virtual std::string convert_with_precedence (const exprt &src, unsigned &precedence)
 
std::string convert_function_application (const function_application_exprt &src, unsigned &precedence)
 
std::string convert_side_effect_expr_function_call (const side_effect_expr_function_callt &src, unsigned &precedence)
 
std::string convert_malloc (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, unsigned &precedence)
 
std::string convert_predicate_symbol (const exprt &src, unsigned &precedence)
 
std::string convert_predicate_next_symbol (const exprt &src, unsigned &precedence)
 
std::string convert_predicate_passive_symbol (const exprt &src, unsigned &precedence)
 
std::string convert_nondet_symbol (const exprt &src, unsigned &precedence)
 
std::string convert_quantified_symbol (const exprt &src, unsigned &precedence)
 
std::string convert_nondet_bool (const exprt &src, unsigned &precedence)
 
std::string convert_object_descriptor (const exprt &src, unsigned &precedence)
 
std::string convert_literal (const exprt &src, unsigned &precedence)
 
virtual std::string convert_constant (const constant_exprt &src, unsigned &precedence)
 
virtual std::string convert_constant_bool (bool boolean_value)
 To get the C-like representation of a given boolean value. More...
 
std::string convert_norep (const exprt &src, unsigned &precedence)
 
virtual std::string convert_struct (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, unsigned &precedence)
 
std::string convert_array_list (const exprt &src, unsigned &precedence)
 
std::string convert_initializer_list (const exprt &src, unsigned &precedence)
 
std::string convert_designated_initializer (const exprt &src, unsigned &precedence)
 
std::string convert_concatenation (const exprt &src, unsigned &precedence)
 
std::string convert_sizeof (const exprt &src, 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...
 

Static Protected Member Functions

static std::string indent_str (unsigned indent)
 

Protected Attributes

const namespacetns
 
std::unordered_map< irep_idt, std::unordered_set< irep_idt, irep_id_hash >, irep_id_hashns_collision
 
std::unordered_map< irep_idt, irep_idt, irep_id_hashshorthands
 
unsigned sizeof_nesting
 

Detailed Description

Definition at line 23 of file expr2c_class.h.

Constructor & Destructor Documentation

§ expr2ct()

expr2ct::expr2ct ( const namespacet _ns)
inlineexplicit

Definition at line 26 of file expr2c_class.h.

§ ~expr2ct()

virtual expr2ct::~expr2ct ( )
inlinevirtual

Definition at line 27 of file expr2c_class.h.

References convert(), and get_shorthands().

Member Function Documentation

§ convert() [1/2]

std::string expr2ct::convert ( const typet src)
virtual

Definition at line 158 of file expr2c.cpp.

References convert_rec().

Referenced by convert_array(), convert_array_list(), convert_array_member_value(), convert_array_of(), convert_array_type(), convert_byte_extract(), convert_byte_update(), convert_code_asm(), convert_code_assert(), convert_code_assume(), expr2cppt::convert_code_cpp_delete(), convert_code_dead(), convert_code_decl(), convert_code_dowhile(), convert_code_expression(), convert_code_for(), convert_code_free(), convert_code_ifthenelse(), expr2javat::convert_code_java_delete(), convert_code_lock(), convert_code_return(), convert_code_switch(), convert_code_switch_case(), convert_code_unlock(), convert_code_while(), convert_constant(), expr2cppt::convert_cpp_new(), convert_designated_initializer(), expr2cppt::convert_extractbit(), expr2cppt::convert_extractbits(), convert_Hoare(), convert_index(), convert_index_designator(), convert_initializer_list(), expr2javat::convert_java_instanceof(), expr2javat::convert_java_new(), convert_malloc(), convert_nondet(), convert_object_descriptor(), convert_overflow(), convert_pointer_arithmetic(), convert_pointer_difference(), convert_pointer_object_has_type(), convert_prob_coin(), convert_prob_uniform(), convert_quantifier(), convert_rec(), expr2javat::convert_rec(), expr2cppt::convert_rec(), convert_sizeof(), expr2javat::convert_struct(), expr2cppt::convert_struct(), convert_struct(), convert_struct_member_value(), convert_symbol(), convert_typecast(), convert_union(), convert_update(), convert_vector(), convert_with_precedence(), expr2c(), expr2cpp(), expr2java(), expr2jsil(), type2c(), type2cpp(), type2java(), type2jsil(), and ~expr2ct().

§ convert() [2/2]

std::string expr2ct::convert ( const exprt src)
virtual

Definition at line 3868 of file expr2c.cpp.

References convert_with_precedence().

§ convert_array()

std::string expr2ct::convert_array ( const exprt src,
unsigned &  precedence 
)
protected

§ convert_array_list()

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

Definition at line 2206 of file expr2c.cpp.

References convert(), convert_norep(), forall_operands, and exprt::operands().

Referenced by convert_with_precedence().

§ convert_array_member_value()

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

Definition at line 1560 of file expr2c.cpp.

References convert(), convert_norep(), exprt::op0(), and exprt::operands().

Referenced by convert_with_precedence().

§ convert_array_of()

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

Definition at line 1279 of file expr2c.cpp.

References convert(), convert_norep(), exprt::op0(), and exprt::operands().

Referenced by convert_with_precedence().

§ convert_array_type() [1/2]

std::string expr2ct::convert_array_type ( const typet src,
const c_qualifierst qualifiers,
const std::string &  declarator_str 
)
protectedvirtual

To generate a C-like type declaration of an array.

Includes the size of the array in the []

Parameters
srcThe array type to convert qualifier declarator_str
Returns
A C-like type declaration of an array

Definition at line 725 of file expr2c.cpp.

Referenced by convert_rec().

§ convert_array_type() [2/2]

std::string expr2ct::convert_array_type ( const typet src,
const c_qualifierst qualifiers,
const std::string &  declarator_str,
bool  inc_size_if_possible 
)
protected

To generate a C-like type declaration of an array.

Optionally can include or exclude the size of the array in the []

Parameters
srcThe array type to convert qualifier declarator_str
inc_size_if_possibleShould the generated string include the size of the array (if it is known).
Returns
A C-like type declaration of an array

Definition at line 741 of file expr2c.cpp.

References convert(), convert_rec(), typet::subtype(), and to_array_type().

§ convert_binary()

std::string expr2ct::convert_binary ( const exprt src,
const std::string &  symbol,
unsigned  precedence,
bool  full_parentheses 
)
protected

§ convert_byte_extract()

std::string expr2ct::convert_byte_extract ( const exprt src,
unsigned  precedence 
)
protected

§ convert_byte_update()

std::string expr2ct::convert_byte_update ( const exprt src,
unsigned  precedence 
)
protected

§ convert_code() [1/2]

§ convert_code() [2/2]

§ convert_code_array_copy()

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

Definition at line 3152 of file expr2c.cpp.

References convert_with_precedence(), forall_operands, indent_str(), and exprt::operands().

Referenced by convert_code().

§ convert_code_array_replace()

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

Definition at line 3174 of file expr2c.cpp.

References convert_with_precedence(), forall_operands, indent_str(), and exprt::operands().

Referenced by convert_code().

§ convert_code_array_set()

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

Definition at line 3130 of file expr2c.cpp.

References convert_with_precedence(), forall_operands, indent_str(), and exprt::operands().

Referenced by convert_code().

§ convert_code_asm()

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

§ convert_code_assert()

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

Definition at line 3195 of file expr2c.cpp.

References convert(), convert_norep(), indent_str(), exprt::op0(), and exprt::operands().

Referenced by convert_code().

§ convert_code_assign()

std::string expr2ct::convert_code_assign ( const code_assignt src,
unsigned  indent 
)
protected

Definition at line 2928 of file expr2c.cpp.

References convert_binary(), and indent_str().

Referenced by convert_code().

§ convert_code_assume()

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

Definition at line 3208 of file expr2c.cpp.

References convert(), convert_norep(), indent_str(), exprt::op0(), and exprt::operands().

Referenced by convert_code().

§ convert_code_block()

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

Definition at line 2742 of file expr2c.cpp.

References convert_code(), forall_operands, indent_str(), and to_code().

Referenced by convert_code().

§ convert_code_break()

std::string expr2ct::convert_code_break ( const codet src,
unsigned  indent 
)
protected

Definition at line 2586 of file expr2c.cpp.

References indent_str().

Referenced by convert_code().

§ convert_code_continue()

std::string expr2ct::convert_code_continue ( const codet src,
unsigned  indent 
)
protected

Definition at line 2640 of file expr2c.cpp.

References indent_str().

Referenced by convert_code().

§ convert_code_dead()

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

Definition at line 2691 of file expr2c.cpp.

References convert(), convert_norep(), exprt::op0(), and exprt::operands().

Referenced by convert_code().

§ convert_code_decl()

§ convert_code_decl_block()

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

Definition at line 2765 of file expr2c.cpp.

References convert_code(), forall_operands, and to_code().

Referenced by convert_code().

§ convert_code_dowhile()

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

§ convert_code_expression()

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

Definition at line 2780 of file expr2c.cpp.

References convert(), convert_norep(), indent_str(), exprt::op0(), and exprt::operands().

Referenced by convert_code().

§ convert_code_fence()

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

Definition at line 3057 of file expr2c.cpp.

References dstringt::empty(), irept::get_bool(), id2string(), and indent_str().

Referenced by convert_code().

§ convert_code_for()

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

§ convert_code_free()

std::string expr2ct::convert_code_free ( const codet src,
unsigned  indent 
)
protected

Definition at line 2939 of file expr2c.cpp.

References convert(), convert_norep(), indent_str(), exprt::op0(), and exprt::operands().

Referenced by convert_code().

§ convert_code_function_call()

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

§ convert_code_goto()

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

Definition at line 2574 of file expr2c.cpp.

References clean_identifier(), irept::get(), and indent_str().

Referenced by convert_code().

§ convert_code_ifthenelse()

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

§ convert_code_init()

std::string expr2ct::convert_code_init ( const codet src,
unsigned  indent 
)
protected

Definition at line 2952 of file expr2c.cpp.

References convert_binary(), and indent_str().

Referenced by convert_code().

§ convert_code_input()

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

Definition at line 3087 of file expr2c.cpp.

References convert_with_precedence(), forall_operands, indent_str(), and exprt::operands().

Referenced by convert_code().

§ convert_code_label()

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

§ convert_code_lock()

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

Definition at line 2961 of file expr2c.cpp.

References convert(), convert_norep(), indent_str(), exprt::op0(), and exprt::operands().

Referenced by convert_code().

§ convert_code_output()

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

Definition at line 3109 of file expr2c.cpp.

References convert_with_precedence(), forall_operands, indent_str(), and exprt::operands().

Referenced by convert_code().

§ convert_code_printf()

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

Definition at line 3035 of file expr2c.cpp.

References convert_with_precedence(), forall_operands, indent_str(), and exprt::operands().

Referenced by convert_code().

§ convert_code_return()

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

Definition at line 2552 of file expr2c.cpp.

References convert(), convert_norep(), indent_str(), exprt::op0(), exprt::operands(), and to_code_return().

Referenced by convert_code().

§ convert_code_switch()

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

§ convert_code_switch_case()

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

§ convert_code_unlock()

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

Definition at line 2974 of file expr2c.cpp.

References convert(), convert_norep(), indent_str(), exprt::op0(), and exprt::operands().

Referenced by convert_code().

§ convert_code_while()

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

§ convert_comma()

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

§ convert_complex()

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

§ convert_concatenation()

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

§ convert_cond()

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

§ convert_constant()

§ convert_constant_bool()

std::string expr2ct::convert_constant_bool ( bool  boolean_value)
protectedvirtual

To get the C-like representation of a given boolean value.

Parameters
boolean_valueThe value of the constant bool expression
Returns
Returns a C-like representation of the boolean value, e.g. TRUE or FALSE.

Definition at line 1935 of file expr2c.cpp.

Referenced by convert_constant().

§ convert_designated_initializer()

std::string expr2ct::convert_designated_initializer ( const exprt src,
unsigned &  precedence 
)
protected

Definition at line 2268 of file expr2c.cpp.

References convert(), convert_norep(), exprt::op0(), and exprt::operands().

Referenced by convert_with_precedence().

§ convert_extractbit()

std::string expr2ct::convert_extractbit ( const exprt src,
unsigned  precedence 
)
protected

§ convert_extractbits()

std::string expr2ct::convert_extractbits ( const exprt src,
unsigned  precedence 
)
protected

§ convert_function()

std::string expr2ct::convert_function ( const exprt src,
const std::string &  symbol,
unsigned  precedence 
)
protected

§ convert_function_application()

std::string expr2ct::convert_function_application ( const function_application_exprt src,
unsigned &  precedence 
)
protected

§ convert_Hoare()

std::string expr2ct::convert_Hoare ( const exprt src)
protected

§ convert_index()

std::string expr2ct::convert_index ( const exprt src,
unsigned  precedence 
)
protected

§ convert_index_designator()

std::string expr2ct::convert_index_designator ( const exprt src)
protected

Definition at line 1474 of file expr2c.cpp.

References convert(), convert_norep(), exprt::op0(), and exprt::operands().

Referenced by convert_with_precedence().

§ convert_initializer_list()

std::string expr2ct::convert_initializer_list ( const exprt src,
unsigned &  precedence 
)
protected

Definition at line 2240 of file expr2c.cpp.

References convert(), forall_operands, irept::id(), and exprt::operands().

Referenced by convert_with_precedence().

§ convert_literal()

std::string expr2ct::convert_literal ( const exprt src,
unsigned &  precedence 
)
protected

Definition at line 1163 of file expr2c.cpp.

References irept::get_string().

Referenced by convert_with_precedence().

§ convert_malloc()

std::string expr2ct::convert_malloc ( const exprt src,
unsigned &  precedence 
)
protected

§ convert_member()

§ convert_member_designator()

std::string expr2ct::convert_member_designator ( const exprt src)
protected

Definition at line 1464 of file expr2c.cpp.

References convert_norep(), irept::get_string(), and exprt::operands().

Referenced by convert_with_precedence().

§ convert_nondet()

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

Definition at line 1132 of file expr2c.cpp.

References convert(), convert_norep(), exprt::operands(), and exprt::type().

Referenced by convert_with_precedence().

§ convert_nondet_bool()

std::string expr2ct::convert_nondet_bool ( const exprt src,
unsigned &  precedence 
)
protected

Definition at line 1673 of file expr2c.cpp.

Referenced by convert_with_precedence().

§ convert_nondet_symbol()

std::string expr2ct::convert_nondet_symbol ( const exprt src,
unsigned &  precedence 
)
protected

Definition at line 1633 of file expr2c.cpp.

References irept::get_string().

Referenced by convert_with_precedence().

§ convert_norep()

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

Definition at line 1580 of file expr2c.cpp.

References lispexprt::expr2string(), irep2lisp(), and MetaString().

Referenced by convert_array_list(), convert_array_member_value(), convert_array_of(), convert_binary(), convert_byte_extract(), convert_byte_update(), convert_code(), convert_code_assert(), convert_code_assume(), expr2cppt::convert_code_cpp_delete(), convert_code_dead(), convert_code_decl(), convert_code_dowhile(), convert_code_expression(), convert_code_for(), convert_code_free(), expr2javat::convert_code_function_call(), convert_code_function_call(), convert_code_ifthenelse(), expr2javat::convert_code_java_delete(), convert_code_lock(), convert_code_return(), convert_code_switch(), convert_code_unlock(), convert_code_while(), convert_comma(), convert_cond(), convert_constant(), convert_designated_initializer(), convert_extractbit(), convert_extractbits(), convert_Hoare(), convert_index(), convert_index_designator(), expr2javat::convert_java_instanceof(), convert_malloc(), convert_member(), convert_member_designator(), convert_nondet(), convert_object_descriptor(), convert_pointer_arithmetic(), convert_pointer_difference(), convert_pointer_object_has_type(), convert_prob_coin(), convert_prob_uniform(), convert_quantifier(), convert_sizeof(), convert_statement_expression(), expr2javat::convert_struct(), expr2cppt::convert_struct(), convert_struct(), convert_struct_member_value(), convert_trinary(), convert_typecast(), convert_unary(), convert_unary_post(), convert_union(), convert_update(), convert_vector(), convert_with(), and convert_with_precedence().

§ convert_object_descriptor()

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

§ convert_overflow()

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

§ convert_pointer_arithmetic()

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

§ convert_pointer_difference()

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

§ convert_pointer_object_has_type()

std::string expr2ct::convert_pointer_object_has_type ( const exprt src,
unsigned  precedence 
)
protected

§ convert_predicate_next_symbol()

std::string expr2ct::convert_predicate_next_symbol ( const exprt src,
unsigned &  precedence 
)
protected

Definition at line 1649 of file expr2c.cpp.

References irept::get_string().

Referenced by convert_with_precedence().

§ convert_predicate_passive_symbol()

std::string expr2ct::convert_predicate_passive_symbol ( const exprt src,
unsigned &  precedence 
)
protected

Definition at line 1657 of file expr2c.cpp.

References irept::get_string().

Referenced by convert_with_precedence().

§ convert_predicate_symbol()

std::string expr2ct::convert_predicate_symbol ( const exprt src,
unsigned &  precedence 
)
protected

Definition at line 1641 of file expr2c.cpp.

References irept::get_string().

Referenced by convert_with_precedence().

§ convert_prob_coin()

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

Definition at line 1153 of file expr2c.cpp.

References convert(), convert_norep(), exprt::op0(), and exprt::operands().

Referenced by convert_with_precedence().

§ convert_prob_uniform()

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

Definition at line 1170 of file expr2c.cpp.

References convert(), convert_norep(), exprt::op0(), exprt::operands(), and exprt::type().

Referenced by convert_with_precedence().

§ convert_quantified_symbol()

std::string expr2ct::convert_quantified_symbol ( const exprt src,
unsigned &  precedence 
)
protected

Definition at line 1665 of file expr2c.cpp.

References irept::get_string().

Referenced by convert_with_precedence().

§ convert_quantifier()

std::string expr2ct::convert_quantifier ( const exprt src,
const std::string &  symbol,
unsigned  precedence 
)
protected

§ convert_rec()

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

Reimplemented in expr2cppt, and expr2javat.

Definition at line 163 of file expr2c.cpp.

References configt::ansi_c, c_qualifierst::as_string(), symbolt::base_name, c_type_as_string(), configt::ansi_ct::char_is_unsigned, configt::ansi_ct::char_width, struct_union_typet::components(), config, convert(), convert_array_type(), convert_struct_type(), configt::ansi_ct::double_width, dstringt::empty(), lispexprt::expr2string(), irept::find(), namespace_baset::follow(), namespace_baset::follow_tag(), irept::get(), fixedbv_typet::get_fraction_bits(), irept::get_string(), struct_union_typet::get_tag(), bitvector_typet::get_width(), code_typet::has_ellipsis(), irept::id(), id2string(), irept::id_string(), configt::ansi_ct::int_width, integer2string(), irep2lisp(), irept::is_nil(), c_qualifierst::is_noreturn, irept::is_not_nil(), is_signed(), configt::ansi_ct::long_double_width, configt::ansi_ct::long_int_width, configt::ansi_ct::long_long_int_width, namespacet::lookup(), c_enum_typet::members(), MetaString(), ns, code_typet::parameters(), c_qualifierst::read(), code_typet::return_type(), configt::ansi_ct::short_int_width, configt::ansi_ct::single_width, vector_typet::size(), sizeof_nesting, string2integer(), typet::subtype(), to_c_bit_field_type(), to_c_enum_tag_type(), to_c_enum_type(), to_code_type(), to_fixedbv_type(), to_floatbv_type(), to_integer(), to_struct_tag_type(), to_struct_type(), to_union_tag_type(), to_union_type(), to_vector_type(), and configt::ansi_ct::use_fixed_for_float.

Referenced by convert(), convert_array_type(), convert_code_decl(), expr2javat::convert_rec(), expr2cppt::convert_rec(), and convert_struct_type().

§ convert_side_effect_expr_function_call()

std::string expr2ct::convert_side_effect_expr_function_call ( const side_effect_expr_function_callt src,
unsigned &  precedence 
)
protected

§ convert_sizeof()

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

Definition at line 3349 of file expr2c.cpp.

References convert(), convert_norep(), irept::find(), and exprt::has_operands().

Referenced by convert_with_precedence().

§ convert_statement_expression()

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

§ convert_struct() [1/2]

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

Reimplemented in expr2cppt, and expr2javat.

Definition at line 1944 of file expr2c.cpp.

Referenced by convert_with_precedence().

§ convert_struct() [2/2]

std::string expr2ct::convert_struct ( const exprt src,
unsigned &  precedence,
bool  include_padding_components 
)
protected

To generate a C-like string representing a struct.

Can optionally include the padding parameters.

Parameters
srcThe struct declaration expression precedence
include_padding_componentsShould the generated C code include the padding members added to structs for GOTOs benefit
Returns
A string representation of the struct expression

Definition at line 1958 of file expr2c.cpp.

References struct_union_typet::components(), convert(), convert_norep(), namespace_baset::follow(), irept::id(), ns, exprt::operands(), to_struct_type(), and exprt::type().

§ convert_struct_member_value()

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

§ convert_struct_type() [1/2]

std::string expr2ct::convert_struct_type ( const typet src,
const std::string &  qualifiers_str,
const std::string &  declarator_str 
)
protectedvirtual

To generate C-like string for defining the given struct.

Parameters
srcthe struct type being converted
qualifiersany qualifiers on the type
declaratorthe declarator on the type
Returns
Returns a type declaration for a struct, containing the body of the struct and in that body the padding parameters.

Definition at line 652 of file expr2c.cpp.

Referenced by convert_rec().

§ convert_struct_type() [2/2]

std::string expr2ct::convert_struct_type ( const typet src,
const std::string &  qualifiers,
const std::string &  declarator,
bool  inc_struct_body,
bool  inc_padding_components 
)
protected

To generate C-like string for declaring (or defining) the given struct.

Parameters
srcthe struct type being converted
qualifiersany qualifiers on the type
declaratorthe declarator on the type
inc_struct_bodywhen generating the code, should we include a complete definition of the struct
inc_padding_componentsshould the padding parameters be included Note this only makes sense if inc_struct_body
Returns
Returns a type declaration for a struct, optionally containing the body of the struct (and in that body, optionally the padding parameters).

Definition at line 670 of file expr2c.cpp.

References struct_union_typet::components(), convert_rec(), struct_union_typet::get_tag(), id2string(), and to_struct_type().

§ convert_symbol()

std::string expr2ct::convert_symbol ( const exprt src,
unsigned &  precedence 
)
protectedvirtual

§ convert_trinary()

std::string expr2ct::convert_trinary ( const exprt src,
const std::string &  symbol1,
const std::string &  symbol2,
unsigned  precedence 
)
protected

Definition at line 795 of file expr2c.cpp.

References convert_norep(), convert_with_precedence(), and exprt::operands().

Referenced by convert_with_precedence().

§ convert_typecast()

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

§ convert_unary()

std::string expr2ct::convert_unary ( const exprt src,
const std::string &  symbol,
unsigned  precedence 
)
protected

§ convert_unary_post()

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

§ convert_union()

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

§ convert_update()

std::string expr2ct::convert_update ( const exprt src,
unsigned  precedence 
)
protected

§ convert_vector()

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

§ convert_with()

§ convert_with_precedence()

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

Reimplemented in expr2cppt, and expr2javat.

Definition at line 3363 of file expr2c.cpp.

References configt::ansi_c, config, convert(), convert_array(), convert_array_list(), convert_array_member_value(), convert_array_of(), convert_binary(), convert_byte_extract(), convert_byte_update(), convert_code(), convert_comma(), convert_complex(), convert_cond(), convert_constant(), convert_designated_initializer(), convert_extractbit(), convert_extractbits(), convert_function(), convert_function_application(), convert_Hoare(), convert_index(), convert_index_designator(), convert_initializer_list(), convert_literal(), convert_malloc(), convert_member(), convert_member_designator(), convert_nondet(), convert_nondet_bool(), convert_nondet_symbol(), convert_norep(), convert_object_descriptor(), convert_overflow(), convert_pointer_arithmetic(), convert_pointer_difference(), convert_pointer_object_has_type(), convert_predicate_next_symbol(), convert_predicate_passive_symbol(), convert_predicate_symbol(), convert_prob_coin(), convert_prob_uniform(), convert_quantified_symbol(), convert_quantifier(), convert_side_effect_expr_function_call(), convert_sizeof(), convert_statement_expression(), convert_struct(), convert_struct_member_value(), convert_symbol(), convert_trinary(), convert_typecast(), convert_unary(), convert_unary_post(), convert_union(), convert_update(), convert_vector(), convert_with(), namespace_baset::follow(), irept::get(), irept::get_string(), has_prefix(), irept::id(), id2string(), irept::id_string(), integer2string(), exprt::is_zero(), MetaString(), configt::ansi_ct::mode, ns, exprt::op0(), exprt::op1(), exprt::operands(), pointer_offset_bits(), typet::subtype(), to_code(), to_constant_expr(), to_function_application_expr(), to_index_expr(), to_member_expr(), to_side_effect_expr_function_call(), to_typecast_expr(), exprt::type(), and configt::ansi_ct::VISUAL_STUDIO.

Referenced by convert(), convert_binary(), convert_byte_extract(), convert_byte_update(), convert_code_array_copy(), convert_code_array_replace(), convert_code_array_set(), convert_code_function_call(), convert_code_input(), convert_code_output(), convert_code_printf(), convert_comma(), convert_complex(), convert_cond(), convert_constant(), convert_extractbit(), convert_extractbits(), convert_function(), convert_function_application(), convert_index(), convert_malloc(), convert_member(), convert_overflow(), convert_pointer_arithmetic(), convert_pointer_difference(), convert_pointer_object_has_type(), convert_quantifier(), convert_side_effect_expr_function_call(), convert_trinary(), convert_typecast(), convert_unary(), convert_unary_post(), convert_update(), convert_with(), expr2javat::convert_with_precedence(), and expr2cppt::convert_with_precedence().

§ get_shorthands()

§ id_shorthand()

irep_idt expr2ct::id_shorthand ( const irep_idt identifier) const
protected

§ indent_str()

Member Data Documentation

§ ns

§ ns_collision

std::unordered_map<irep_idt, std::unordered_set<irep_idt, irep_id_hash>, irep_id_hash> expr2ct::ns_collision
protected

Definition at line 69 of file expr2c_class.h.

Referenced by get_shorthands().

§ shorthands

std::unordered_map<irep_idt, irep_idt, irep_id_hash> expr2ct::shorthands
protected

Definition at line 70 of file expr2c_class.h.

Referenced by convert_symbol(), and get_shorthands().

§ sizeof_nesting

unsigned expr2ct::sizeof_nesting
protected

Definition at line 72 of file expr2c_class.h.

Referenced by convert_constant(), convert_rec(), and convert_symbol().


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