cprover
|
#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 | |
static irep_idt | get_tag (const typet &type) |
static typet | string_length_type () |
static const typet & | get_data_type (const typet &type, const symbol_tablet &symbol_table) |
Finds the type of the data component. More... | |
static const 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... | |
static codet | make_allocate_code (const symbol_exprt &lhs, const exprt &size) |
Create code allocating object of size size and assigning it to lhs 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 706 of file java_string_library_preprocess.cpp.
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 741 of file java_string_library_preprocess.cpp.
void add_keys_to_container | ( | const TMap & | map, |
TContainer & | container | ||
) |
Definition at line 1772 of file java_string_library_preprocess.cpp.
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 672 of file java_string_library_preprocess.cpp.
|
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 591 of file java_string_library_preprocess.cpp.
|
static |
access data member
expr | an expression of structured type with data component |
symbol_table | symbol table |
Definition at line 434 of file java_string_library_preprocess.cpp.
|
static |
Finds the type of the data component.
type | a type containing a "data" component |
symbol_table | symbol table |
Definition at line 385 of file java_string_library_preprocess.cpp.
|
static |
access length member
expr | an expression of structured type with length component |
symbol_table | symbol table |
Definition at line 424 of file java_string_library_preprocess.cpp.
|
static |
Finds the type of the length component.
type | a type containing a "length" component |
symbol_table | symbol table |
Definition at line 405 of file java_string_library_preprocess.cpp.
Definition at line 36 of file java_string_library_preprocess.cpp.
|
static |
Create code allocating object of size size
and assigning it to lhs
lhs | : pointer which will be allocated |
size | : size of the object |
lhs
Definition at line 626 of file java_string_library_preprocess.cpp.
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 |
function_id | name of the function containing the array |
code | [out] : code block where the declaration gets added |
Definition at line 640 of file java_string_library_preprocess.cpp.
|
static |
Definition at line 172 of file java_string_library_preprocess.cpp.