cprover
java_string_library_preprocesst Class Reference

#include <java_string_library_preprocess.h>

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

Public Member Functions

 java_string_library_preprocesst ()
 
void initialize_known_type_table ()
 
void initialize_conversion_table ()
 fill maps with correspondence from java method names to conversion functions More...
 
void initialize_refined_string_type ()
 
bool implements_function (const irep_idt &function_id) const
 
void get_all_function_names (std::unordered_set< irep_idt > &methods) const
 
exprt code_for_function (const symbolt &symbol, symbol_table_baset &symbol_table)
 Should be called to provide code for string functions that are used in the code but for which no implementation is provided. More...
 
codet replace_character_call (code_function_callt call)
 
std::vector< irep_idtget_string_type_base_classes (const irep_idt &class_name)
 Gets the base classes for known String and String-related types, or returns an empty list for other types. More...
 
void add_string_type (const irep_idt &class_name, symbol_tablet &symbol_table)
 Add to the symbol table type declaration for a String-like Java class. More...
 
bool is_known_string_type (irep_idt class_name)
 Check whether a class name is known as a string type. More...
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to mstream using output_generator if the configured verbosity is at least as high as that of mstream. More...
 

Static Public Member Functions

static bool implements_java_char_sequence_pointer (const typet &type)
 
static bool implements_java_char_sequence (const typet &type)
 
- 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 mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Private Types

typedef std::function< codet(const code_typet &, const source_locationt &, const irep_idt &, symbol_table_baset &)> conversion_functiont
 
typedef std::unordered_map< irep_idt, irep_idtid_mapt
 

Private Member Functions

 java_string_library_preprocesst (const java_string_library_preprocesst &)=delete
 
