cprover
|
Java_string_libraries_preprocess, gives code for methods on strings of the java standard library. More...
#include <util/arith_tools.h>
#include <util/std_expr.h>
#include <util/std_code.h>
#include <util/fresh_symbol.h>
#include <util/refined_string_type.h>
#include <util/string_expr.h>
#include <util/c_types.h>
#include "java_types.h"
#include "java_object_factory.h"
#include "java_utils.h"
#include "java_string_library_preprocess.h"
#include "java_root_class.h"
Go to the source code of this file.
Functions | |
irep_idt | get_tag (const typet &type) |
typet | string_data_type (const symbol_tablet &symbol_table) |
typet | string_length_type () |
static typet | get_data_type (const typet &type, const symbol_tablet &symbol_table) |
Finds the type of the data component. More... | |
static typet | get_length_type (const typet &type, const symbol_tablet &symbol_table) |
Finds the type of the length component. More... | |
static exprt | get_length (const exprt &expr, const symbol_tablet &symbol_table) |
access length member More... | |
static exprt | get_data (const exprt &expr, const symbol_tablet &symbol_table) |
access data member More... | |
static codet | code_assign_function_application (const exprt &lhs, const irep_idt &function_name, const exprt::operandst &arguments, symbol_table_baset &symbol_table) |
assign the result of a function call More... | |
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. More... | |
void | add_pointer_to_array_association (const exprt &pointer, const exprt &array, symbol_table_baset &symbol_table, const source_locationt &loc, 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 . More... | |
void | add_array_to_length_association (const exprt &array, const exprt &length, symbol_table_baset &symbol_table, const source_locationt &loc, code_blockt &code) |
Add a call to a primitive of the string solver, letting it know that the actual length of array is length . More... | |
void | add_character_set_constraint (const exprt &pointer, const exprt &length, const irep_idt &char_set, symbol_table_baset &symbol_table, const source_locationt &loc, code_blockt &code) |
Add a call to a primitive of the string solver which ensures all characters belong to the character set. More... | |
template<typename TMap , typename TContainer > | |
void | add_keys_to_container (const TMap &map, TContainer &container) |
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.
void add_array_to_length_association | ( | const exprt & | array, |
const exprt & | length, | ||
symbol_table_baset & | symbol_table, | ||
const source_locationt & | loc, | ||
code_blockt & | code | ||
) |
Add a call to a primitive of the string solver, letting it know that the actual length of array
is length
.
array | infinite size character array expression |
length | integer expression |
symbol_table | the symbol table |
loc | source location |
code | [out] : code block to which declaration and calls get added |
Definition at line 715 of file java_string_library_preprocess.cpp.
References code_blockt::add(), code_assign_function_application(), get_fresh_aux_symbol(), java_int_type(), loc, and symbolt::symbol_expr().
Referenced by initialize_nondet_string_struct(), and java_string_library_preprocesst::make_nondet_string_expr().
void add_character_set_constraint | ( | const exprt & | pointer, |
const exprt & | length, | ||
const irep_idt & | char_set, | ||
symbol_table_baset & | symbol_table, | ||
const source_locationt & | loc, | ||
code_blockt & | code | ||
) |
Add a call to a primitive of the string solver which ensures all characters belong to the character set.
pointer | a character pointer expression |
length | length of the character sequence pointed by pointer |
char_set | 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 |
code | [out] : code block to which declaration and calls get added |
Definition at line 750 of file java_string_library_preprocess.cpp.
References code_blockt::add(), code_assign_function_application(), get_fresh_aux_symbol(), irept::id(), java_int_type(), loc, PRECONDITION, and exprt::type().
Referenced by initialize_nondet_string_struct().
void add_keys_to_container | ( | const TMap & | map, |
TContainer & | container | ||
) |
Definition at line 1852 of file java_string_library_preprocess.cpp.
Referenced by java_string_library_preprocesst::get_all_function_names().
void add_pointer_to_array_association | ( | const exprt & | pointer, |
const exprt & | array, | ||
symbol_table_baset & | symbol_table, | ||
const source_locationt & | loc, | ||
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
.
pointer | a character pointer expression |
array | a character array expression |
symbol_table | the symbol table |
loc | source location |
code | [out] : code block to which declaration and calls get added |
Definition at line 681 of file java_string_library_preprocess.cpp.
References code_blockt::add(), code_assign_function_application(), get_fresh_aux_symbol(), irept::id(), java_int_type(), loc, PRECONDITION, and exprt::type().
Referenced by initialize_nondet_string_struct(), java_string_library_preprocesst::make_nondet_string_expr(), and java_string_library_preprocesst::replace_char_array().
|
static |
assign the result of a function call
lhs | an expression |
function_name | the name of the function |
arguments | a list of arguments |
symbol_table | a symbol table |
Definition at line 616 of file java_string_library_preprocess.cpp.
References make_function_application(), and exprt::type().
Referenced by add_array_to_length_association(), add_character_set_constraint(), add_pointer_to_array_association(), and java_string_library_preprocesst::string_expr_of_function().
|
static |
access data member
expr | an expression of structured type with data component |
symbol_table | symbol table |
Definition at line 441 of file java_string_library_preprocess.cpp.
References get_data_type(), and exprt::type().
Referenced by java_string_library_preprocesst::code_assign_java_string_to_string_expr(), and java_string_library_preprocesst::replace_char_array().
|
static |
Finds the type of the data component.
type | a type containing a "data" component |
symbol_table | symbol table |
Definition at line 394 of file java_string_library_preprocess.cpp.
References CHECK_RETURN, struct_union_typet::component_type(), irept::id(), symbol_table_baset::lookup(), PRECONDITION, to_struct_type(), to_symbol_type(), and symbolt::type.
Referenced by get_data().
|
static |
access length member
expr | an expression of structured type with length component |
symbol_table | symbol table |
Definition at line 431 of file java_string_library_preprocess.cpp.
References get_length_type(), and exprt::type().
Referenced by java_string_library_preprocesst::code_assign_java_string_to_string_expr(), java_string_library_preprocesst::make_string_length_code(), and java_string_library_preprocesst::replace_char_array().
|
static |
Finds the type of the length component.
type | a type containing a "length" component |
symbol_table | symbol table |
Definition at line 413 of file java_string_library_preprocess.cpp.
References CHECK_RETURN, struct_union_typet::component_type(), irept::id(), symbol_table_baset::lookup(), PRECONDITION, to_struct_type(), to_symbol_type(), and symbolt::type.
Referenced by get_length().
Definition at line 36 of file java_string_library_preprocess.cpp.
References symbol_typet::get_identifier(), irept::id(), id2string(), to_struct_type(), and to_symbol_type().
Referenced by java_string_library_preprocesst::code_assign_components_to_java_string(), java_object_factoryt::gen_pointer_target_init(), remove_exceptionst::instrument_exceptions(), java_is_array_type(), and java_string_library_preprocesst::java_type_matches_tag().
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.
symbol_table | the symbol table |
loc | source location |
code | [out] : code block where the declaration gets added |
Definition at line 652 of file java_string_library_preprocess.cpp.
References code_blockt::add(), get_fresh_aux_symbol(), java_char_type(), java_int_type(), loc, symbolt::symbol_expr(), and exprt::type().
Referenced by initialize_nondet_string_struct(), and java_string_library_preprocesst::make_nondet_string_expr().
typet string_data_type | ( | const symbol_tablet & | symbol_table | ) |
symbol_table | a symbol_table containing an entry for java Strings |
Definition at line 173 of file java_string_library_preprocess.cpp.
References struct_union_typet::component_number(), struct_union_typet::components(), symbol_table_baset::lookup(), to_struct_type(), and symbolt::type.
typet string_length_type | ( | ) |
Definition at line 184 of file java_string_library_preprocess.cpp.
References java_int_type().
Referenced by java_string_library_preprocesst::add_string_type().