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 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 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 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_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_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_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, 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 nondet_symbol_exprt &, 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_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...
 

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 > > ns_collision
 
std::unordered_map< irep_idt, irep_idtshorthands
 
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.

Member Function Documentation

◆ convert() [1/2]

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

◆ convert() [2/2]

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

Reimplemented in expr2javat.

Definition at line 3961 of file expr2c.cpp.

References convert_with_precedence().

◆ convert_allocate()

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

◆ 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 2288 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 1642 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 1361 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 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 732 of file expr2c.cpp.

Referenced by convert_rec().

◆ convert_array_type() [2/2]

std::string expr2ct::convert_array_type ( const typet src,
const 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 748 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 3245 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 3267 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 3223 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 3288 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 3021 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 3301 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 2829 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 2668 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 2722 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 2778 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 2852 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 2867 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 3150 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 3032 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 2656 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 3045 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 3180 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 3054 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 3202 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 3128 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 2634 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 3067 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 2017 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 2350 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 1556 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 2322 of file expr2c.cpp.

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

Referenced by convert_with_precedence().

◆ convert_let()

std::string expr2ct::convert_let ( const let_exprt src,
unsigned  precedence 
)
protected

◆ convert_literal()

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

Definition at line 1245 of file expr2c.cpp.

References irept::get_string().

Referenced by convert_with_precedence().

◆ convert_member()

◆ convert_member_designator()

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

Definition at line 1546 of file expr2c.cpp.

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

Referenced by convert_with_precedence().

◆ convert_multi_ary()

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

◆ convert_nondet()

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

Definition at line 1214 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 1755 of file expr2c.cpp.

Referenced by convert_with_precedence().

◆ convert_nondet_symbol()

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

Definition at line 1715 of file expr2c.cpp.

References nondet_symbol_exprt::get_identifier(), and id2string().

Referenced by convert_with_precedence().

◆ convert_norep()

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

Definition at line 1662 of file expr2c.cpp.

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

Referenced by convert_allocate(), 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_let(), convert_member(), convert_member_designator(), convert_multi_ary(), 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 1731 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 1739 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 1723 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 1235 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 1252 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 1747 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 qualifierst qualifiers,
const std::string &  declarator 
)
protectedvirtual

Reimplemented in expr2cppt, and expr2javat.

Definition at line 166 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, qualifierst::clone(), 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_string(), to_struct_tag_type(), to_struct_type(), to_symbol_type(), to_union_tag_type(), to_union_type(), and to_vector_type().

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 3442 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 2026 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 2040 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 659 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 677 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

◆ 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 3456 of file expr2c.cpp.

References configt::ansi_c, config, convert(), convert_allocate(), 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_let(), convert_literal(), convert_member(), convert_member_designator(), convert_multi_ary(), 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_let_expr(), to_member_expr(), to_nondet_symbol_expr(), to_side_effect_expr_function_call(), to_typecast_expr(), exprt::type(), and configt::ansi_ct::VISUAL_STUDIO.

Referenced by convert(), convert_allocate(), 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_let(), convert_member(), convert_multi_ary(), 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> > expr2ct::ns_collision
protected

Definition at line 67 of file expr2c_class.h.

Referenced by get_shorthands().

◆ shorthands

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

Definition at line 68 of file expr2c_class.h.

Referenced by convert_symbol(), and get_shorthands().

◆ sizeof_nesting

unsigned expr2ct::sizeof_nesting
protected

Definition at line 70 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: