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

refined_string_exprt replace_char_array (const exprt &array_pointer, const source_locationt &loc, const irep_idt &function_name, symbol_table_baset &symbol_table, code_blockt &code)

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

symbol_exprt fresh_string (const typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)

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

refined_string_exprt decl_string_expr (const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)

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

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.

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

codet code_return_function_application (const irep_idt &function_id, const exprt::operandst &arguments, const typet &type, symbol_table_baset &symbol_table)

return the result of a function call

refined_string_exprt string_expr_of_function (const irep_idt &function_id, 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_id.

codet code_assign_components_to_java_string (const exprt &lhs, const exprt &rhs_array, const exprt &rhs_length, const symbol_table_baset &symbol_table, bool is_constructor)

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

codet code_assign_string_expr_to_java_string (const exprt &lhs, const refined_string_exprt &rhs, const symbol_table_baset &symbol_table, bool is_constructor)

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

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.

code_blockt make_function_from_call (const irep_idt &function_id, const java_method_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.

code_blockt make_init_function_from_call (const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table, bool is_constructor=true)

Generate the goto code for string initialization.

code_blockt make_assign_and_return_function_from_call (const irep_idt &function_id, const java_method_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.

code_blockt make_assign_function_from_call (const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)

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

code_blockt make_string_returning_function_from_call (const irep_idt &function_id, const java_method_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.

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_functiont > conversion_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_idt > string_types

Friends

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

Detailed Description

Definition at line 37 of file java_string_library_preprocess.h.

Member Typedef Documentation

◆ conversion_functiont

typedef std::function<codet( const java_method_typet &, const source_locationt &, const irep_idt &, symbol_table_baset &, message_handlert &)> java_string_library_preprocesst::conversion_functiont

private

Definition at line 112 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 114 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 40 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_table_baset & symbol_table

)

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

Parameters: class_name a name for the class such as "java.lang.String"

symbol_table symbol table to which the class will be added

Definition at line 220 of file java_string_library_preprocess.cpp.

◆ 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: type a type for string

loc a location in the program

function_id function the fresh string is created in

symbol_table symbol table

code code block to which allocation instruction will be added

Returns: a new string

Definition at line 549 of file java_string_library_preprocess.cpp.

◆ 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,

bool is_constructor

)

private

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

Parameters: lhs expression representing the java string to assign to

rhs_array pointer to the array to assign

rhs_length length of the array to assign

symbol_table symbol table

is_constructor the assignment happens in the context of a constructor, so the whole object should be initialised, not just its length and data fields.

Returns: return the following code:
lhs = { {Object}, length=rhs_length, data=rhs_array }

ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566

Definition at line 797 of file java_string_library_preprocess.cpp.

◆ 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: lhs a string expression

rhs an expression representing a java string

loc source location

symbol_table symbol table

[out] code code block that gets appended the following code:
lhs.length = rhs==null ? 0 : rhs->length

lhs.data=rhs->data

Definition at line 859 of file java_string_library_preprocess.cpp.

◆ 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,

bool is_constructor

)

private

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

Parameters: lhs an expression representing a java string

rhs a string expression

symbol_table symbol table

is_constructor the assignment happens in the context of a constructor, so the whole object should be initialised, not just its length and data fields.

Returns: return the following code:
lhs = { {Object}, length=rhs.length, data=rhs.data }

Definition at line 840 of file java_string_library_preprocess.cpp.

◆ code_for_function()

codet java_string_library_preprocesst::code_for_function ( const symbolt & symbol,

symbol_table_baset & symbol_table,

message_handlert & message_handler

)

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

Parameters: symbol symbol of the function to provide code for

symbol_table a symbol table

message_handler a message handler

Returns: Code for the body of the String functions if they are part of the supported String functions, nil_exprt otherwise.

Definition at line 1462 of file java_string_library_preprocess.cpp.

◆ code_return_function_application()

codet java_string_library_preprocesst::code_return_function_application ( const irep_idt & function_id,

const exprt::operandst & arguments,

const typet & type,

symbol_table_baset & symbol_table

)

private

return the result of a function call

Parameters: function_id the name of the function

arguments a list of arguments

type the return type

symbol_table a symbol table

Returns: the following code:
return <function_id>(arguments)

Definition at line 599 of file java_string_library_preprocess.cpp.

◆ 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,

const irep_idt & function_id,

code_blockt & init_code

)

