cprover
Loading...
Searching...
No Matches
java_string_library_preprocess.cpp File Reference

Java_string_libraries_preprocess, gives code for methods on strings of the java standard library. More...

+ Include dependency graph for java_string_library_preprocess.cpp:

Go to the source code of this file.

Functions

static irep_idt get_tag (const typet &type)
 
static typet string_length_type ()
 
static const typetget_data_type (const typet &type, const symbol_table_baset &symbol_table)
 Finds the type of the data component.
 
static const typetget_length_type (const typet &type, const symbol_table_baset &symbol_table)
 Finds the type of the length component.
 
static exprt get_length (const exprt &expr, const symbol_table_baset &symbol_table)
 access length member
 
static exprt get_data (const exprt &expr, const symbol_table_baset &symbol_table)
 access data member
 
static codet code_assign_function_application (const exprt &lhs, const irep_idt &function_id, const exprt::operandst &arguments, symbol_table_baset &symbol_table)
 assign the result of a function call
 
exprt make_nondet_infinite_char_array (symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
 Declare a fresh symbol of type array of character with infinite size.
 
void add_pointer_to_array_association (const exprt &pointer, const exprt &array, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
 Add a call to a primitive of the string solver, letting it know that pointer points to the first character of array.
 
void add_array_to_length_association (const exprt &array, const exprt &length, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
 Add a call to a primitive of the string solver, letting it know that the actual length of array is length.
 
void add_character_set_constraint (const exprt &pointer, const exprt &length, const irep_idt &char_range, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
 Add a call to a primitive of the string solver which ensures all characters belong to the character set.
 
copy_constructor_body add (code_assign_string_expr_to_java_string(arg_this, string_expr, symbol_table, true), loc)
 
template<typename TMap , typename TContainer >
void add_keys_to_container (const TMap &map, TContainer &container)
 

Variables

const symbol_exprt arg_this {params[0].get_identifier(), params[0].type()}
 Create a refined_string_exprt str whose content and length are fresh symbols, calls the string primitive with name function_id.
 
return copy_constructor_body
 

Detailed Description

Java_string_libraries_preprocess, gives code for methods on strings of the java standard library.

In particular methods from java.lang.String, java.lang.StringBuilder, java.lang.StringBuffer.

Definition in file java_string_library_preprocess.cpp.

Function Documentation

◆ add()

copy_constructor_body add ( code_assign_string_expr_to_java_string(arg_this, string_expr, symbol_table, true) ,
loc  )

◆ add_array_to_length_association()

void add_array_to_length_association ( const exprt & array,
const exprt & length,
symbol_table_baset & symbol_table,
const source_locationt & loc,
const irep_idt & function_id,
code_blockt & code )

Add a call to a primitive of the string solver, letting it know that the actual length of array is length.

Parameters
arrayinfinite size character array expression
lengthinteger expression
symbol_tablethe symbol table
locsource location
function_idname of the function in which the code will be added
[out]codecode block to which declaration and calls get added

Definition at line 678 of file java_string_library_preprocess.cpp.

◆ add_character_set_constraint()

void add_character_set_constraint ( const exprt & pointer,
const exprt & length,
const irep_idt & char_range,
symbol_table_baset & symbol_table,
const source_locationt & loc,
const irep_idt & function_id,
code_blockt & code )

Add a call to a primitive of the string solver which ensures all characters belong to the character set.

Parameters
pointera character pointer expression
lengthlength of the character sequence pointed by pointer
char_rangecharacter set given by a range expression consisting of two characters separated by an hyphen. For instance "a-z" denotes all lower case ascii letters.
symbol_tablethe symbol table
locsource location
function_idthe name of the function
[out]codecode block to which declaration and calls get added

Definition at line 710 of file java_string_library_preprocess.cpp.

◆ add_keys_to_container()

template<typename TMap , typename TContainer >
void add_keys_to_container ( const TMap & map,
TContainer & container )

Definition at line 1432 of file java_string_library_preprocess.cpp.

◆ add_pointer_to_array_association()

void add_pointer_to_array_association ( const exprt & pointer,
const exprt & array,
symbol_table_baset & symbol_table,
const source_locationt & loc,
const irep_idt & function_id,
code_blockt & code )

Add a call to a primitive of the string solver, letting it know that pointer points to the first character of array.

Parameters
pointera character pointer expression
arraya character array expression
symbol_tablethe symbol table
locsource location
function_idname of the function in which the code will be added
[out]codecode block to which declaration and calls get added

Definition at line 647 of file java_string_library_preprocess.cpp.

◆ code_assign_function_application()

static codet code_assign_function_application ( const exprt & lhs,
const irep_idt & function_id,
const exprt::operandst & arguments,
symbol_table_baset & symbol_table )
static

assign the result of a function call

Parameters
lhsan expression
function_idthe name of the function
argumentsa list of arguments
symbol_tablea symbol table
Returns
the following code:
lhs = <function_id>(arguments)

Definition at line 578 of file java_string_library_preprocess.cpp.

◆ get_data()

static exprt get_data ( const exprt & expr,
const symbol_table_baset & symbol_table )
static

access data member

Parameters
expran expression of structured type with data component
symbol_tablesymbol table
Returns
expression representing the "data" member

Definition at line 418 of file java_string_library_preprocess.cpp.

◆ get_data_type()

static const typet & get_data_type ( const typet & type,
const symbol_table_baset & symbol_table )
static

Finds the type of the data component.

Parameters
typea type containing a "data" component
symbol_tablesymbol table
Returns
type of the "data" component

Definition at line 368 of file java_string_library_preprocess.cpp.

◆ get_length()

static exprt get_length ( const exprt & expr,
const symbol_table_baset & symbol_table )
static

access length member

Parameters
expran expression of structured type with length component
symbol_tablesymbol table
Returns
expression representing the "length" member

Definition at line 408 of file java_string_library_preprocess.cpp.

◆ get_length_type()

static const typet & get_length_type ( const typet & type,
const symbol_table_baset & symbol_table )
static

Finds the type of the length component.

Parameters
typea type containing a "length" component
symbol_tablesymbol table
Returns
type of the "length" component

Definition at line 388 of file java_string_library_preprocess.cpp.

◆ get_tag()

static irep_idt get_tag ( const typet & type)
static
Returns
tag of a struct prefixed by "java::" or symbolic tag empty string if not symbol or struct

Definition at line 41 of file java_string_library_preprocess.cpp.

◆ make_nondet_infinite_char_array()

exprt make_nondet_infinite_char_array ( symbol_table_baset & symbol_table,
const source_locationt & loc,
const irep_idt & function_id,
code_blockt & code )

Declare a fresh symbol of type array of character with infinite size.

Parameters
symbol_tablethe symbol table
locsource location
function_idname of the function containing the array
[out]codecode block where the declaration gets added
Returns
created symbol expression

Definition at line 615 of file java_string_library_preprocess.cpp.

◆ string_length_type()

static typet string_length_type ( )
static
Returns
the type of the length field in java Strings.

Definition at line 177 of file java_string_library_preprocess.cpp.

Variable Documentation

◆ arg_this

const symbol_exprt arg_this {params[0].get_identifier(), params[0].type()}

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: / ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ / int return_code; / int str.length; / char str.data[str.length] / return_code = <function_id>(str.length, str.data, arguments) / ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ / \return refined string expressionstr` 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) { int return_code; const symbolt return_code_sym = fresh_java_symbol( java_int_type(), std::string("return_code_") + function_id.c_str(), loc, function_id, symbol_table); const auto return_code = return_code_sym.symbol_expr(); code.add(code_declt(return_code), loc);

const refined_string_exprt string_expr = make_nondet_string_expr(loc, function_id, symbol_table, code);

args is { str.length, str.content, arguments... } exprt::operandst args; args.push_back(string_expr.length()); args.push_back(string_expr.content()); args.insert(args.end(), arguments.begin(), arguments.end());

return_code = <function_id>_data(args) code.add( code_assign_function_application( return_code, function_id, args, symbol_table), loc);

return string_expr; }

/ 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 /
is_constructorthe 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 } / ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 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) { PRECONDITION(implements_java_char_sequence_pointer(lhs.type())); dereference_exprt deref = checked_dereference(lhs);

if(is_constructor) { Initialise the supertype with the appropriate classid: namespacet ns(symbol_table); const struct_typet &lhs_type = ns.follow_tag(to_struct_tag_type(deref.type())); auto zero_base_object = *zero_initializer( lhs_type.components().front().type(), source_locationt{}, ns); set_class_identifier( to_struct_expr(zero_base_object), ns, to_struct_tag_type(deref.type())); struct_exprt struct_rhs( {zero_base_object, rhs_length, rhs_array}, deref.type()); return code_assignt(checked_dereference(lhs), struct_rhs); } else { return code_blockt( {code_assignt(get_length(deref, symbol_table), rhs_length), code_assignt(get_data(deref, symbol_table), rhs_array)}); } }

/ 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 /
is_constructorthe 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 } / ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 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) { return code_assign_components_to_java_string( lhs, rhs.content(), rhs.length(), symbol_table, is_constructor); }

/

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 / ~~~~~~~~~~~~~~~~~~~~~~ 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) { PRECONDITION(implements_java_char_sequence_pointer(rhs.type()));

const dereference_exprt deref = checked_dereference(rhs);

Although we should not reach this code if rhs is null, the association pointer -> length is added to the solver anyway, so we have to make sure the length is set to something reasonable. auto rhs_length = if_exprt( equal_exprt(rhs, null_pointer_exprt(to_pointer_type(rhs.type()))), from_integer(0, lhs.length().type()), get_length(deref, symbol_table)); rhs_length.set(ID_mode, ID_java);

Assignments code.add(code_assignt(lhs.length(), rhs_length), loc); exprt data_as_array = get_data(deref, symbol_table); code.add(code_assignt{lhs.content(), std::move(data_as_array)}, loc); }

/ 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 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) { return string_expr_of_function( ID_cprover_string_literal_func, {constant_exprt{s, string_typet{}}}, loc, symbol_table, code); }

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

Parameters
typetype of the function call /
loclocation in the program_invocation_name /
function_idfunction the generated code will be added to /
symbol_tablesymbol table /
message_handlera message handler /
Returns
Code corresponding to the Java conversion of floats to strings. 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) { (void)message_handler;

Getting the argument java_method_typet::parameterst params = type.parameters(); PRECONDITION(params.size()==1); PRECONDITION(!params[0].get_identifier().empty()); const symbol_exprt arg(params[0].get_identifier(), params[0].type());

Holder for output code code_blockt code;

Declaring and allocating String * str const exprt str = allocate_fresh_string( type.return_type(), loc, function_id, symbol_table, code);

Expression representing 0.0 const ieee_float_spect float_spec{to_floatbv_type(params[0].type())}; ieee_floatt zero_float(float_spec); zero_float.from_float(0.0); const constant_exprt zero = zero_float.to_expr();

For each possible case with have a condition and a string_exprt std::vector<exprt> condition_list; std::vector<refined_string_exprt> string_expr_list;

Case of computerized scientific notation condition_list.push_back(binary_relation_exprt(arg, ID_ge, zero)); const refined_string_exprt sci_notation = string_expr_of_function( ID_cprover_string_of_float_scientific_notation_func, {arg}, loc, symbol_table, code); string_expr_list.push_back(sci_notation);

Subcase of negative scientific notation condition_list.push_back(binary_relation_exprt(arg, ID_lt, zero)); const refined_string_exprt minus_sign = string_literal_to_string_expr("-", loc, symbol_table, code); const refined_string_exprt neg_sci_notation = string_expr_of_function( ID_cprover_string_concat_func, {minus_sign, sci_notation}, loc, symbol_table, code); string_expr_list.push_back(neg_sci_notation);

Case of NaN condition_list.push_back(isnan_exprt(arg)); const refined_string_exprt nan = string_literal_to_string_expr("NaN", loc, symbol_table, code); string_expr_list.push_back(nan);

Case of Infinity extractbit_exprt is_neg(arg, float_spec.width()-1); condition_list.push_back(and_exprt(isinf_exprt(arg), not_exprt(is_neg))); const refined_string_exprt infinity = string_literal_to_string_expr("Infinity", loc, symbol_table, code); string_expr_list.push_back(infinity);

Case -Infinity condition_list.push_back(and_exprt(isinf_exprt(arg), is_neg)); const refined_string_exprt minus_infinity = string_literal_to_string_expr("-Infinity", loc, symbol_table, code); string_expr_list.push_back(minus_infinity);

Case of 0.0 Note: for zeros we must use equal_exprt and not ieee_float_equal_exprt, the latter disregards the sign condition_list.push_back(equal_exprt(arg, zero)); const refined_string_exprt zero_string = string_literal_to_string_expr("0.0", loc, symbol_table, code); string_expr_list.push_back(zero_string);

Case of -0.0 ieee_floatt minus_zero_float(float_spec); minus_zero_float.from_float(-0.0f); condition_list.push_back(equal_exprt(arg, minus_zero_float.to_expr())); const refined_string_exprt minus_zero_string = string_literal_to_string_expr("-0.0", loc, symbol_table, code); string_expr_list.push_back(minus_zero_string);

Case of simple notation ieee_floatt bound_inf_float(float_spec); ieee_floatt bound_sup_float(float_spec); bound_inf_float.from_float(1e-3f); bound_sup_float.from_float(1e7f); bound_inf_float.change_spec(float_spec); bound_sup_float.change_spec(float_spec); const constant_exprt bound_inf = bound_inf_float.to_expr(); const constant_exprt bound_sup = bound_sup_float.to_expr();

const and_exprt is_simple_float{binary_relation_exprt(arg, ID_ge, bound_inf), binary_relation_exprt(arg, ID_lt, bound_sup)}; condition_list.push_back(is_simple_float);

const refined_string_exprt simple_notation = string_expr_of_function( ID_cprover_string_of_float_func, {arg}, loc, symbol_table, code); string_expr_list.push_back(simple_notation);

Case of a negative number in simple notation const and_exprt is_neg_simple_float{ binary_relation_exprt(arg, ID_le, unary_minus_exprt(bound_inf)), binary_relation_exprt(arg, ID_gt, unary_minus_exprt(bound_sup))}; condition_list.push_back(is_neg_simple_float);

const refined_string_exprt neg_simple_notation = string_expr_of_function( ID_cprover_string_concat_func, {minus_sign, simple_notation}, loc, symbol_table, code); string_expr_list.push_back(neg_simple_notation);

Combining all cases INVARIANT( string_expr_list.size()==condition_list.size(), "number of created strings should correspond to number of conditions");

We do not check the condition of the first element in the list as it will be reached only if all other conditions are not satisfied. codet tmp_code = code_assign_string_expr_to_java_string( str, string_expr_list[0], symbol_table, true); for(std::size_t i=1; i<condition_list.size(); i++) { tmp_code = code_ifthenelset( condition_list[i], code_assign_string_expr_to_java_string( str, string_expr_list[i], symbol_table, true), tmp_code); } code.add(tmp_code, loc);

Return str code.add(code_returnt(str), loc); return code; }

/ Generate the goto code for string initialization. /

Parameters
function_idname of the function to be called /
typethe type of the function call /
loclocation in program /
symbol_tablethe symbol table to populate /
is_constructorthe 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}; / 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) { java_method_typet::parameterst params = type.parameters();

The first parameter is the object to be initialized PRECONDITION(!params.empty()); PRECONDITION(!params[0].get_identifier().empty()); const symbol_exprt arg_this(params[0].get_identifier(), params[0].type()); if(is_constructor) params.erase(params.begin());

Holder for output code code_blockt code;

Processing parameters const exprt::operandst args = process_parameters(params, loc, function_id, symbol_table, code);

string_expr <- function(arg1) const refined_string_exprt string_expr = string_expr_of_function(function_id, args, loc, symbol_table, code);

arg_this <- string_expr code.add( code_assign_string_expr_to_java_string( arg_this, string_expr, symbol_table, is_constructor), loc);

return code; }

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

Parameters
function_idname 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. 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) { This is similar to assign functions except we return a pointer to this const java_method_typet::parameterst &params = type.parameters(); PRECONDITION(!params.empty()); PRECONDITION(!params[0].get_identifier().empty()); code_blockt code; code.add( make_assign_function_from_call(function_id, type, loc, symbol_table), loc); const symbol_exprt arg_this(params[0].get_identifier(), params[0].type()); code.add(code_returnt(arg_this), loc); return code; }

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

Parameters
function_idname 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. 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) { This is similar to initialization function except we do not ignore the first argument return make_init_function_from_call( function_id, type, loc, symbol_table, false); }

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

Parameters
typetype of the function called /
loclocation in the source /
function_idfunction the generated code will be added to /
symbol_tablethe symbol table /
message_handlera message handler /
Returns
Code corresponding to / ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ / string_expr1 = substr(obj->@class_identifier, 6) / return string_expr1; / ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 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) { java_method_typet::parameterst params = type.parameters(); PRECONDITION(!params.empty()); PRECONDITION(!params[0].get_identifier().empty()); const symbol_exprt obj(params[0].get_identifier(), params[0].type());

Code to be returned code_blockt code;

class_identifier is obj->@class_identifier const member_exprt class_identifier{ checked_dereference(obj), JAVA_CLASS_IDENTIFIER_FIELD_NAME, string_typet()};

string_expr = cprover_string_literal(this->@class_identifier) const refined_string_exprt string_expr = string_expr_of_function( ID_cprover_string_literal_func, {class_identifier}, loc, symbol_table, code);

string_expr1 = substr(string_expr, 6) We do this to remove the "java::" prefix const refined_string_exprt string_expr1 = string_expr_of_function( ID_cprover_string_substring_func, {string_expr, from_integer(6, java_int_type())}, loc, symbol_table, code);

string1 = (String*) string_expr const typet &string_ptr_type = type.return_type(); const exprt string1 = allocate_fresh_string( string_ptr_type, loc, function_id, symbol_table, code); code.add( code_assign_string_expr_to_java_string( string1, string_expr1, symbol_table, true), loc);

‍return string1; code.add(code_returnt{string1}, loc); return code; }

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

Parameters
function_idname of the function to be called /
typetype of the function /
loclocation in the source /
symbol_tablesymbol table /
Returns
Code corresponding to: / ~~~~~~~~~~~~~~~~~~~~~~~~~~ / return function_id(args) / ~~~~~~~~~~~~~~~~~~~~~~~~~~ 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) { code_blockt code; const exprt::operandst args = process_parameters(type.parameters(), loc, function_id, symbol_table, code); code.add( code_return_function_application( function_id, args, type.return_type(), symbol_table), loc); return code; }

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

Parameters
function_idname of the function to be called /
typetype of the function /
loclocation in the source /
symbol_tablesymbol table /
Returns
Code corresponding to: / ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ / string_expr = function_id(args) / string = new String / string = string_expr_to_string(string) / return string / ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 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) { Code for the output code_blockt code;

Calling the function const exprt::operandst arguments = process_parameters(type.parameters(), loc, function_id, symbol_table, code);

String expression that will hold the result const refined_string_exprt string_expr = string_expr_of_function(function_id, arguments, loc, symbol_table, code);

Assign to string const exprt str = allocate_fresh_string( type.return_type(), loc, function_id, symbol_table, code); code.add( code_assign_string_expr_to_java_string( str, string_expr, symbol_table, true), loc);

Return value code.add(code_returnt(str), loc); return code; }

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

Parameters
typetype of the function /
loclocation in the source /
function_idfunction the generated code will be added to /
symbol_tablesymbol table /
message_handlera 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 / ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 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) { (void)message_handler;

Code for the output code_blockt code;

String expression that will hold the result const refined_string_exprt string_expr = decl_string_expr(loc, function_id, symbol_table, code);

Assign the argument to string_expr const java_method_typet::parametert &op = type.parameters()[0]; PRECONDITION(!op.get_identifier().empty()); const symbol_exprt arg0{op.get_identifier(), op.type()}; code_assign_java_string_to_string_expr( string_expr, arg0, loc, symbol_table, code);

Allocate and assign the string const exprt str = allocate_fresh_string( type.return_type(), loc, function_id, symbol_table, code); code.add( code_assign_string_expr_to_java_string( str, string_expr, symbol_table, true), loc);

Return value code.add(code_returnt(str), loc); return code; }

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

Parameters
typetype of the function /
loclocation in the source /
function_idname of the function (used for variable naming) where / the generated code ends up. /
symbol_tablesymbol table /
message_handlera 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) / ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 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) { (void)message_handler;

code_blockt copy_constructor_body;

String expression that will hold the result const refined_string_exprt string_expr = decl_string_expr(loc, function_id, symbol_table, copy_constructor_body);

Assign argument to a string_expr const java_method_typet::parameterst &params = type.parameters(); PRECONDITION(!params[0].get_identifier().empty()); PRECONDITION(!params[1].get_identifier().empty()); const symbol_exprt arg1{params[1].get_identifier(), params[1].type()}; code_assign_java_string_to_string_expr( string_expr, arg1, loc, symbol_table, copy_constructor_body);

Assign string_expr to this object

Definition at line 1379 of file java_string_library_preprocess.cpp.

◆ copy_constructor_body

return copy_constructor_body

Definition at line 1385 of file java_string_library_preprocess.cpp.