codet make_equals_function_code (const code_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
 Used to provide code for the Java String.equals(Object) function. More...
 
codet make_float_to_string_code (const code_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
 Provide code for the String.valueOf(F) function. More...
 
codet make_string_to_char_array_code (const code_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_tablet &symbol_table)
 
codet make_string_format_code (const code_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
 Used to provide code for the Java String.format function. More...
 
codet make_copy_string_code (const code_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
 Generates code for a function which copies a string object to a new string object. More...
 
codet make_copy_constructor_code (const code_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
 Generates code for a constructor of a string object from another string object. More...
 
codet make_string_length_code (const code_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
 Generates code for the String.length method. More...
 
codet make_object_get_class_code (const code_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
 Used to provide our own implementation of the java.lang.Object.getClass() function. More...
 
exprt::operandst process_parameters (const code_typet::parameterst &params, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &init_code)
 calls string_refine_preprocesst::process_operands with a list of parameters. More...
 
refined_string_exprt convert_exprt_to_string_exprt (const exprt &deref, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &init_code)
 Creates a string_exprt from the input exprt representing a char sequence. More...
 
exprt::operandst process_operands (const exprt::operandst &operands, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &init_code)
 for each expression that is of a type implementing strings, we declare a new cprover_string whose contents is deduced from the expression and replace the expression by this cprover_string in the output list; in the other case the expression is kept as is for the output list. More...
 
exprt::operandst process_equals_function_operands (const exprt::operandst &operands, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &init_code)
 Converts the operands of the equals function to string expressions and outputs these conversions. More...
 
refined_string_exprt replace_char_array (const exprt &array_pointer, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
 we declare a new cprover_string whose contents is deduced from the char array. More...
 
symbol_exprt fresh_string (const typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
 add a symbol with static lifetime and name containing cprover_string and given type More...
 
symbol_exprt fresh_array (const typet &type, const source_locationt &loc, symbol_tablet &symbol_table)
 add a symbol in the table with static lifetime and name containing cprover_string_array and given type More...
 
refined_string_exprt decl_string_expr (const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
 Add declaration of a refined string expr whose content and length are fresh symbols. More...
 
refined_string_exprt make_nondet_string_expr (const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)
 add symbols with prefix cprover_string_length and cprover_string_data and construct a string_expr from them. More...
 
exprt allocate_fresh_string (const typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)
 declare a new String and allocate it More...
 
exprt allocate_fresh_array (const typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_tablet &symbol_table, code_blockt &code)
 declare a new character array and allocate it More...
 
codet code_return_function_application (const irep_idt &function_name, const exprt::operandst &arguments, const typet &type, symbol_table_baset &symbol_table)
 return the result of a function call More...
 
refined_string_exprt string_expr_of_function (const irep_idt &function_name, const exprt::operandst &arguments, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
 Create a refined_string_exprt str whose content and length are fresh symbols, calls the string primitive with name function_name. More...
 
codet code_assign_components_to_java_string (const exprt &lhs, const exprt &rhs_array, const exprt &rhs_length, const symbol_table_baset &symbol_table)
 Produce code for an assignment of a string expr to a Java string. More...
 
codet code_assign_string_expr_to_java_string (const exprt &lhs, const refined_string_exprt &rhs, const symbol_table_baset &symbol_table)
 Produce code for an assignemnt of a string expr to a Java string. More...
 
void code_assign_java_string_to_string_expr (const refined_string_exprt &lhs, const exprt &rhs, const source_locationt &loc, const symbol_table_baset &symbol_table, code_blockt &code)
 
refined_string_exprt string_literal_to_string_expr (const std::string &s, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
 Create a string expression whose value is given by a literal. More...
 
codet make_function_from_call (const irep_idt &function_name, const code_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
 Provide code for a function that calls a function from the solver and simply returns it. More...
 
codet make_init_function_from_call (const irep_idt &function_name, const code_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table, bool ignore_first_arg=true)
 Generate the goto code for string initialization. More...
 
codet make_assign_and_return_function_from_call (const irep_idt &function_name, const code_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
 Call a cprover internal function, assign the result to object this and return it. More...
 
codet make_assign_function_from_call (const irep_idt &function_name, const code_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
 Call a cprover internal function and assign the result to object this. More...
 
codet make_string_returning_function_from_call (const irep_idt &function_name, const code_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
 Provide code for a function that calls a function from the solver and return the string_expr result as a Java string. More...
 
exprt make_argument_for_format (const exprt &argv, int index, const struct_typet &structured_type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)
 Helper for format function. More...
 
exprt get_primitive_value_of_object (const exprt &object, irep_idt type_name, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
 Adds to the code an assignment of the form

type_name tmp_type_name
tmp_type_name = ((Classname*)arg_i)->value

and returns tmp_typename. More...

 
exprt get_object_at_index (const exprt &argv, int index)
 Helper for format function. More...
 
codet make_init_from_array_code (const code_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
 Used to provide code for constructor from a char array. More...
 

Static Private Member Functions

static bool java_type_matches_tag (const typet &type, const std::string &tag)
 
static bool is_java_string_pointer_type (const typet &type)
 
static bool is_java_string_type (const typet &type)
 
static bool is_java_string_builder_type (const typet &type)
 
static bool is_java_string_builder_pointer_type (const typet &type)
 
static bool is_java_string_buffer_type (const typet &type)
 
static bool is_java_string_buffer_pointer_type (const typet &type)
 
static bool is_java_char_sequence_type (const typet &type)
 
static bool is_java_char_sequence_pointer_type (const typet &type)
 
static bool is_java_char_array_type (const typet &type)
 
static bool is_java_char_array_pointer_type (const typet &type)
 

Private Attributes

character_refine_preprocesst character_preprocess
 
const typet char_type
 
const typet index_type
 
const refined_string_typet refined_string_type
 
std::unordered_map< irep_idt, conversion_functiontconversion_table
 
id_mapt cprover_equivalent_to_java_function
 
id_mapt cprover_equivalent_to_java_string_returning_function
 
id_mapt cprover_equivalent_to_java_constructor
 
id_mapt cprover_equivalent_to_java_assign_and_return_function
 
id_mapt cprover_equivalent_to_java_assign_function
 
const std::array< id_mapt *, 5 > id_maps
 
std::unordered_set< irep_idtstring_types
 

Friends

refined_string_exprt convert_exprt_to_string_exprt_unit_test (java_string_library_preprocesst &preprocess, const exprt &deref, const source_locationt &loc, symbol_tablet &symbol_table, code_blockt &init_code)
 

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
}
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Detailed Description

Definition at line 34 of file java_string_library_preprocess.h.

Member Typedef Documentation

◆ conversion_functiont

Definition at line 106 of file java_string_library_preprocess.h.

◆ id_mapt

typedef std::unordered_map<irep_idt, irep_idt> java_string_library_preprocesst::id_mapt
private

Definition at line 108 of file java_string_library_preprocess.h.

Constructor & Destructor Documentation

◆ java_string_library_preprocesst() [1/2]

java_string_library_preprocesst::java_string_library_preprocesst ( )
inline

Definition at line 37 of file java_string_library_preprocess.h.

◆ java_string_library_preprocesst() [2/2]

java_string_library_preprocesst::java_string_library_preprocesst ( const java_string_library_preprocesst )
privatedelete

Member Function Documentation

◆ add_string_type()

void java_string_library_preprocesst::add_string_type ( const irep_idt class_name,
symbol_tablet symbol_table 
)

Add to the symbol table type declaration for a String-like Java class.

Parameters
class_namea name for the class such as "java.lang.String"
symbol_tablesymbol table to which the class will be added

Definition at line 220 of file java_string_library_preprocess.cpp.

References class_typet::add_base(), symbolt::base_name, struct_union_typet::components(), get_string_type_base_classes(), id2string(), symbolt::is_type, java_char_type(), symbolt::mode, symbol_tablet::move(), symbolt::name, pointer_type(), symbolt::pretty_name, java_class_typet::set_access(), struct_union_typet::set_tag(), string_length_type(), and symbolt::type.

Referenced by java_bytecode_convert_classt::operator()().

◆ allocate_fresh_array()

exprt java_string_library_preprocesst::allocate_fresh_array ( const typet type,
const source_locationt loc,
const irep_idt function_id,
symbol_tablet symbol_table,
code_blockt code 
)
private

declare a new character array and allocate it

Parameters
typea type for string
loca location in the program
symbol_tablesymbol table
codecode block to which allocation instruction will be added
Returns
a new array

Definition at line 593 of file java_string_library_preprocess.cpp.

References code_blockt::add(), allocate_dynamic_object_with_decl(), fresh_array(), and loc.

◆ allocate_fresh_string()

exprt java_string_library_preprocesst::allocate_fresh_string ( const typet type,
const source_locationt loc,
const irep_idt function_id,
symbol_table_baset symbol_table,
code_blockt code 
)
private

declare a new String and allocate it

Parameters
typea type for string
loca location in the program
symbol_tablesymbol table
codecode block to which allocation instruction will be added
Returns
a new string

Definition at line 575 of file java_string_library_preprocess.cpp.

References allocate_dynamic_object_with_decl(), fresh_string(), and loc.

Referenced by make_copy_string_code(), make_float_to_string_code(), make_object_get_class_code(), make_string_format_code(), and make_string_returning_function_from_call().

◆ code_assign_components_to_java_string()

codet java_string_library_preprocesst::code_assign_components_to_java_string ( const exprt lhs,
const exprt rhs_array,
const exprt rhs_length,
const symbol_table_baset symbol_table 
)
private

Produce code for an assignment of a string expr to a Java string.

Parameters
lhsexpression representing the java string to assign to
rhs_arraypointer to the array to assign
rhs_lengthlength of the array to assign
symbol_tablesymbol table
Returns
return the following code:
lhs = { {Object}, length=rhs_length, data=rhs_array }

Definition at line 834 of file java_string_library_preprocess.cpp.

References checked_dereference(), exprt::copy_to_operands(), get_tag(), implements_java_char_sequence_pointer(), java_root_class_init(), symbol_table_baset::lookup(), PRECONDITION, typet::subtype(), to_struct_type(), and exprt::type().

Referenced by code_assign_string_expr_to_java_string().

◆ code_assign_java_string_to_string_expr()

void java_string_library_preprocesst::code_assign_java_string_to_string_expr ( const refined_string_exprt lhs,
const exprt rhs,
const source_locationt loc,
const symbol_table_baset symbol_table,
code_blockt code 
)
private
Parameters
lhsa string expression
rhsan expression representing a java string
locsource location
symbol_tablesymbol table
[out]codecode block that gets appended the following code:
lhs.length = rhs==null ? 0 : rhs->length
lhs.data=rhs->data

Definition at line 884 of file java_string_library_preprocess.cpp.

References code_blockt::add(), checked_dereference(), refined_string_exprt::content(), from_integer(), get_data(), get_length(), irept::id(), implements_java_char_sequence_pointer(), refined_string_exprt::length(), loc, symbol_table_baset::lookup_ref(), PRECONDITION, irept::set(), typet::subtype(), to_pointer_type(), to_symbol_type(), and exprt::type().

Referenced by convert_exprt_to_string_exprt(), make_argument_for_format(), make_copy_constructor_code(), and make_copy_string_code().

◆ code_assign_string_expr_to_java_string()

codet java_string_library_preprocesst::code_assign_string_expr_to_java_string ( const exprt lhs,
const refined_string_exprt rhs,
const symbol_table_baset symbol_table 
)
private

Produce code for an assignemnt of a string expr to a Java string.

Parameters
lhsan expression representing a java string
rhsa string expression
symbol_tablesymbol table
Returns
return the following code:
lhs = { {Object}, length=rhs.length, data=rhs.data }

Definition at line 866 of file java_string_library_preprocess.cpp.

References code_assign_components_to_java_string(), refined_string_exprt::content(), and refined_string_exprt::length().

Referenced by make_copy_constructor_code(), make_copy_string_code(), make_float_to_string_code(), make_init_from_array_code(), make_init_function_from_call(), make_object_get_class_code(), make_string_format_code(), and make_string_returning_function_from_call().

◆ code_for_function()

exprt java_string_library_preprocesst::code_for_function ( const symbolt symbol,
symbol_table_baset symbol_table 
)

Should be called to provide code for string functions that are used in the code but for which no implementation is provided.

Parameters
function_idname of the function
typeits type
loclocation in the program
symbol_tablea symbol table
Returns
Code for the body of the String functions if they are part of the supported String functions, nil_exprt otherwise.

Definition at line 1882 of file java_string_library_preprocess.cpp.

References conversion_table, cprover_equivalent_to_java_assign_and_return_function, cprover_equivalent_to_java_assign_function, cprover_equivalent_to_java_constructor, cprover_equivalent_to_java_function, cprover_equivalent_to_java_string_returning_function, loc, symbolt::location, make_assign_and_return_function_from_call(), make_assign_function_from_call(), make_function_from_call(), make_init_function_from_call(), make_string_returning_function_from_call(), symbolt::name, to_code_type(), and symbolt::type.

Referenced by java_bytecode_languaget::convert_single_method().

◆ code_return_function_application()

codet java_string_library_preprocesst::code_return_function_application ( const irep_idt function_name,
const exprt::operandst arguments,
const typet type,
symbol_table_baset symbol_table 
)
private

return the result of a function call

Parameters
function_namethe name of the function
argumentsa list of arguments
typethe return type
symbol_tablea symbol table
Returns
the following code:
return <function_name>(arguments)

Definition at line 636 of file java_string_library_preprocess.cpp.

References make_function_application().

Referenced by make_function_from_call().

◆ convert_exprt_to_string_exprt()

refined_string_exprt java_string_library_preprocesst::convert_exprt_to_string_exprt ( const exprt expr_to_process,
const source_locationt loc,
symbol_table_baset symbol_table,
code_blockt init_code 
)
private

Creates a string_exprt from the input exprt representing a char sequence.

Parameters
expr_to_processan expression of a type which implements char sequence
loclocation in the source
symbol_tablesymbol table
init_codecode block, in which declaration will be added:
char *cprover_string_content;
int cprover_string_length;
cprover_string_length = a->length;
cprover_string_content = a->data;
Returns
the processed operand: {content=cprover_string_content, length=cprover_string_length}

Definition at line 311 of file java_string_library_preprocess.cpp.

References code_assign_java_string_to_string_expr(), decl_string_expr(), implements_java_char_sequence_pointer(), loc, PRECONDITION, and exprt::type().

Referenced by process_equals_function_operands(), and process_operands().

◆ decl_string_expr()

refined_string_exprt java_string_library_preprocesst::decl_string_expr ( const source_locationt loc,
symbol_table_baset symbol_table,
code_blockt code 
)
private

Add declaration of a refined string expr whose content and length are fresh symbols.

Parameters
locsource location
symbol_tablethe symbol table
code[out] : code block to which the declaration is added
Returns
refined string expr with fresh content and length symbols

Definition at line 506 of file java_string_library_preprocess.cpp.

References code_blockt::add(), get_fresh_aux_symbol(), index_type, java_char_type(), loc, pointer_type(), refined_string_type, and symbolt::symbol_expr().

Referenced by convert_exprt_to_string_exprt(), make_copy_constructor_code(), make_copy_string_code(), and make_nondet_string_expr().

◆ fresh_array()

symbol_exprt java_string_library_preprocesst::fresh_array ( const typet type,
const source_locationt location,
symbol_tablet symbol_table 
)
private

add a symbol in the table with static lifetime and name containing cprover_string_array and given type

Parameters
typean array type
locationa location in the program
symbol_tablesymbol table

Definition at line 258 of file java_string_library_preprocess.cpp.

References get_fresh_aux_symbol(), symbolt::is_static_lifetime, and symbolt::symbol_expr().

Referenced by allocate_fresh_array().

◆ fresh_string()

symbol_exprt java_string_library_preprocesst::fresh_string ( const typet type,
const source_locationt loc,
symbol_table_baset symbol_table 
)
private

add a symbol with static lifetime and name containing cprover_string and given type

Parameters
typea type for refined strings
loca location in the program
symbol_tablesymbol table
Returns
a new symbol

Definition at line 489 of file java_string_library_preprocess.cpp.

References get_fresh_aux_symbol(), symbolt::is_static_lifetime, loc, and symbolt::symbol_expr().

Referenced by allocate_fresh_string().

◆ get_all_function_names()

void java_string_library_preprocesst::get_all_function_names ( std::unordered_set< irep_idt > &  methods) const

◆ get_object_at_index()

exprt java_string_library_preprocesst::get_object_at_index ( const exprt argv,
int  index 
)
private

Helper for format function.

Returns the expression:

*((void**)(argv->data)+index )

which corresponds to the object at position index in argv.

Parameters
argvreference to an array of references
indexindex of the desired object
Returns
An expression representing the object at position index of argv.

Definition at line 1343 of file java_string_library_preprocess.cpp.

References from_integer(), java_int_type(), pointer_type(), typet::subtype(), and exprt::type().

Referenced by make_argument_for_format().

◆ get_primitive_value_of_object()

exprt java_string_library_preprocesst::get_primitive_value_of_object ( const exprt object,
irep_idt  type_name,
const source_locationt loc,
symbol_table_baset symbol_table,
code_blockt code 
)
private

Adds to the code an assignment of the form

type_name tmp_type_name
tmp_type_name = ((Classname*)arg_i)->value

and returns tmp_typename.

In case the class corresponding to type_name is not available in symbol_table, the variable is declared but not assigned. Used to access the values of the arguments of String.format.

Parameters
objectan expression representing a reference to an object
type_namename of the corresponding primitive type, this can be one of the following: ID_boolean, ID_char, ID_byte, ID_short, ID_int, ID_long, ID_float, ID_double, ID_void
loca location in the source
symbol_tablethe symbol table
codecode block to which we are adding some assignments
Returns
An expression contaning a symbol tmp_type_name where type_name is the given argument (ie. boolean, char etc.). Which represents the primitive value contained in the given object.

Definition at line 1245 of file java_string_library_preprocess.cpp.

References code_blockt::add(), DATA_INVARIANT, messaget::eom(), struct_union_typet::get_component(), get_fresh_aux_symbol(), struct_union_typet::componentt::get_name(), id2string(), irept::is_nil(), java_boolean_type(), java_byte_type(), java_char_type(), java_double_type(), java_float_type(), java_int_type(), java_long_type(), java_short_type(), loc, symbol_table_baset::lookup(), pointer_type(), typet::subtype(), symbolt::symbol_expr(), to_struct_type(), exprt::type(), UNREACHABLE, and messaget::warning().

Referenced by make_argument_for_format().

◆ get_string_type_base_classes()

std::vector< irep_idt > java_string_library_preprocesst::get_string_type_base_classes ( const irep_idt class_name)

Gets the base classes for known String and String-related types, or returns an empty list for other types.

Parameters
class_nameclass identifier, without "java::" prefix.
Returns
a list of base classes, again without "java::" prefix.

Definition at line 194 of file java_string_library_preprocess.cpp.

References is_known_string_type().

Referenced by add_string_type(), and java_bytecode_languaget::parse().

◆ implements_function()

bool java_string_library_preprocesst::implements_function ( const irep_idt function_id) const

◆ implements_java_char_sequence()

static bool java_string_library_preprocesst::implements_java_char_sequence ( const typet type)
inlinestatic

◆ implements_java_char_sequence_pointer()

◆ initialize_conversion_table()

◆ initialize_known_type_table()

void java_string_library_preprocesst::initialize_known_type_table ( )

Definition at line 1930 of file java_string_library_preprocess.cpp.

References string_types.

Referenced by java_bytecode_languaget::parse().

◆ initialize_refined_string_type()

void java_string_library_preprocesst::initialize_refined_string_type ( )

◆ is_java_char_array_pointer_type()

bool java_string_library_preprocesst::is_java_char_array_pointer_type ( const typet type)
staticprivate
parameters: a type
Returns
Boolean telling whether the type is that of a pointer to a java char array

Definition at line 159 of file java_string_library_preprocess.cpp.

References irept::id(), is_java_char_array_type(), typet::subtype(), and to_pointer_type().

Referenced by process_operands().

◆ is_java_char_array_type()

bool java_string_library_preprocesst::is_java_char_array_type ( const typet type)
staticprivate
Parameters
typea type
Returns
Boolean telling whether the type is that of java char array

Definition at line 150 of file java_string_library_preprocess.cpp.

References java_type_matches_tag().

Referenced by is_java_char_array_pointer_type().

◆ is_java_char_sequence_pointer_type()

bool java_string_library_preprocesst::is_java_char_sequence_pointer_type ( const typet type)
staticprivate
Parameters
typea type
Returns
Boolean telling whether the type is that of a pointer to a java char sequence

Definition at line 136 of file java_string_library_preprocess.cpp.

References irept::id(), is_java_char_sequence_type(), typet::subtype(), and to_pointer_type().

Referenced by implements_java_char_sequence_pointer().

◆ is_java_char_sequence_type()

bool java_string_library_preprocesst::is_java_char_sequence_type ( const typet type)
staticprivate
Parameters
typea type
Returns
Boolean telling whether the type is that of java char sequence

Definition at line 127 of file java_string_library_preprocess.cpp.

References java_type_matches_tag().

Referenced by implements_java_char_sequence(), and is_java_char_sequence_pointer_type().

◆ is_java_string_buffer_pointer_type()

bool java_string_library_preprocesst::is_java_string_buffer_pointer_type ( const typet type)
staticprivate
Parameters
typea type
Returns
Boolean telling whether the type is that of java StringBuffer pointers

Definition at line 113 of file java_string_library_preprocess.cpp.

References irept::id(), is_java_string_buffer_type(), typet::subtype(), and to_pointer_type().

Referenced by implements_java_char_sequence_pointer().

◆ is_java_string_buffer_type()

bool java_string_library_preprocesst::is_java_string_buffer_type ( const typet type)
staticprivate
Parameters
typea type
Returns
Boolean telling whether the type is that of java StringBuffer

Definition at line 104 of file java_string_library_preprocess.cpp.

References java_type_matches_tag().

Referenced by implements_java_char_sequence(), and is_java_string_buffer_pointer_type().

◆ is_java_string_builder_pointer_type()

bool java_string_library_preprocesst::is_java_string_builder_pointer_type ( const typet type)
staticprivate
Parameters
typea type
Returns
Boolean telling whether the type is that of java StringBuilder pointers

Definition at line 90 of file java_string_library_preprocess.cpp.

References irept::id(), is_java_string_builder_type(), typet::subtype(), and to_pointer_type().

Referenced by implements_java_char_sequence_pointer().

◆ is_java_string_builder_type()

bool java_string_library_preprocesst::is_java_string_builder_type ( const typet type)
staticprivate
Parameters
typea type
Returns
Boolean telling whether the type is that of java StringBuilder

Definition at line 81 of file java_string_library_preprocess.cpp.

References java_type_matches_tag().

Referenced by implements_java_char_sequence(), and is_java_string_builder_pointer_type().

◆ is_java_string_pointer_type()

bool java_string_library_preprocesst::is_java_string_pointer_type ( const typet type)
staticprivate
Parameters
typea type
Returns
Boolean telling whether the type is that of java string pointer

Definition at line 59 of file java_string_library_preprocess.cpp.

References irept::id(), is_java_string_type(), typet::subtype(), and to_pointer_type().

Referenced by implements_java_char_sequence_pointer().

◆ is_java_string_type()

bool java_string_library_preprocesst::is_java_string_type ( const typet type)
staticprivate
Parameters
typea type
Returns
Boolean telling whether the type is that of java string

Definition at line 73 of file java_string_library_preprocess.cpp.

References java_type_matches_tag().

Referenced by implements_java_char_sequence(), and is_java_string_pointer_type().

◆ is_known_string_type()

bool java_string_library_preprocesst::is_known_string_type ( irep_idt  class_name)

Check whether a class name is known as a string type.

Parameters
class_namename of the class
Returns
True if the type is one that is known to our preprocessing, false otherwise

Definition at line 1924 of file java_string_library_preprocess.cpp.

References string_types.

Referenced by get_string_type_base_classes(), and java_bytecode_convert_classt::operator()().

◆ java_type_matches_tag()

bool java_string_library_preprocesst::java_type_matches_tag ( const typet type,
const std::string &  tag 
)
staticprivate
Parameters
typea type
taga string
Returns
Boolean telling whether the type is a struct with the given tag or a symbolic type with the tag prefixed by "java::"

Definition at line 51 of file java_string_library_preprocess.cpp.

References get_tag().

Referenced by is_java_char_array_type(), is_java_char_sequence_type(), is_java_string_buffer_type(), is_java_string_builder_type(), and is_java_string_type().

◆ make_argument_for_format()

exprt java_string_library_preprocesst::make_argument_for_format ( const exprt argv,
int  index,
const struct_typet structured_type,
const source_locationt loc,
const irep_idt function_id,
symbol_table_baset symbol_table,
code_blockt code 
)
private

Helper for format function.

Adds code:

string_expr arg_i_string_expr;
int tmp_int;
float tmp_float;
char tmp_char;
boolean tmp_boolean;
Object* arg_i=get_object_at_index(argv, index)
if(arg_i!=NULL)
{
if(arg_i.@class_identifier=="java::java.lang.String")
{
arg_i_string_expr = (string_expr)((String*)arg_i_as_string)
}
tmp_int=((Integer)arg_i)->value
tmp_float=((Float)arg_i)->value
tmp_char=((Char)arg_i)->value
tmp_boolean=((Boolean)arg_i)->value
}
arg_i_struct = { string_expr=arg_i_string_expr;
integer=tmp_int; float=tmp_float; char=tmp_char; boolean=tmp_boolean}

and returns arg_i_struct.

TODO: date_time and hash code are not implemented

Parameters
argvreference to an array of references
indexindex of the desired argument
structured_typetype for arguments of the internal format function
loca location in the source
symbol_tablethe symbol table
codecode block to which we are adding some assignments
Returns
An expression of type structured_type representing the possible values of the argument at position index of argv.

Definition at line 1391 of file java_string_library_preprocess.cpp.

References code_blockt::add(), allocate_dynamic_object_with_decl(), code_assign_java_string_to_string_expr(), struct_union_typet::components(), code_ifthenelset::cond(), exprt::copy_to_operands(), get_fresh_aux_symbol(), get_object_at_index(), get_primitive_value_of_object(), id2string(), java_reference_type(), loc, make_nondet_string_expr(), symbolt::symbol_expr(), to_pointer_type(), to_string_expr(), and exprt::type().

Referenced by make_string_format_code().

◆ make_assign_and_return_function_from_call()

codet java_string_library_preprocesst::make_assign_and_return_function_from_call ( const irep_idt function_name,
const code_typet type,
const source_locationt loc,
symbol_table_baset symbol_table 
)
private

Call a cprover internal function, assign the result to object this and return it.

Parameters
function_namename of the function to be called
typethe type of the function call
loclocation in program
symbol_tablethe symbol table to populate
Returns
Code calling function with the given function name.

Definition at line 1188 of file java_string_library_preprocess.cpp.

References code_blockt::add(), loc, make_assign_function_from_call(), code_typet::parameters(), and PRECONDITION.

Referenced by code_for_function().

◆ make_assign_function_from_call()

codet java_string_library_preprocesst::make_assign_function_from_call ( const irep_idt function_name,
const code_typet type,
const source_locationt loc,
symbol_table_baset symbol_table 
)
private

Call a cprover internal function and assign the result to object this.

Parameters
function_namename of the function to be called
typethe type of the function call
loclocation in program
symbol_tablethe symbol table to populate
Returns
Code assigning result of a call to the function with given function name.

Definition at line 1213 of file java_string_library_preprocess.cpp.

References loc, and make_init_function_from_call().

Referenced by code_for_function(), and make_assign_and_return_function_from_call().

◆ make_copy_constructor_code()

codet java_string_library_preprocesst::make_copy_constructor_code ( const code_typet type,
const source_locationt loc,
const irep_idt function_id,
symbol_table_baset symbol_table 
)
private

Generates code for a constructor of a string object from another string object.

Parameters
typetype of the function
loclocation in the source
symbol_tablesymbol table
Returns
Code corresponding to:
string_expr = java_string_to_string_expr(arg1)
string_expr_sym = { string_expr.length; string_expr.content }
this = string_expr_to_java_string(string_expr)

Definition at line 1745 of file java_string_library_preprocess.cpp.

References code_blockt::add(), code_assign_java_string_to_string_expr(), code_assign_string_expr_to_java_string(), decl_string_expr(), loc, and code_typet::parameters().

Referenced by initialize_conversion_table().

◆ make_copy_string_code()

codet java_string_library_preprocesst::make_copy_string_code ( const code_typet type,
const source_locationt loc,
const irep_idt function_id,
symbol_table_baset symbol_table 
)
private

Generates code for a function which copies a string object to a new string object.

Parameters
typetype of the function
loclocation in the source
symbol_tablesymbol table
Returns
Code corresponding to:
string_expr = string_to_string_expr(arg0)
string_expr_sym = { string_expr.length; string_expr.content }
str = new String
str = string_expr_to_string(string_expr)
return str

Definition at line 1704 of file java_string_library_preprocess.cpp.

References code_blockt::add(), allocate_fresh_string(), code_assign_java_string_to_string_expr(), code_assign_string_expr_to_java_string(), decl_string_expr(), code_typet::parametert::get_identifier(), loc, code_typet::parameters(), code_typet::return_type(), and exprt::type().

Referenced by initialize_conversion_table().

◆ make_equals_function_code()

codet java_string_library_preprocesst::make_equals_function_code ( const code_typet type,
const source_locationt loc,
const irep_idt function_id,
symbol_table_baset symbol_table 
)
private

Used to provide code for the Java String.equals(Object) function.

Parameters
typetype of the function call
loclocation in the program_invocation_name
symbol_tablesymbol table
Returns
Code corresponding to:
IF arg->@class_identifier == "java.lang.String"
THEN
string_expr1 = {this->length; *this->data}
string_expr2 = {arg->length; *arg->data}
bool string_equals_tmp = cprover_string_equal(string_expr1, string_expr2)
return string_equals_tmp
ELSE
return false

Definition at line 954 of file java_string_library_preprocess.cpp.

References code_blockt::add(), checked_dereference(), code_ifthenelset::cond(), code_ifthenelset::else_case(), from_integer(), get_fresh_aux_symbol(), loc, make_function_application(), code_typet::parameters(), process_equals_function_operands(), code_typet::return_type(), symbolt::symbol_expr(), and code_ifthenelset::then_case().

Referenced by initialize_conversion_table().

◆ make_float_to_string_code()

codet java_string_library_preprocesst::make_float_to_string_code ( const code_typet type,
const source_locationt loc,
const irep_idt function_id,
symbol_table_baset symbol_table 
)
private

Provide code for the String.valueOf(F) function.

Parameters
typetype of the function call
loclocation in the program_invocation_name
symbol_tablesymbol table
Returns
Code corresponding to the Java conversion of floats to strings.

Definition at line 1004 of file java_string_library_preprocess.cpp.

References code_blockt::add(), allocate_fresh_string(), ieee_floatt::change_spec(), code_assign_string_expr_to_java_string(), code_ifthenelset::cond(), code_ifthenelset::else_case(), ieee_floatt::from_float(), INVARIANT, loc, code_typet::parameters(), PRECONDITION, code_typet::return_type(), string_expr_of_function(), string_literal_to_string_expr(), code_ifthenelset::then_case(), ieee_floatt::to_expr(), and to_floatbv_type().

Referenced by initialize_conversion_table().

◆ make_function_from_call()

codet java_string_library_preprocesst::make_function_from_call ( const irep_idt function_name,
const code_typet type,
const source_locationt loc,
symbol_table_baset symbol_table 
)
private

Provide code for a function that calls a function from the solver and simply returns it.

Parameters
function_namename of the function to be called
typetype of the function
loclocation in the source
symbol_tablesymbol table
Returns
Code corresponding to:
return function_name(args)

Definition at line 1633 of file java_string_library_preprocess.cpp.

References code_blockt::add(), code_return_function_application(), loc, code_typet::parameters(), process_parameters(), and code_typet::return_type().

Referenced by code_for_function().

◆ make_init_from_array_code()

codet java_string_library_preprocesst::make_init_from_array_code ( const code_typet type,
const source_locationt loc,
const irep_idt function_id,
symbol_table_baset symbol_table 
)
private

Used to provide code for constructor from a char array.

The implementation is similar to substring except the 3rd argument is a count instead of end index

Parameters
typetype of the function call
loclocation in the program_invocation_name
symbol_tablesymbol table
Returns
code implementing String intitialization from a char array and arguments offset and end.

Definition at line 1780 of file java_string_library_preprocess.cpp.

References code_blockt::add(), code_assign_string_expr_to_java_string(), INVARIANT, loc, code_typet::parameters(), PRECONDITION, process_parameters(), string_expr_of_function(), and to_string_expr().

Referenced by initialize_conversion_table().

◆ make_init_function_from_call()

codet java_string_library_preprocesst::make_init_function_from_call ( const irep_idt function_name,
const code_typet type,
const source_locationt loc,
symbol_table_baset symbol_table,
bool  ignore_first_arg = true 
)
private

Generate the goto code for string initialization.

Parameters
function_namename of the function to be called
typethe type of the function call
loclocation in program
symbol_tablethe symbol table to populate
ignore_first_argboolean flag telling that the first argument should not be part of the arguments of the call (but only used to be assigned the result)
Returns
code for the String.<init>(args) function:
cprover_string_length = fun(arg).length;
cprover_string_array = fun(arg).data;
this->length = cprover_string_length;
this->data = cprover_string_array;
cprover_string = {.=cprover_string_length, .=cprover_string_array};

Definition at line 1147 of file java_string_library_preprocess.cpp.

References code_blockt::add(), code_assign_string_expr_to_java_string(), loc, code_typet::parameters(), PRECONDITION, process_parameters(), and string_expr_of_function().

Referenced by code_for_function(), and make_assign_function_from_call().

◆ make_nondet_string_expr()

refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr ( const source_locationt loc,
const irep_idt function_id,
symbol_table_baset symbol_table,
code_blockt code 
)
private

add symbols with prefix cprover_string_length and cprover_string_data and construct a string_expr from them.

Parameters
loca location in the program
symbol_tablesymbol table
codecode block to which allocation instruction will be added
Returns
a new string_expr

Definition at line 540 of file java_string_library_preprocess.cpp.

References code_blockt::add(), add_array_to_length_association(), add_pointer_to_array_association(), refined_string_exprt::content(), decl_string_expr(), from_integer(), java_int_type(), refined_string_exprt::length(), loc, make_nondet_infinite_char_array(), and exprt::type().

Referenced by make_argument_for_format(), and string_expr_of_function().

◆ make_object_get_class_code()

codet java_string_library_preprocesst::make_object_get_class_code ( const code_typet type,
const source_locationt loc,
const irep_idt function_id,
symbol_table_baset symbol_table 
)
private

Used to provide our own implementation of the java.lang.Object.getClass() function.

Parameters
typetype of the function called
loclocation in the source
symbol_tablethe symbol table
Returns
Code corresponding to
Class class1;
string_expr1 = substr(this->@class_identifier, 6)
class1=Class.forName(string_expr1)
return class1

Definition at line 1555 of file java_string_library_preprocess.cpp.

References code_blockt::add(), allocate_fresh_string(), code_function_callt::arguments(), checked_dereference(), code_assign_string_expr_to_java_string(), from_integer(), code_function_callt::function(), get_fresh_aux_symbol(), java_int_type(), java_reference_type(), code_function_callt::lhs(), loc, symbol_table_baset::lookup_ref(), code_typet::parameters(), string_expr_of_function(), typet::subtype(), symbolt::type, and exprt::type().

Referenced by initialize_conversion_table().

◆ make_string_format_code()

codet java_string_library_preprocesst::make_string_format_code ( const code_typet type,
const source_locationt loc,
const irep_idt function_id,
symbol_table_baset symbol_table 
)
private

Used to provide code for the Java String.format function.

TODO: date_time and hash code are not implemented, and we set a limit of 10 arguments

Parameters
typetype of the function call
loclocation in the program_invocation_name
symbol_tablesymbol table
Returns
Code implementing the Java String.format function. Since the exact class of the arguments is not known, we give as argument to the internal format function a structure containing the different possible types.

Definition at line 1496 of file java_string_library_preprocess.cpp.

References irept::add(), allocate_fresh_string(), code_assign_string_expr_to_java_string(), struct_union_typet::components(), INVARIANT, java_boolean_type(), java_char_type(), java_float_type(), java_int_type(), loc, make_argument_for_format(), MAX_FORMAT_ARGS, code_typet::parameters(), PRECONDITION, process_parameters(), refined_string_type, code_typet::return_type(), and string_expr_of_function().

Referenced by initialize_conversion_table().

◆ make_string_length_code()

codet java_string_library_preprocesst::make_string_length_code ( const code_typet type,
const source_locationt loc,
const irep_idt function_id,
symbol_table_baset symbol_table 
)
private

Generates code for the String.length method.

Parameters
typetype of the function
loclocation in the source
symbol_tablesymbol table
Returns
Code corresponding to:
str_expr = java_string_to_string_expr(this)
str_expr_sym = str_expr
return this->length

Definition at line 1828 of file java_string_library_preprocess.cpp.

References checked_dereference(), get_length(), code_typet::parameters(), typet::subtype(), and exprt::type().

Referenced by initialize_conversion_table().

◆ make_string_returning_function_from_call()

codet java_string_library_preprocesst::make_string_returning_function_from_call ( const irep_idt function_name,
const code_typet type,
const source_locationt loc,
symbol_table_baset symbol_table 
)
private

Provide code for a function that calls a function from the solver and return the string_expr result as a Java string.

Parameters
function_namename of the function to be called
typetype of the function
loclocation in the source
symbol_tablesymbol table
Returns
Code corresponding to:
string_expr = function_name(args)
string = new String
string = string_expr_to_string(string)
return string

Definition at line 1662 of file java_string_library_preprocess.cpp.

References code_blockt::add(), allocate_fresh_string(), code_assign_string_expr_to_java_string(), loc, code_typet::parameters(), process_parameters(), code_typet::return_type(), and string_expr_of_function().

Referenced by code_for_function().

◆ make_string_to_char_array_code()

codet java_string_library_preprocesst::make_string_to_char_array_code ( const code_typet type,
const source_locationt loc,
const irep_idt function_id,
symbol_tablet symbol_table 
)
private

◆ process_equals_function_operands()

exprt::operandst java_string_library_preprocesst::process_equals_function_operands ( const exprt::operandst operands,
const source_locationt loc,
symbol_table_baset symbol_table,
code_blockt init_code 
)
private

Converts the operands of the equals function to string expressions and outputs these conversions.

As a side effect of the conversions it adds some code to init_code.

Parameters
operandsa list of expressions
loclocation in the source
symbol_tablesymbol table
init_codecode block, in which declaration of some arguments may be added
Returns
a list of expressions

Definition at line 366 of file java_string_library_preprocess.cpp.

References convert_exprt_to_string_exprt(), implements_java_char_sequence_pointer(), loc, PRECONDITION, to_pointer_type(), and exprt::type().

Referenced by make_equals_function_code().

◆ process_operands()

exprt::operandst java_string_library_preprocesst::process_operands ( const exprt::operandst operands,
const source_locationt loc,
symbol_table_baset symbol_table,
code_blockt init_code 
)
private

for each expression that is of a type implementing strings, we declare a new cprover_string whose contents is deduced from the expression and replace the expression by this cprover_string in the output list; in the other case the expression is kept as is for the output list.

Also does the same thing for char array references.

Parameters
operandsa list of expressions
loclocation in the source
symbol_tablesymbol table
init_codecode block, in which declaration of some arguments may be added
Returns
a list of expressions

Definition at line 336 of file java_string_library_preprocess.cpp.

References convert_exprt_to_string_exprt(), implements_java_char_sequence_pointer(), is_java_char_array_pointer_type(), loc, and replace_char_array().

Referenced by process_parameters().

◆ process_parameters()

exprt::operandst java_string_library_preprocesst::process_parameters ( const code_typet::parameterst params,
const source_locationt loc,
symbol_table_baset symbol_table,
code_blockt init_code 
)
private

calls string_refine_preprocesst::process_operands with a list of parameters.

Parameters
paramsa list of function parameters
loclocation in the source
symbol_tablesymbol table
init_codecode block, in which declaration of some arguments may be added
Returns
a list of expressions

Definition at line 281 of file java_string_library_preprocess.cpp.

References loc, and process_operands().

Referenced by make_function_from_call(), make_init_from_array_code(), make_init_function_from_call(), make_string_format_code(), and make_string_returning_function_from_call().

◆ replace_char_array()

refined_string_exprt java_string_library_preprocesst::replace_char_array ( const exprt array_pointer,
const source_locationt loc,
symbol_table_baset symbol_table,
code_blockt code 
)
private

we declare a new cprover_string whose contents is deduced from the char array.

Parameters
array_pointeran expression of type char array pointer
loclocation in the source
symbol_tablesymbol table
codecode block, in which some assignments will be added
Returns
a string expression

Definition at line 453 of file java_string_library_preprocess.cpp.

References code_blockt::add(), add_pointer_to_array_association(), checked_dereference(), refined_string_exprt::content(), get_data(), get_fresh_aux_symbol(), get_length(), java_char_type(), java_int_type(), loc, refined_string_type, typet::subtype(), symbolt::symbol_expr(), and exprt::type().

Referenced by process_operands().

◆ replace_character_call()

codet java_string_library_preprocesst::replace_character_call ( code_function_callt  call)
inline

◆ string_expr_of_function()

refined_string_exprt java_string_library_preprocesst::string_expr_of_function ( const irep_idt function_name,
const exprt::operandst arguments,
const source_locationt loc,
symbol_table_baset symbol_table,
code_blockt code 
)
private

Create a refined_string_exprt str whose content and length are fresh symbols, calls the string primitive with name function_name.

In the arguments of the primitive str takes the place of the result and the following arguments are given by parameter `arguments.

Parameters
function_namethe name of the function
argumentsarguments of the function
locsource location
symbol_tablesymbol table
[out]codegets added the following code:
int return_code;
int str.length;
char str.data[str.length]
return_code = <function_name>(str.length, str.data, arguments)
Returns
refined string expression str

Definition at line 789 of file java_string_library_preprocess.cpp.

References code_blockt::add(), dstringt::c_str(), code_assign_function_application(), refined_string_exprt::content(), get_fresh_aux_symbol(), java_int_type(), refined_string_exprt::length(), loc, make_nondet_string_expr(), and symbolt::symbol_expr().

Referenced by make_float_to_string_code(), make_init_from_array_code(), make_init_function_from_call(), make_object_get_class_code(), make_string_format_code(), make_string_returning_function_from_call(), and string_literal_to_string_expr().

◆ string_literal_to_string_expr()

refined_string_exprt java_string_library_preprocesst::string_literal_to_string_expr ( const std::string &  s,
const source_locationt loc,
symbol_table_baset symbol_table,
code_blockt code 
)
private

Create a string expression whose value is given by a literal.

Parameters
sthe literal to be assigned
loclocation in the source
symbol_tablesymbol table
[out]codegets added the following:
tmp_string = "<s>"
lhs = cprover_string_literal_func(tmp_string)
Returns
a new refined string

Definition at line 928 of file java_string_library_preprocess.cpp.

References loc, and string_expr_of_function().

Referenced by make_float_to_string_code().

Friends And Related Function Documentation

◆ convert_exprt_to_string_exprt_unit_test

refined_string_exprt convert_exprt_to_string_exprt_unit_test ( java_string_library_preprocesst preprocess,
const exprt deref,
const source_locationt loc,
symbol_tablet symbol_table,
code_blockt init_code 
)
friend

Member Data Documentation

◆ char_type

const typet java_string_library_preprocesst::char_type
private

Definition at line 97 of file java_string_library_preprocess.h.

◆ character_preprocess

character_refine_preprocesst java_string_library_preprocesst::character_preprocess
private

◆ conversion_table

std::unordered_map<irep_idt, conversion_functiont> java_string_library_preprocesst::conversion_table
private

◆ cprover_equivalent_to_java_assign_and_return_function

id_mapt java_string_library_preprocesst::cprover_equivalent_to_java_assign_and_return_function
private

◆ cprover_equivalent_to_java_assign_function

id_mapt java_string_library_preprocesst::cprover_equivalent_to_java_assign_function
private

◆ cprover_equivalent_to_java_constructor

id_mapt java_string_library_preprocesst::cprover_equivalent_to_java_constructor
private

◆ cprover_equivalent_to_java_function

id_mapt java_string_library_preprocesst::cprover_equivalent_to_java_function
private

◆ cprover_equivalent_to_java_string_returning_function

id_mapt java_string_library_preprocesst::cprover_equivalent_to_java_string_returning_function
private

◆ id_maps

◆ index_type

const typet java_string_library_preprocesst::index_type
private

Definition at line 98 of file java_string_library_preprocess.h.

Referenced by decl_string_expr().

◆ refined_string_type

const refined_string_typet java_string_library_preprocesst::refined_string_type
private

◆ string_types

std::unordered_set<irep_idt> java_string_library_preprocesst::string_types
private

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