private

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

Parameters: expr_to_process an expression of a type which implements char sequence

loc location in the source

symbol_table symbol table

function_id name of the function in which the code will be added

init_code code 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 309 of file java_string_library_preprocess.cpp.

◆ decl_string_expr()

refined_string_exprt java_string_library_preprocesst::decl_string_expr ( const source_locationt & loc,

const irep_idt & function_id,

symbol_table_baset & symbol_table,

code_blockt & code

)

private

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

Parameters: loc source location

function_id name of the function in which the string is defined

symbol_table the symbol table

[out] code code block to which the declaration is added

Returns: refined string expr with fresh content and length symbols

Definition at line 487 of file java_string_library_preprocess.cpp.

◆ fresh_string()

symbol_exprt java_string_library_preprocesst::fresh_string ( const typet & type,

const source_locationt & loc,

const irep_idt & function_id,

symbol_table_baset & symbol_table

)

private

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

Parameters: type a type for refined strings

loc a location in the program

function_id name of the function in which the code will be added

symbol_table symbol table

Returns: a new symbol

Definition at line 468 of file java_string_library_preprocess.cpp.

◆ get_all_function_names()

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

Definition at line 1446 of file java_string_library_preprocess.cpp.

◆ 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_name class identifier, without "java::" prefix.

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

Definition at line 187 of file java_string_library_preprocess.cpp.

◆ implements_function()

bool java_string_library_preprocesst::implements_function ( const irep_idt & function_id ) const

Definition at line 1422 of file java_string_library_preprocess.cpp.

◆ implements_java_char_sequence()

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

inlinestatic

Definition at line 75 of file java_string_library_preprocess.h.

◆ implements_java_char_sequence_pointer()

static bool java_string_library_preprocesst::implements_java_char_sequence_pointer ( const typet & type )

inlinestatic

Definition at line 68 of file java_string_library_preprocess.h.

◆ initialize_conversion_table()

void java_string_library_preprocesst::initialize_conversion_table ( )

fill maps with correspondence from java method names to conversion functions

Definition at line 1520 of file java_string_library_preprocess.cpp.

◆ initialize_known_type_table()

void java_string_library_preprocesst::initialize_known_type_table ( )

Definition at line 1511 of file java_string_library_preprocess.cpp.

◆ 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 164 of file java_string_library_preprocess.cpp.

◆ is_java_char_array_type()

bool java_string_library_preprocesst::is_java_char_array_type ( const typet & type )

staticprivate

Parameters: type a type

Returns: Boolean telling whether the type is that of java char array

Definition at line 155 of file java_string_library_preprocess.cpp.

◆ is_java_char_sequence_pointer_type()

bool java_string_library_preprocesst::is_java_char_sequence_pointer_type ( const typet & type )

staticprivate

Parameters: type a type

Returns: Boolean telling whether the type is that of a pointer to a java char sequence

Definition at line 141 of file java_string_library_preprocess.cpp.

◆ is_java_char_sequence_type()

bool java_string_library_preprocesst::is_java_char_sequence_type ( const typet & type )

staticprivate

Parameters: type a type

Returns: Boolean telling whether the type is that of java char sequence

Definition at line 132 of file java_string_library_preprocess.cpp.

◆ is_java_string_buffer_pointer_type()

bool java_string_library_preprocesst::is_java_string_buffer_pointer_type ( const typet & type )

staticprivate

Parameters: type a type

Returns: Boolean telling whether the type is that of java StringBuffer pointers

Definition at line 118 of file java_string_library_preprocess.cpp.

◆ is_java_string_buffer_type()

bool java_string_library_preprocesst::is_java_string_buffer_type ( const typet & type )

staticprivate

Parameters: type a type

Returns: Boolean telling whether the type is that of java StringBuffer

Definition at line 109 of file java_string_library_preprocess.cpp.

◆ is_java_string_builder_pointer_type()

bool java_string_library_preprocesst::is_java_string_builder_pointer_type ( const typet & type )

staticprivate

