cprover
string_constraint_generator_main.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Generates string constraints to link results from string functions
4  with their arguments. This is inspired by the PASS paper at HVC'13:
5  "PASS: String Solving with Parameterized Array and Interval Automaton"
6  by Guodong Li and Indradeep Ghosh, which gives examples of constraints
7  for several functions.
8 
9 Author: Romain Brenguier, romain.brenguier@diffblue.com
10 
11 \*******************************************************************/
12 
19 
21 
22 #include <ansi-c/string_constant.h>
24 #include <util/arith_tools.h>
26 #include <util/ssa_expr.h>
27 
29 
37  int i, const typet &char_type)
38 {
39  return from_integer(i, char_type);
40 }
41 
47  const irep_idt &prefix, const typet &type)
48 {
49  std::ostringstream buf;
50  buf << "string_refinement#" << prefix << "#" << (next_symbol_id++);
51  irep_idt name(buf.str());
52  return symbol_exprt(name, type);
53 }
54 
59  const irep_idt &prefix, const typet &type)
60 {
61  return fresh_symbol(prefix, type);
62 }
63 
68  const irep_idt &prefix, const typet &type)
69 {
70  symbol_exprt s=fresh_symbol(prefix, type);
71  index_symbols.push_back(s);
72  return s;
73 }
74 
79  const irep_idt &prefix)
80 {
82  boolean_symbols.push_back(b);
83  return b;
84 }
85 
90  const refined_string_typet &type)
91 {
92  symbol_exprt length=
93  fresh_symbol("string_length", type.get_index_type());
94  symbol_exprt content=fresh_symbol("string_content", type.get_content_type());
95  return string_exprt(length, content, type);
96 }
97 
104  const exprt &unrefined_string)
105 {
106  string_exprt s;
107 
108  if(unrefined_string.id()==ID_function_application)
109  {
111  to_function_application_expr(unrefined_string));
112  s=to_string_expr(res);
113  }
114  else if(unrefined_string.id()==ID_symbol)
115  s=find_or_add_string_of_symbol(to_symbol_expr(unrefined_string));
116  else if(unrefined_string.id()==ID_address_of)
117  {
118  assert(unrefined_string.op0().id()==ID_symbol);
119  s=find_or_add_string_of_symbol(to_symbol_expr(unrefined_string.op0()));
120  }
121  else if(unrefined_string.id()==ID_if)
122  s=add_axioms_for_if(to_if_expr(unrefined_string));
123  else if(unrefined_string.id()==ID_nondet_symbol ||
124  unrefined_string.id()==ID_struct)
125  {
126  // TODO: for now we ignore non deterministic symbols and struct
127  }
128  else if(unrefined_string.id()==ID_typecast)
129  {
130  exprt arg=to_typecast_expr(unrefined_string).op();
132  s=to_string_expr(res);
133  }
134  else
135  {
136  throw "add_axioms_for_string_expr:\n"+unrefined_string.pretty()+
137  "\nwhich is not a function application, "+
138  "a symbol or an if expression";
139  }
140 
141  axioms.push_back(
143  return s;
144 }
145 
150  const if_exprt &expr)
151 {
152  assert(
155  assert(
158  const refined_string_typet &ref_type=to_refined_string_type(t.type());
159  const typet &index_type=ref_type.get_index_type();
160  string_exprt res=fresh_string(ref_type);
161 
162  axioms.push_back(
164  symbol_exprt qvar=fresh_univ_index("QA_string_if_true", index_type);
165  equal_exprt qequal(res[qvar], t[qvar]);
166  axioms.push_back(string_constraintt(qvar, t.length(), expr.cond(), qequal));
167  axioms.push_back(
169  symbol_exprt qvar2=fresh_univ_index("QA_string_if_false", index_type);
170  equal_exprt qequal2(res[qvar2], f[qvar2]);
171  string_constraintt sc2(qvar2, f.length(), not_exprt(expr.cond()), qequal2);
172  axioms.push_back(sc2);
173  return res;
174 }
175 
183  const symbol_exprt &sym)
184 {
185  irep_idt id=sym.get_identifier();
186  const refined_string_typet &ref_type=to_refined_string_type(sym.type());
187  string_exprt str=fresh_string(ref_type);
188  auto entry=symbol_to_string.insert(std::make_pair(id, str));
189  return entry.first->second;
190 }
191 
198  const function_application_exprt &expr)
199 {
200  const exprt &name=expr.function();
201  assert(name.id()==ID_symbol);
202 
203  const irep_idt &id=is_ssa_expr(name)?to_ssa_expr(name).get_object_name():
205 
206  // TODO: improve efficiency of this test by either ordering test by frequency
207  // or using a map
208 
209  if(id==ID_cprover_char_literal_func)
210  return add_axioms_for_char_literal(expr);
211  else if(id==ID_cprover_string_length_func)
212  return add_axioms_for_length(expr);
213  else if(id==ID_cprover_string_equal_func)
214  return add_axioms_for_equals(expr);
215  else if(id==ID_cprover_string_equals_ignore_case_func)
217  else if(id==ID_cprover_string_is_empty_func)
218  return add_axioms_for_is_empty(expr);
219  else if(id==ID_cprover_string_char_at_func)
220  return add_axioms_for_char_at(expr);
221  else if(id==ID_cprover_string_is_prefix_func)
222  return add_axioms_for_is_prefix(expr);
223  else if(id==ID_cprover_string_is_suffix_func)
224  return add_axioms_for_is_suffix(expr);
225  else if(id==ID_cprover_string_startswith_func)
226  return add_axioms_for_is_prefix(expr, true);
227  else if(id==ID_cprover_string_endswith_func)
228  return add_axioms_for_is_suffix(expr, true);
229  else if(id==ID_cprover_string_contains_func)
230  return add_axioms_for_contains(expr);
231  else if(id==ID_cprover_string_hash_code_func)
232  return add_axioms_for_hash_code(expr);
233  else if(id==ID_cprover_string_index_of_func)
234  return add_axioms_for_index_of(expr);
235  else if(id==ID_cprover_string_last_index_of_func)
236  return add_axioms_for_last_index_of(expr);
237  else if(id==ID_cprover_string_parse_int_func)
238  return add_axioms_for_parse_int(expr);
239  else if(id==ID_cprover_string_to_char_array_func)
240  return add_axioms_for_to_char_array(expr);
241  else if(id==ID_cprover_string_code_point_at_func)
242  return add_axioms_for_code_point_at(expr);
243  else if(id==ID_cprover_string_code_point_before_func)
245  else if(id==ID_cprover_string_code_point_count_func)
246  return add_axioms_for_code_point_count(expr);
247  else if(id==ID_cprover_string_offset_by_code_point_func)
249  else if(id==ID_cprover_string_compare_to_func)
250  return add_axioms_for_compare_to(expr);
251  else if(id==ID_cprover_string_literal_func)
252  return add_axioms_from_literal(expr);
253  else if(id==ID_cprover_string_concat_func)
254  return add_axioms_for_concat(expr);
255  else if(id==ID_cprover_string_concat_int_func)
256  return add_axioms_for_concat_int(expr);
257  else if(id==ID_cprover_string_concat_long_func)
258  return add_axioms_for_concat_long(expr);
259  else if(id==ID_cprover_string_concat_bool_func)
260  return add_axioms_for_concat_bool(expr);
261  else if(id==ID_cprover_string_concat_char_func)
262  return add_axioms_for_concat_char(expr);
263  else if(id==ID_cprover_string_concat_double_func)
264  return add_axioms_for_concat_double(expr);
265  else if(id==ID_cprover_string_concat_float_func)
266  return add_axioms_for_concat_float(expr);
267  else if(id==ID_cprover_string_concat_code_point_func)
269  else if(id==ID_cprover_string_insert_func)
270  return add_axioms_for_insert(expr);
271  else if(id==ID_cprover_string_insert_int_func)
272  return add_axioms_for_insert_int(expr);
273  else if(id==ID_cprover_string_insert_long_func)
274  return add_axioms_for_insert_long(expr);
275  else if(id==ID_cprover_string_insert_bool_func)
276  return add_axioms_for_insert_bool(expr);
277  else if(id==ID_cprover_string_insert_char_func)
278  return add_axioms_for_insert_char(expr);
279  else if(id==ID_cprover_string_insert_double_func)
280  return add_axioms_for_insert_double(expr);
281  else if(id==ID_cprover_string_insert_float_func)
282  return add_axioms_for_insert_float(expr);
283  else if(id==ID_cprover_string_insert_char_array_func)
285  else if(id==ID_cprover_string_substring_func)
286  return add_axioms_for_substring(expr);
287  else if(id==ID_cprover_string_trim_func)
288  return add_axioms_for_trim(expr);
289  else if(id==ID_cprover_string_to_lower_case_func)
290  return add_axioms_for_to_lower_case(expr);
291  else if(id==ID_cprover_string_to_upper_case_func)
292  return add_axioms_for_to_upper_case(expr);
293  else if(id==ID_cprover_string_char_set_func)
294  return add_axioms_for_char_set(expr);
295  else if(id==ID_cprover_string_value_of_func)
296  return add_axioms_for_value_of(expr);
297  else if(id==ID_cprover_string_empty_string_func)
298  return add_axioms_for_empty_string(expr);
299  else if(id==ID_cprover_string_copy_func)
300  return add_axioms_for_copy(expr);
301  else if(id==ID_cprover_string_of_int_func)
302  return add_axioms_from_int(expr);
303  else if(id==ID_cprover_string_of_int_hex_func)
304  return add_axioms_from_int_hex(expr);
305  else if(id==ID_cprover_string_of_float_func)
306  return add_axioms_from_float(expr);
307  else if(id==ID_cprover_string_of_double_func)
308  return add_axioms_from_double(expr);
309  else if(id==ID_cprover_string_of_long_func)
310  return add_axioms_from_long(expr);
311  else if(id==ID_cprover_string_of_bool_func)
312  return add_axioms_from_bool(expr);
313  else if(id==ID_cprover_string_of_char_func)
314  return add_axioms_from_char(expr);
315  else if(id==ID_cprover_string_of_char_array_func)
316  return add_axioms_from_char_array(expr);
317  else if(id==ID_cprover_string_set_length_func)
318  return add_axioms_for_set_length(expr);
319  else if(id==ID_cprover_string_delete_func)
320  return add_axioms_for_delete(expr);
321  else if(id==ID_cprover_string_delete_char_at_func)
322  return add_axioms_for_delete_char_at(expr);
323  else if(id==ID_cprover_string_replace_func)
324  return add_axioms_for_replace(expr);
325  else
326  {
327  std::string msg(
328  "string_constraint_generator::function_application: unknown symbol :");
329  msg+=id2string(id);
330  throw msg;
331  }
332 }
333 
340 {
342  const refined_string_typet &ref_type=to_refined_string_type(s1.type());
343  string_exprt res=fresh_string(ref_type);
344 
345  // We add axioms:
346  // a1 : |res|=|s1|
347  // a2 : forall i<|s1|. s1[i]=res[i]
348 
349  axioms.push_back(res.axiom_for_has_same_length_as(s1));
350 
351  symbol_exprt idx=fresh_univ_index("QA_index_copy", ref_type.get_index_type());
352  string_constraintt a2(idx, s1.length(), equal_exprt(s1[idx], res[idx]));
353  axioms.push_back(a2);
354  return res;
355 }
356 
362  const exprt &char_array)
363 {
366  exprt arr=to_address_of_expr(char_array).object();
367  exprt len=member_exprt(arr, "length", res.length().type());
368  exprt cont=member_exprt(arr, "data", res.content().type());
369  res.length()=len;
370  res.content()=cont;
371  return res;
372 }
373 
379 {
381  return str.length();
382 }
383 
392  const exprt &length,
393  const exprt &data,
394  const exprt &offset,
395  const exprt &count)
396 {
397  const typet &char_type=to_array_type(data.type()).subtype();
398  const typet &index_type=length.type();
400  string_exprt str=fresh_string(ref_type);
401 
402  // We add axioms:
403  // a1 : forall q < count. str[q] = data[q+offset]
404  // a2 : |str| = count
405 
406  symbol_exprt qvar=fresh_univ_index("QA_string_of_char_array", index_type);
407  exprt char_in_tab=data;
408  assert(char_in_tab.id()==ID_index);
409  char_in_tab.op1()=plus_exprt(qvar, offset);
410 
411  string_constraintt a1(qvar, count, equal_exprt(str[qvar], char_in_tab));
412  axioms.push_back(a1);
413  axioms.push_back(equal_exprt(str.length(), count));
414 
415  return str;
416 }
417 
425 {
426  exprt offset;
427  exprt count;
428  if(f.arguments().size()==4)
429  {
430  offset=f.arguments()[2];
431  count=f.arguments()[3];
432  }
433  else
434  {
435  assert(f.arguments().size()==2);
436  count=f.arguments()[0];
437  offset=from_integer(0, count.type());
438  }
439  const exprt &tab_length=f.arguments()[0];
440  const exprt &data=f.arguments()[1];
441  return add_axioms_from_char_array(tab_length, data, offset, count);
442 }
443 
448 {
449  return binary_relation_exprt(
450  x, ID_ge, from_integer(0, x.type()));
451 }
452 
458 {
460  assert(args.size()==1); // there should be exactly 1 argument to char literal
461 
462  const exprt &arg=args[0];
463  // for C programs argument to char literal should be one string constant
464  // of size 1.
465  if(arg.operands().size()==1 &&
466  arg.op0().operands().size()==1 &&
467  arg.op0().op0().operands().size()==2 &&
468  arg.op0().op0().op0().id()==ID_string_constant)
469  {
470  const string_constantt s=to_string_constant(arg.op0().op0().op0());
471  irep_idt sval=s.get_value();
472  assert(sval.size()==1);
473  return from_integer(unsigned(sval[0]), arg.type());
474  }
475  else
476  {
477  throw "convert_char_literal unimplemented";
478  }
479 }
480 
488 {
490  const refined_string_typet &ref_type=to_refined_string_type(str.type());
491  symbol_exprt char_sym=fresh_symbol("char", ref_type.get_char_type());
492  axioms.push_back(equal_exprt(char_sym, str[args(f, 2)[1]]));
493  return char_sym;
494 }
495 
501 {
503  return str.content();
504 }
505 
510  const symbol_exprt &sym, const exprt &str)
511 {
512  if(str.id()==ID_symbol)
514  else
516 }
exprt add_axioms_for_compare_to(const function_application_exprt &f)
add axioms corresponding to the String.compareTo java function
The type of an expression.
Definition: type.h:20
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:1760
string_exprt add_axioms_for_insert_char(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(C) java function
string_exprt add_axioms_for_insert_int(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(I) java function
string_exprt add_axioms_from_literal(const function_application_exprt &f)
add axioms to say that the returned string expression is equal to the string literal ...
Boolean negation.
Definition: std_expr.h:2648
exprt add_axioms_for_is_prefix(const string_exprt &prefix, const string_exprt &str, const exprt &offset)
add axioms stating that the returned expression is true exactly when the first string is a prefix of ...
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast a generic exprt to a function_application_exprt.
Definition: std_expr.h:3826
exprt & true_case()
Definition: std_expr.h:2805
string_exprt add_axioms_for_java_char_array(const exprt &char_array)
add axioms corresponding to the String.valueOf([C) java function
Generates string constraints to link results from string functions with their arguments.
void assign_to_symbol(const symbol_exprt &sym, const string_exprt &expr)
exprt add_axioms_for_code_point_at(const function_application_exprt &f)
add axioms corresponding to the String.codePointAt java function
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:568
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
string_exprt add_axioms_for_concat_double(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.append(D) java function
std::list< symbol_exprt > boolean_symbols
string_exprt add_axioms_for_delete(const string_exprt &str, const exprt &start, const exprt &end)
add axioms stating that the returned string corresponds to the input one where we removed characters ...
string_exprt add_axioms_for_delete_char_at(const function_application_exprt &expr)
add axioms corresponding to the StringBuilder.deleteCharAt java function
application of (mathematical) function
Definition: std_expr.h:3785
exprt & object()
Definition: std_expr.h:2608
string_exprt add_axioms_from_bool(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(Z) java function
string_exprt & to_string_expr(exprt &expr)
Definition: string_expr.h:133
string_exprt add_axioms_for_concat_int(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.append(I) java function
exprt & op0()
Definition: expr.h:84
const typet & get_char_type() const
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
typet java_int_type()
Definition: java_types.cpp:19
exprt add_axioms_for_equals(const function_application_exprt &f)
add axioms stating that the result is true exactly when the strings represented by the arguments are ...
exprt add_axioms_for_length(const function_application_exprt &f)
add axioms corresponding to the String.length java function
const irep_idt & get_identifier() const
Definition: std_expr.h:120
string_exprt add_axioms_for_copy(const function_application_exprt &f)
add axioms to say that the returned string expression is equal to the argument of the function applic...
string_exprt add_axioms_for_insert_float(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(F) java function
argumentst & arguments()
Definition: std_expr.h:3805
string_exprt add_axioms_for_concat_code_point(const function_application_exprt &f)
Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.
static symbol_exprt fresh_symbol(const irep_idt &prefix, const typet &type=bool_typet())
generate a new symbol expression of the given type with some prefix
exprt add_axioms_for_contains(const function_application_exprt &f)
add axioms corresponding to the String.contains java function
exprt add_axioms_for_code_point_count(const function_application_exprt &f)
add axioms giving approximate bounds on the result of the String.codePointCount java function ...
exprt add_axioms_for_offset_by_code_point(const function_application_exprt &f)
add axioms giving approximate bounds on the result of the String.offsetByCodePointCount java function...
symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type)
generate an index symbol to be used as an universaly quantified variable
string_exprt add_axioms_from_double(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(D) java function
string_exprt add_axioms_for_insert_long(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(J) java function
The trinary if-then-else operator.
Definition: std_expr.h:2771
exprt & cond()
Definition: std_expr.h:2795
equal_exprt axiom_for_has_same_length_as(const string_exprt &rhs) const
Definition: string_expr.h:114
typet & type()
Definition: expr.h:60
string_exprt add_axioms_from_long(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(J) java function
The proper Booleans.
Definition: std_types.h:33
string_exprt add_axioms_for_trim(const function_application_exprt &expr)
add axioms corresponding to the String.trim java function
A constant literal expression.
Definition: std_expr.h:3685
exprt add_axioms_for_is_empty(const function_application_exprt &f)
add axioms stating that the returned value is true exactly when the argument string is empty ...
exprt & op()
Definition: std_expr.h:1739
string_exprt add_axioms_for_empty_string(const function_application_exprt &f)
add axioms to say that the returned string expression is empty
boolean implication
Definition: std_expr.h:1926
string_exprt add_axioms_for_if(const if_exprt &expr)
add axioms for an if expression which should return a string
const array_typet & get_content_type() const
string_exprt add_axioms_for_concat_float(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.append(F) java function
exprt add_axioms_for_index_of(const string_exprt &str, const exprt &c, const exprt &from_index)
add axioms that the returned value is either -1 or greater than from_index and the character at that ...
exprt add_axioms_for_last_index_of(const string_exprt &str, const exprt &c, const exprt &from_index)
Extract member of struct or union.
Definition: std_expr.h:3214
equality
Definition: std_expr.h:1082
exprt add_axioms_for_function_application(const function_application_exprt &expr)
strings contained in this call are converted to objects of type string_exprt, through adding axioms...
symbol_exprt fresh_boolean(const irep_idt &prefix)
generate a Boolean symbol which is existentially quantified
string_exprt add_axioms_for_insert_double(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(D) java function
std::map< irep_idt, string_exprt > symbol_to_string
string_exprt fresh_string(const refined_string_typet &type)
construct a string expression whose length and content are new variables
string_exprt add_axioms_for_char_set(const function_application_exprt &expr)
add axioms corresponding stating that the result is similar to that of the StringBuilder.setCharAt java function Warning: this may be underspecified in the case wher the index exceed the length of the string
const irep_idt & id() const
Definition: irep.h:189
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:2629
static bool is_unrefined_string_type(const typet &type)
string_exprt add_axioms_for_concat_bool(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.append(Z) java function
const exprt & length() const
Definition: string_expr.h:35
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:150
exprt add_axioms_for_hash_code(const function_application_exprt &f)
add axioms stating that if two strings are equal then their hash codes are equals ...
string_exprt add_axioms_from_float(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(F) java function
exprt::operandst argumentst
Definition: std_expr.h:3803
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:2836
string_exprt add_axioms_for_value_of(const function_application_exprt &f)
add axioms corresponding to the String.valueOf([C) and String.valueOf([CII) functions ...
string_exprt add_axioms_for_string_expr(const exprt &expr)
obtain a refined string expression corresponding to string variable of string function call ...
const refined_string_typet & to_refined_string_type(const typet &type)
string_exprt add_axioms_for_insert_bool(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(Z) java function
string_exprt add_axioms_for_concat(const string_exprt &s1, const string_exprt &s2)
add axioms to say that the returned string expression is equal to the concatenation of the two string...
exprt add_axioms_for_parse_int(const function_application_exprt &f)
add axioms corresponding to the Integer.parseInt java function
exprt add_axioms_for_is_suffix(const function_application_exprt &f, bool swap_arguments=false)
add axioms corresponding to the String.isSuffix java function
exprt & op1()
Definition: expr.h:87
string_exprt find_or_add_string_of_symbol(const symbol_exprt &sym)
if a symbol represent a string is present in the symbol_to_string table, returns the corresponding st...
exprt add_axioms_for_equals_ignore_case(const function_application_exprt &f)
add axioms corresponding to the String.equalsIgnoreCase java function
The plus expression.
Definition: std_expr.h:702
string_exprt add_axioms_for_insert(const string_exprt &s1, const string_exprt &s2, const exprt &offset)
add axioms stating that the result correspond to the first string where we inserted the second one at...
exprt add_axioms_for_char_literal(const function_application_exprt &f)
add axioms stating that the returned value is equal to the argument
const typet & get_index_type() const
bitvector_typet index_type()
Definition: c_types.cpp:15
exprt & false_case()
Definition: std_expr.h:2815
Various predicates over pointers in programs.
binary_relation_exprt axiom_for_is_longer_than(const string_exprt &rhs) const
Definition: string_expr.h:56
string_exprt add_axioms_from_char(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(C) java function
exprt add_axioms_for_to_char_array(const function_application_exprt &f)
add axioms corresponding to the String.toCharArray java function
static constant_exprt constant_char(int i, const typet &char_type)
generate constant character expression with character type.
symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type)
generate an index symbol which is existentially quantified
void set_string_symbol_equal_to_expr(const symbol_exprt &sym, const exprt &str)
add a correspondence to make sure the symbol points to the same string as the second argument ...
string_exprt add_axioms_for_to_lower_case(const function_application_exprt &expr)
add axioms corresponding to the String.toLowerCase java function
exprt add_axioms_for_char_at(const function_application_exprt &f)
add axioms stating that the character of the string at the given position is equal to the returned va...
const string_constantt & to_string_constant(const exprt &expr)
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
const exprt & content() const
Definition: string_expr.h:39
string_exprt add_axioms_for_to_upper_case(const function_application_exprt &expr)
add axioms corresponding to the String.toUpperCase java function
irep_idt get_object_name() const
Definition: ssa_expr.h:46
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:169
string_exprt add_axioms_for_set_length(const function_application_exprt &f)
add axioms to say that the returned string expression has length given by the second argument and who...
std::list< symbol_exprt > index_symbols
exprt add_axioms_for_code_point_before(const function_application_exprt &f)
add axioms corresponding to the String.codePointBefore java function
string_exprt add_axioms_from_int(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(I) java function
string_exprt add_axioms_for_replace(const function_application_exprt &f)
add axioms corresponding to the String.replace java function
Expression to hold a symbol (variable)
Definition: std_expr.h:82
string_exprt add_axioms_from_int_hex(const exprt &i, const refined_string_typet &ref_type)
add axioms stating that the returned string corresponds to the integer argument written in hexadecima...
int8_t s1
Definition: bytecode_info.h:59
string_exprt add_axioms_for_concat_long(const function_application_exprt &f)
Add axioms corresponding to the StringBuilder.append(J) java function.
string_exprt add_axioms_for_concat_char(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.append(C) java function
typet java_char_type()
Definition: java_types.cpp:44
const irep_idt & get_value() const
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
static const function_application_exprt::argumentst & args(const function_application_exprt &expr, size_t nb)
bitvector_typet char_type()
Definition: c_types.cpp:113
string_exprt add_axioms_for_insert_char_array(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert:(I[CII) and StringBuilder.insert:(I[C) java func...
Definition: kdev_t.h:24
string_exprt add_axioms_from_char_array(const function_application_exprt &f)
add axioms corresponding to the String.
exprt axiom_for_is_positive_index(const exprt &x)
expression true exactly when the index is positive
string_exprt add_axioms_for_substring(const string_exprt &str, const exprt &start, const exprt &end)
add axioms stating that the returned string expression is equal to the input one starting at start an...