cprover
java_string_library_preprocess.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Produce code for simple implementation of String Java libraries
4 
5 Author: Romain Brenguier
6 
7 Date: March 2017
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_JAVA_BYTECODE_JAVA_STRING_LIBRARY_PREPROCESS_H
15 #define CPROVER_JAVA_BYTECODE_JAVA_STRING_LIBRARY_PREPROCESS_H
16 
17 #include <util/ui_message.h>
18 #include <util/std_code.h>
19 #include <util/symbol_table.h>
21 #include <util/string_expr.h>
22 
23 #include <util/ieee_float.h> // should get rid of this
24 #include <util/optional.h>
25 
26 #include <array>
27 #include <unordered_set>
28 #include <functional>
30 #include "java_types.h"
31 
32 // Arbitrary limit of 10 arguments for the number of arguments to String.format
33 #define MAX_FORMAT_ARGS 10
34 
36 {
37 public:
42  {
43  }
44 
47 
48  bool implements_function(const irep_idt &function_id) const;
49  void get_all_function_names(std::unordered_set<irep_idt> &methods) const;
50 
51  codet
52  code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table);
53 
55  {
57  }
58  std::vector<irep_idt> get_string_type_base_classes(
59  const irep_idt &class_name);
60  void add_string_type(const irep_idt &class_name, symbol_tablet &symbol_table);
61  bool is_known_string_type(irep_idt class_name);
62 
64  {
69  }
70  static bool implements_java_char_sequence(const typet &type)
71  {
72  return is_java_char_sequence_type(type)
75  || is_java_string_type(type);
76  }
77 
78 private:
79  // We forbid copies of the object
81  const java_string_library_preprocesst &)=delete;
82 
83  static bool java_type_matches_tag(const typet &type, const std::string &tag);
84  static bool is_java_string_pointer_type(const typet &type);
85  static bool is_java_string_type(const typet &type);
86  static bool is_java_string_builder_type(const typet &type);
87  static bool is_java_string_builder_pointer_type(const typet &type);
88  static bool is_java_string_buffer_type(const typet &type);
89  static bool is_java_string_buffer_pointer_type(const typet &type);
90  static bool is_java_char_sequence_type(const typet &type);
91  static bool is_java_char_sequence_pointer_type(const typet &type);
92  static bool is_java_char_array_type(const typet &type);
93  static bool is_java_char_array_pointer_type(const typet &type);
94 
96 
100 
101  typedef std::function<codet(
102  const java_method_typet &,
103  const source_locationt &,
104  const irep_idt &,
107 
108  typedef std::unordered_map<irep_idt, irep_idt> id_mapt;
109 
110  // Table mapping each java method signature to the code generating function
111  std::unordered_map<irep_idt, conversion_functiont> conversion_table;
112 
113  // Some Java functions have an equivalent in the solver that we will
114  // call with the same argument and will return the same result
116 
117  // Some Java functions have an equivalent except that they should
118  // return Java Strings instead of string_exprt
120 
121  // Some Java initialization function initialize strings with the
122  // same result as some function of the solver
124 
125  // Some Java functions have an equivalent in the solver except that
126  // in addition they assign the result to the object on which it is called
128 
129  // Some Java functions have an equivalent in the solver except that
130  // they assign the result to the object on which it is called instead
131  // of returning it
133 
134  const std::array<id_mapt *, 5> id_maps = std::array<id_mapt *, 5>
135  {
136  {
142  }
143  };
144 
145  // A set tells us what java types should be considered as string objects
146  std::unordered_set<irep_idt> string_types;
147 
149  const java_method_typet &type,
150  const source_locationt &loc,
151  const irep_idt &function_id,
152  symbol_table_baset &symbol_table);
153 
155  const java_method_typet &type,
156  const source_locationt &loc,
157  const irep_idt &function_id,
158  symbol_table_baset &symbol_table);
159 
161  const java_method_typet &type,
162  const source_locationt &loc,
163  const irep_idt &function_id,
164  symbol_table_baset &symbol_table);
165 
167  const java_method_typet &type,
168  const source_locationt &loc,
169  const irep_idt &function_id,
170  symbol_table_baset &symbol_table);
171 
173  const java_method_typet &type,
174  const source_locationt &loc,
175  const irep_idt &function_id,
176  symbol_table_baset &symbol_table);
177 
178  // Helper functions
180  const java_method_typet::parameterst &params,
181  const source_locationt &loc,
182  const irep_idt &function_name,
183  symbol_table_baset &symbol_table,
184  code_blockt &init_code);
185 
186  // Friending this function for unit testing convert_exprt_to_string_exprt
189  const exprt &deref,
190  const source_locationt &loc,
191  const irep_idt &function_id,
192  symbol_tablet &symbol_table,
193  code_blockt &init_code);
194 
196  const exprt &deref,
197  const source_locationt &loc,
198  symbol_table_baset &symbol_table,
199  const irep_idt &function_name,
200  code_blockt &init_code);
201 
203  const exprt::operandst &operands,
204  const source_locationt &loc,
205  const irep_idt &function_name,
206  symbol_table_baset &symbol_table,
207  code_blockt &init_code);
208 
210  const exprt &array_pointer,
211  const source_locationt &loc,
212  const irep_idt &function_name,
213  symbol_table_baset &symbol_table,
214  code_blockt &code);
215 
217  const typet &type,
218  const source_locationt &loc,
219  const irep_idt &function_id,
220  symbol_table_baset &symbol_table);
221 
223  const source_locationt &loc,
224  const irep_idt &function_id,
225  symbol_table_baset &symbol_table,
226  code_blockt &code);
227 
229  const source_locationt &loc,
230  const irep_idt &function_id,
231  symbol_table_baset &symbol_table,
232  code_blockt &code);
233 
235  const typet &type,
236  const source_locationt &loc,
237  const irep_idt &function_id,
238  symbol_table_baset &symbol_table,
239  code_blockt &code);
240 
242  const irep_idt &function_id,
243  const exprt::operandst &arguments,
244  const typet &type,
245  symbol_table_baset &symbol_table);
246 
248  const irep_idt &function_id,
249  const exprt::operandst &arguments,
250  const source_locationt &loc,
251  symbol_table_baset &symbol_table,
252  code_blockt &code);
253 
255  const exprt &lhs,
256  const exprt &rhs_array,
257  const exprt &rhs_length,
258  const symbol_table_baset &symbol_table,
259  bool is_constructor);
260 
262  const exprt &lhs,
263  const refined_string_exprt &rhs,
264  const symbol_table_baset &symbol_table,
265  bool is_constructor);
266 
268  const refined_string_exprt &lhs,
269  const exprt &rhs,
270  const source_locationt &loc,
271  const symbol_table_baset &symbol_table,
272  code_blockt &code);
273 
275  const std::string &s,
276  const source_locationt &loc,
277  symbol_table_baset &symbol_table,
278  code_blockt &code);
279 
281  const irep_idt &function_id,
282  const java_method_typet &type,
283  const source_locationt &loc,
284  symbol_table_baset &symbol_table);
285 
287  const irep_idt &function_id,
288  const java_method_typet &type,
289  const source_locationt &loc,
290  symbol_table_baset &symbol_table,
291  bool is_constructor = true);
292 
294  const irep_idt &function_id,
295  const java_method_typet &type,
296  const source_locationt &loc,
297  symbol_table_baset &symbol_table);
298 
300  const irep_idt &function_id,
301  const java_method_typet &type,
302  const source_locationt &loc,
303  symbol_table_baset &symbol_table);
304 
306  const irep_idt &function_id,
307  const java_method_typet &type,
308  const source_locationt &loc,
309  symbol_table_baset &symbol_table);
310 };
311 
313  symbol_table_baset &symbol_table,
314  const source_locationt &loc,
315  const irep_idt &function_id,
316  code_blockt &code);
317 
319  const exprt &pointer,
320  const exprt &array,
321  symbol_table_baset &symbol_table,
322  const source_locationt &loc,
323  const irep_idt &function_id,
324  code_blockt &code);
325 
327  const exprt &array,
328  const exprt &length,
329  symbol_table_baset &symbol_table,
330  const source_locationt &loc,
331  const irep_idt &function_id,
332  code_blockt &code);
333 
335  const exprt &pointer,
336  const exprt &length,
337  const irep_idt &char_range,
338  symbol_table_baset &symbol_table,
339  const source_locationt &loc,
340  const irep_idt &function_id,
341  code_blockt &code);
342 
343 #endif // CPROVER_JAVA_BYTECODE_JAVA_STRING_LIBRARY_PREPROCESS_H
java_string_library_preprocesst::convert_exprt_to_string_exprt
refined_string_exprt convert_exprt_to_string_exprt(const exprt &deref, const source_locationt &loc, symbol_table_baset &symbol_table, const irep_idt &function_name, code_blockt &init_code)
Creates a string_exprt from the input exprt representing a char sequence.
Definition: java_string_library_preprocess.cpp:308
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
java_string_library_preprocesst::replace_char_array
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.
Definition: java_string_library_preprocess.cpp:429
java_string_library_preprocesst::char_type
const typet char_type
Definition: java_string_library_preprocess.h:97
java_string_library_preprocesst::process_parameters
exprt::operandst process_parameters(const java_method_typet::parameterst &params, const source_locationt &loc, const irep_idt &function_name, symbol_table_baset &symbol_table, code_blockt &init_code)
calls string_refine_preprocesst::process_operands with a list of parameters.
Definition: java_string_library_preprocess.cpp:279
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
java_string_library_preprocesst::make_copy_string_code
code_blockt make_copy_string_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Generates code for a function which copies a string object to a new string object.
Definition: java_string_library_preprocess.cpp:1294
java_string_library_preprocesst::make_string_length_code
code_returnt make_string_length_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Generates code for the String.length method.
Definition: java_string_library_preprocess.cpp:1381
java_string_library_preprocesst::id_mapt
std::unordered_map< irep_idt, irep_idt > id_mapt
Definition: java_string_library_preprocess.h:108
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:127
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
java_string_library_preprocesst::java_string_library_preprocesst
java_string_library_preprocesst()
Definition: java_string_library_preprocess.h:38
java_string_library_preprocesst::index_type
const typet index_type
Definition: java_string_library_preprocess.h:98
java_string_library_preprocesst::make_string_returning_function_from_call
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 a...
Definition: java_string_library_preprocess.cpp:1250
character_refine_preprocess.h
Preprocess a goto-programs so that calls to the java Character library are replaced by simple express...
typet
The type of an expression, extends irept.
Definition: type.h:29
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.
Definition: java_string_library_preprocess.cpp:612
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
optional.h
java_string_library_preprocesst::string_expr_of_function
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 primit...
Definition: java_string_library_preprocess.cpp:747
character_refine_preprocesst
Definition: character_refine_preprocess.h:29
refined_string_typet
Definition: refined_string_type.h:27
java_string_library_preprocesst::cprover_equivalent_to_java_function
id_mapt cprover_equivalent_to_java_function
Definition: java_string_library_preprocess.h:115
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:119
java_string_library_preprocesst::make_assign_and_return_function_from_call
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.
Definition: java_string_library_preprocess.cpp:1113
java_string_library_preprocesst::cprover_equivalent_to_java_constructor
id_mapt cprover_equivalent_to_java_constructor
Definition: java_string_library_preprocess.h:123
java_string_library_preprocesst::decl_string_expr
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.
Definition: java_string_library_preprocess.cpp:485
exprt
Base class for all expressions.
Definition: expr.h:53
java_string_library_preprocesst::implements_function
bool implements_function(const irep_idt &function_id) const
Definition: java_string_library_preprocess.cpp:1400
java_string_library_preprocesst::make_assign_function_from_call
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.
Definition: java_string_library_preprocess.cpp:1138
java_string_library_preprocesst::make_init_function_from_call
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.
Definition: java_string_library_preprocess.cpp:1069
java_string_library_preprocesst::make_class_identifier_code
code_blockt make_class_identifier_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Used to provide our own implementation of the CProver.classIdentifier() function.
Definition: java_string_library_preprocess.cpp:1161
java_string_library_preprocesst::initialize_known_type_table
void initialize_known_type_table()
Definition: java_string_library_preprocess.cpp:1487
java_string_library_preprocesst::process_operands
exprt::operandst process_operands(const exprt::operandst &operands, const source_locationt &loc, const irep_idt &function_name, symbol_table_baset &symbol_table, code_blockt &init_code)
for each expression that is of a type implementing strings, we declare a new cprover_string whose con...
Definition: java_string_library_preprocess.cpp:336
java_string_library_preprocesst::is_java_char_sequence_pointer_type
static bool is_java_char_sequence_pointer_type(const typet &type)
Definition: java_string_library_preprocess.cpp:138
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
java_string_library_preprocesst::code_assign_java_string_to_string_expr
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)
Definition: java_string_library_preprocess.cpp:855
java_string_library_preprocesst::is_java_string_builder_type
static bool is_java_string_builder_type(const typet &type)
Definition: java_string_library_preprocess.cpp:83
java_string_library_preprocesst::get_string_type_base_classes
std::vector< irep_idt > 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 t...
Definition: java_string_library_preprocess.cpp:184
refined_string_exprt
Definition: string_expr.h:109
java_string_library_preprocesst::string_literal_to_string_expr
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.
Definition: java_string_library_preprocess.cpp:892
java_string_library_preprocesst::add_string_type
void add_string_type(const irep_idt &class_name, symbol_tablet &symbol_table)
Add to the symbol table type declaration for a String-like Java class.
Definition: java_string_library_preprocess.cpp:217
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
java_string_library_preprocesst::conversion_functiont
std::function< codet(const java_method_typet &, const source_locationt &, const irep_idt &, symbol_table_baset &)> conversion_functiont
Definition: java_string_library_preprocess.h:106
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 s...
Definition: java_string_library_preprocess.cpp:707
java_string_library_preprocesst::conversion_table
std::unordered_map< irep_idt, conversion_functiont > conversion_table
Definition: java_string_library_preprocess.h:111
java_string_library_preprocesst::make_copy_constructor_code
code_blockt make_copy_constructor_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Generates code for a constructor of a string object from another string object.
Definition: java_string_library_preprocess.cpp:1340
java_string_library_preprocesst::make_function_from_call
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.
Definition: java_string_library_preprocess.cpp:1220
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
java_string_library_preprocesst::get_all_function_names
void get_all_function_names(std::unordered_set< irep_idt > &methods) const
Definition: java_string_library_preprocess.cpp:1424
java_string_library_preprocesst::is_java_char_array_type
static bool is_java_char_array_type(const typet &type)
Definition: java_string_library_preprocess.cpp:152
java_string_library_preprocesst::replace_character_call
codet replace_character_call(code_function_callt call)
Definition: java_string_library_preprocess.h:54
java_string_library_preprocesst::make_nondet_string_expr
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 fro...
Definition: java_string_library_preprocess.cpp:510
java_string_library_preprocesst::code_for_function
codet code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table)
Should be called to provide code for string functions that are used in the code but for which no impl...
Definition: java_string_library_preprocess.cpp:1439
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
java_string_library_preprocesst::cprover_equivalent_to_java_assign_function
id_mapt cprover_equivalent_to_java_assign_function
Definition: java_string_library_preprocess.h:132
java_string_library_preprocesst::implements_java_char_sequence
static bool implements_java_char_sequence(const typet &type)
Definition: java_string_library_preprocess.h:70
java_string_library_preprocesst::is_java_char_sequence_type
static bool is_java_char_sequence_type(const typet &type)
Definition: java_string_library_preprocess.cpp:129
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
java_int_type
signedbv_typet java_int_type()
Definition: java_types.cpp:32
std_code.h
java_string_library_preprocesst::java_type_matches_tag
static bool java_type_matches_tag(const typet &type, const std::string &tag)
Definition: java_string_library_preprocess.cpp:53
java_string_library_preprocesst::character_preprocess
character_refine_preprocesst character_preprocess
Definition: java_string_library_preprocess.h:95
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 le...
Definition: java_string_library_preprocess.cpp:675
source_locationt
Definition: source_location.h:20
java_string_library_preprocesst::is_java_char_array_pointer_type
static bool is_java_char_array_pointer_type(const typet &type)
Definition: java_string_library_preprocess.cpp:161
java_string_library_preprocesst::make_float_to_string_code
code_blockt make_float_to_string_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Provide code for the String.valueOf(F) function.
Definition: java_string_library_preprocess.cpp:912
java_string_library_preprocesst::is_java_string_buffer_type
static bool is_java_string_buffer_type(const typet &type)
Definition: java_string_library_preprocess.cpp:106
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1310
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 char...
Definition: java_string_library_preprocess.cpp:644
refined_string_type.h
Type for string expressions used by the string solver.
java_string_library_preprocesst::refined_string_type
const refined_string_typet refined_string_type
Definition: java_string_library_preprocess.h:99
java_string_library_preprocesst::code_assign_components_to_java_string
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.
Definition: java_string_library_preprocess.cpp:794
java_string_library_preprocesst::is_java_string_buffer_pointer_type
static bool is_java_string_buffer_pointer_type(const typet &type)
Definition: java_string_library_preprocess.cpp:115
java_string_library_preprocesst::id_maps
const std::array< id_mapt *, 5 > id_maps
Definition: java_string_library_preprocess.h:134
java_string_library_preprocesst::implements_java_char_sequence_pointer
static bool implements_java_char_sequence_pointer(const typet &type)
Definition: java_string_library_preprocess.h:63
symbolt
Symbol table entry.
Definition: symbol.h:28
ieee_float.h
java_string_library_preprocesst::convert_exprt_to_string_exprt_unit_test
friend 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_tablet &symbol_table, code_blockt &init_code)
java_char_type
unsignedbv_typet java_char_type()
Definition: java_types.cpp:62
java_string_library_preprocesst
Definition: java_string_library_preprocess.h:36
java_string_library_preprocesst::is_known_string_type
bool is_known_string_type(irep_idt class_name)
Check whether a class name is known as a string type.
Definition: java_string_library_preprocess.cpp:1481
java_string_library_preprocesst::java_string_library_preprocesst
java_string_library_preprocesst(const java_string_library_preprocesst &)=delete
java_string_library_preprocesst::allocate_fresh_string
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
Definition: java_string_library_preprocess.cpp:547
java_string_library_preprocesst::initialize_conversion_table
void initialize_conversion_table()
fill maps with correspondence from java method names to conversion functions
Definition: java_string_library_preprocess.cpp:1496
java_string_library_preprocesst::fresh_string
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
Definition: java_string_library_preprocess.cpp:466
java_types.h
symbol_table.h
Author: Diffblue Ltd.
is_constructor
static bool is_constructor(const irep_idt &method_name)
Definition: java_bytecode_convert_method.cpp:128
java_string_library_preprocesst::is_java_string_pointer_type
static bool is_java_string_pointer_type(const typet &type)
Definition: java_string_library_preprocess.cpp:61
java_string_library_preprocesst::code_assign_string_expr_to_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.
Definition: java_string_library_preprocess.cpp:836
character_refine_preprocesst::replace_character_call
codet replace_character_call(const code_function_callt &call) const
replace function calls to functions of the Character by an affectation if possible,...
Definition: character_refine_preprocess.cpp:1287
java_string_library_preprocesst::string_types
std::unordered_set< irep_idt > string_types
Definition: java_string_library_preprocess.h:146
string_expr.h
String expressions for the string solver.
java_method_typet
Definition: java_types.h:103
java_string_library_preprocesst::is_java_string_type
static bool is_java_string_type(const typet &type)
Definition: java_string_library_preprocess.cpp:75
java_string_library_preprocesst::is_java_string_builder_pointer_type
static bool is_java_string_builder_pointer_type(const typet &type)
Definition: java_string_library_preprocess.cpp:92
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
ui_message.h
java_string_library_preprocesst::code_return_function_application
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
Definition: java_string_library_preprocess.cpp:596