Parameters: type a type

Returns: Boolean telling whether the type is that of java StringBuilder pointers

Definition at line 95 of file java_string_library_preprocess.cpp.

◆ is_java_string_builder_type()

bool java_string_library_preprocesst::is_java_string_builder_type ( const typet & type )

staticprivate

Parameters: type a type

Returns: Boolean telling whether the type is that of java StringBuilder

Definition at line 86 of file java_string_library_preprocess.cpp.

◆ is_java_string_pointer_type()

bool java_string_library_preprocesst::is_java_string_pointer_type ( const typet & type )

staticprivate

Parameters: type a type

Returns: Boolean telling whether the type is that of java string pointer

Definition at line 64 of file java_string_library_preprocess.cpp.

◆ is_java_string_type()

bool java_string_library_preprocesst::is_java_string_type ( const typet & type )

staticprivate

Parameters: type a type

Returns: Boolean telling whether the type is that of java string

Definition at line 78 of file java_string_library_preprocess.cpp.

◆ 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_name name of the class

Returns: True if the type is one that is known to our preprocessing, false otherwise

Definition at line 1505 of file java_string_library_preprocess.cpp.

◆ java_type_matches_tag()

bool java_string_library_preprocesst::java_type_matches_tag ( const typet & type,

const std::string & tag

)

staticprivate

Parameters: type a type

tag a 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 56 of file java_string_library_preprocess.cpp.

◆ make_assign_and_return_function_from_call()

