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 "java_string_library_preprocess.h"
#include <util/arith_tools.h>
#include <util/bitvector_expr.h>
#include <util/c_types.h>
#include <util/expr_initializer.h>
#include <util/floatbv_expr.h>
#include <util/ieee_float.h>
#include <util/refined_string_type.h>
#include <util/std_code.h>
#include <util/string_expr.h>
#include <util/symbol_table_base.h>
#include <goto-programs/class_identifier.h>
#include <ansi-c/allocate_objects.h>
#include "java_types.h"
#include "java_utils.h"

+ 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 typet & get_data_type (const typet &type, const symbol_table_baset &symbol_table)

Finds the type of the data component.

static const typet & get_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.

template<typename TMap , typename TContainer >

void add_keys_to_container (const TMap &map, TContainer &container)

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_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: array infinite size character array expression

length integer expression

symbol_table the symbol table

loc source location

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

[out] code code 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: pointer a character pointer expression

length length of the character sequence pointed by pointer

char_range character 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_table the symbol table

loc source location

function_id the name of the function

[out] code code 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 1433 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: pointer a character pointer expression

array a character array expression

symbol_table the symbol table

loc source location

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

[out] code code 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: lhs an expression

function_id the name of the function

arguments a list of arguments

symbol_table a 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: expr an expression of structured type with data component

symbol_table symbol 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: type a type containing a "data" component

symbol_table symbol 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: expr an expression of structured type with length component

symbol_table symbol 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: type a type containing a "length" component

symbol_table symbol 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_table the symbol table

loc source location

function_id name of the function containing the array

[out] code code 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.