code_blockt java_string_library_preprocesst::make_assign_and_return_function_from_call ( const irep_idt & function_id,

const java_method_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_id name of the function to be called

type the type of the function call

loc location in program

symbol_table the symbol table to populate

Returns: Code calling function with the given function name.

Definition at line 1122 of file java_string_library_preprocess.cpp.

◆ make_assign_function_from_call()

code_blockt java_string_library_preprocesst::make_assign_function_from_call ( const irep_idt & function_id,

const java_method_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_id name of the function to be called

type the type of the function call

loc location in program

symbol_table the symbol table to populate

Returns: Code assigning result of a call to the function with given function name.

Definition at line 1147 of file java_string_library_preprocess.cpp.

◆ make_class_identifier_code()

code_blockt java_string_library_preprocesst::make_class_identifier_code ( const java_method_typet & type,

const source_locationt & loc,

const irep_idt & function_id,

symbol_table_baset & symbol_table,

message_handlert & message_handler

)

private

Used to provide our own implementation of the CProver.classIdentifier() function.

Parameters: type type of the function called

loc location in the source

function_id function the generated code will be added to

symbol_table the symbol table

message_handler a message handler

Returns: Code corresponding to
string_expr1 = substr(obj->@class_identifier, 6)

return string_expr1;

Definition at line 1171 of file java_string_library_preprocess.cpp.

◆ make_copy_constructor_code()

code_blockt java_string_library_preprocesst::make_copy_constructor_code ( const java_method_typet & type,

const source_locationt & loc,

const irep_idt & function_id,

symbol_table_baset & symbol_table,

message_handlert & message_handler

)

private

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

Parameters: type type of the function

loc location in the source

function_id name of the function (used for variable naming) where the generated code ends up.

symbol_table symbol table

message_handler a message handler

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 1356 of file java_string_library_preprocess.cpp.

◆ make_copy_string_code()

code_blockt java_string_library_preprocesst::make_copy_string_code ( const java_method_typet & type,

const source_locationt & loc,

const irep_idt & function_id,

symbol_table_baset & symbol_table,

message_handlert & message_handler

)

private

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

Parameters: type type of the function

loc location in the source

function_id function the generated code will be added to

symbol_table symbol table

message_handler a message handler

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 1306 of file java_string_library_preprocess.cpp.

◆ make_float_to_string_code()

code_blockt java_string_library_preprocesst::make_float_to_string_code ( const java_method_typet & type,

const source_locationt & loc,

const irep_idt & function_id,

symbol_table_baset & symbol_table,

message_handlert & message_handler

)

private

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

Parameters: type type of the function call

loc location in the program_invocation_name

function_id function the generated code will be added to

symbol_table symbol table

message_handler a message handler

Returns: Code corresponding to the Java conversion of floats to strings.

Definition at line 917 of file java_string_library_preprocess.cpp.

◆ make_function_from_call()

code_blockt java_string_library_preprocesst::make_function_from_call ( const irep_idt & function_id,

const java_method_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_id name of the function to be called

type type of the function

loc location in the source

symbol_table symbol table

Returns: Code corresponding to:
return function_id(args)

Definition at line 1231 of file java_string_library_preprocess.cpp.

◆ make_init_function_from_call()

code_blockt java_string_library_preprocesst::make_init_function_from_call ( const irep_idt & function_id,

const java_method_typet & type,

const source_locationt & loc,

symbol_table_baset & symbol_table,

bool is_constructor = true

)

private

Generate the goto code for string initialization.

Parameters: function_id name of the function to be called

type the type of the function call

loc location in program

symbol_table the symbol table to populate

is_constructor the function being made is a constructor, so the whole object should be initialised, not just its length and data fields.

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 1078 of file java_string_library_preprocess.cpp.

◆ 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: loc a location in the program

function_id name of the function containing the string

symbol_table symbol table

code code block to which allocation instruction will be added

Returns: a new string_expr

Definition at line 512 of file java_string_library_preprocess.cpp.

◆ make_string_length_code()

code_returnt java_string_library_preprocesst::make_string_length_code ( const java_method_typet & type,

const source_locationt & loc,

const irep_idt & function_id,

symbol_table_baset & symbol_table,

message_handlert & message_handler

)

private

Generates code for the String.length method.

Parameters: type type of the function

loc location in the source

function_id unused

symbol_table symbol table

message_handler a message handler

Returns: Code corresponding to:
str_expr = java_string_to_string_expr(this)

str_expr_sym = str_expr

return this->length

Definition at line 1401 of file java_string_library_preprocess.cpp.

◆ make_string_returning_function_from_call()

code_blockt java_string_library_preprocesst::make_string_returning_function_from_call ( const irep_idt & function_id,

const java_method_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_id name of the function to be called

type type of the function

loc location in the source

symbol_table symbol table

Returns: Code corresponding to:
string_expr = function_id(args)

string = new String

string = string_expr_to_string(string)

return string

Definition at line 1261 of file java_string_library_preprocess.cpp.

◆ process_operands()

exprt::operandst java_string_library_preprocesst::process_operands ( const exprt::operandst & operands,

const source_locationt & loc,

const irep_idt & function_id,

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, replace the expression by this cprover_string in the output list, and add an assumption that the object is not null; in the other case the expression is kept as is for the output list.

Also does the same thing for char array references.

Parameters: operands a list of expressions

loc location in the source

function_id name of the function in which the code will be added

symbol_table symbol table

init_code code block, in which declaration of some arguments may be added

Returns: a list of expressions

Definition at line 337 of file java_string_library_preprocess.cpp.

◆ process_parameters()

exprt::operandst java_string_library_preprocesst::process_parameters ( const java_method_typet::parameterst & params,

const source_locationt & loc,

const irep_idt & function_id,

symbol_table_baset & symbol_table,

code_blockt & init_code

)

private

calls string_refine_preprocesst::process_operands with a list of parameters.

Parameters: params a list of function parameters

loc location in the source

function_id name of the function in which the code will be added

symbol_table symbol table

init_code code block, in which declaration of some arguments may be added

Returns: a list of expressions

Definition at line 280 of file java_string_library_preprocess.cpp.

◆ replace_char_array()

refined_string_exprt java_string_library_preprocesst::replace_char_array ( const exprt & array_pointer,

const source_locationt & loc,

const irep_idt & function_id,

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_pointer an expression of type char array pointer

loc location in the source

function_id name of the function in which the string is defined

symbol_table symbol table

code code block, in which some assignments will be added

Returns: a string expression

Definition at line 431 of file java_string_library_preprocess.cpp.

◆ replace_character_call()

codet java_string_library_preprocesst::replace_character_call ( code_function_callt call )

inline

Definition at line 58 of file java_string_library_preprocess.h.

◆ string_expr_of_function()

refined_string_exprt java_string_library_preprocesst::string_expr_of_function ( const irep_idt & function_id,

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_id.

In the arguments of the primitive str takes the place of the result and the following arguments are given by parameter arguments. \param function_id: the name of the function \param arguments: arguments of the function \param loc: source location \param symbol_table: symbol table \param [out] code: gets added the following code: @icode int return_code; int str.length; char str.data[str.length] return_code = <function_id>(str.length, str.data, arguments) @endicode \return refined string expressionstr`

Definition at line 750 of file java_string_library_preprocess.cpp.

◆ 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: s the literal to be assigned

loc location in the source

symbol_table symbol table

[out] code gets added the following:
tmp_string = "<s>"

lhs = cprover_string_literal_func(tmp_string)

Returns: a new refined string

Definition at line 896 of file java_string_library_preprocess.cpp.

Friends And Related Symbol 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,

const irep_idt & function_id,

symbol_table_baset & symbol_table,

code_blockt & init_code

)

friend

Member Data Documentation

◆ char_type

const typet java_string_library_preprocesst::char_type

private

Definition at line 102 of file java_string_library_preprocess.h.

◆ character_preprocess

character_refine_preprocesst java_string_library_preprocesst::character_preprocess

private

Definition at line 100 of file java_string_library_preprocess.h.

◆ conversion_table

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

private

Definition at line 117 of file java_string_library_preprocess.h.

◆ cprover_equivalent_to_java_assign_and_return_function

id_mapt java_string_library_preprocesst::cprover_equivalent_to_java_assign_and_return_function

private

Definition at line 133 of file java_string_library_preprocess.h.

◆ cprover_equivalent_to_java_assign_function

id_mapt java_string_library_preprocesst::cprover_equivalent_to_java_assign_function

private

Definition at line 138 of file java_string_library_preprocess.h.

◆ cprover_equivalent_to_java_constructor

id_mapt java_string_library_preprocesst::cprover_equivalent_to_java_constructor

private

Definition at line 129 of file java_string_library_preprocess.h.

◆ cprover_equivalent_to_java_function

id_mapt java_string_library_preprocesst::cprover_equivalent_to_java_function

private

Definition at line 121 of file java_string_library_preprocess.h.

◆ cprover_equivalent_to_java_string_returning_function

id_mapt java_string_library_preprocesst::cprover_equivalent_to_java_string_returning_function

private

Definition at line 125 of file java_string_library_preprocess.h.

◆ id_maps

const std::array<id_mapt *, 5> java_string_library_preprocesst::id_maps

private

Initial value:

= std::array<id_mapt *, 5>

{

&cprover_equivalent_to_java_function,

&cprover_equivalent_to_java_string_returning_function,

&cprover_equivalent_to_java_constructor,

&cprover_equivalent_to_java_assign_and_return_function,

&cprover_equivalent_to_java_assign_function,

}

java_string_library_preprocesst::cprover_equivalent_to_java_string_returning_function

id_mapt cprover_equivalent_to_java_string_returning_function

Definition java_string_library_preprocess.h:125

java_string_library_preprocesst::cprover_equivalent_to_java_assign_and_return_function

id_mapt cprover_equivalent_to_java_assign_and_return_function

Definition java_string_library_preprocess.h:133

java_string_library_preprocesst::cprover_equivalent_to_java_function

id_mapt cprover_equivalent_to_java_function

Definition java_string_library_preprocess.h:121

java_string_library_preprocesst::cprover_equivalent_to_java_constructor

id_mapt cprover_equivalent_to_java_constructor

Definition java_string_library_preprocess.h:129

java_string_library_preprocesst::cprover_equivalent_to_java_assign_function

id_mapt cprover_equivalent_to_java_assign_function

Definition java_string_library_preprocess.h:138

Definition at line 140 of file java_string_library_preprocess.h.

◆ index_type

const typet java_string_library_preprocesst::index_type

private

Definition at line 103 of file java_string_library_preprocess.h.

◆ refined_string_type

const refined_string_typet java_string_library_preprocesst::refined_string_type

private

Definition at line 104 of file java_string_library_preprocess.h.

◆ string_types

std::unordered_set<irep_idt> java_string_library_preprocesst::string_types

private

Definition at line 152 of file java_string_library_preprocess.h.

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

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