cprover
string_constraint_generator_valueof.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Generates string constraints for functions generating strings
4  from other types, in particular int, long, float, double, char, bool
5 
6 Author: Romain Brenguier, romain.brenguier@diffblue.com
7 
8 \*******************************************************************/
9 
13 
16 #include <util/simplify_expr.h>
17 #include <util/deprecate.h>
18 
19 #include <cmath>
21 
28 static unsigned long to_integer_or_default(
29  const exprt &expr,
30  unsigned long def,
31  const namespacet &ns)
32 {
33  if(const auto i = numeric_cast<unsigned long>(simplify_expr(expr, ns)))
34  return *i;
35  return def;
36 }
37 
44 DEPRECATED("should use add_axioms_for_string_of_int instead")
47  array_poolt &array_pool,
48  const namespacet &ns)
49 {
50  PRECONDITION(f.arguments().size() == 3 || f.arguments().size() == 4);
51  const array_string_exprt res =
52  char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
53  if(f.arguments().size() == 4)
55  res, f.arguments()[2], f.arguments()[3], 0, ns);
56  else
57  return add_axioms_for_string_of_int(res, f.arguments()[2], 0, ns);
58 }
59 
65 DEPRECATED("This is Java specific and should be implemented in Java instead")
68  array_poolt &array_pool)
69 {
70  PRECONDITION(f.arguments().size() == 3);
71  const array_string_exprt res =
72  char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
73  return add_axioms_from_bool(res, f.arguments()[2]);
74 }
75 
82 DEPRECATED("This is Java specific and should be implemented in Java instead")
84  const array_string_exprt &res,
85  const exprt &b)
86 {
87  const typet &char_type = res.content().type().subtype();
88  PRECONDITION(b.type()==bool_typet() || b.type().id()==ID_c_bool);
89  string_constraintst constraints;
90  typecast_exprt eq(b, bool_typet());
91 
92  // We add axioms:
93  // a1 : eq => res = |"true"|
94  // a2 : forall i < |"true"|. eq => res[i]="true"[i]
95  // a3 : !eq => res = |"false"|
96  // a4 : forall i < |"false"|. !eq => res[i]="false"[i]
97 
98  std::string str_true="true";
99  const implies_exprt a1(eq, length_eq(res, str_true.length()));
100  constraints.existential.push_back(a1);
101 
102  for(std::size_t i=0; i<str_true.length(); i++)
103  {
104  exprt chr=from_integer(str_true[i], char_type);
105  implies_exprt a2(eq, equal_exprt(res[i], chr));
106  constraints.existential.push_back(a2);
107  }
108 
109  std::string str_false="false";
110  const implies_exprt a3(not_exprt(eq), length_eq(res, str_false.length()));
111  constraints.existential.push_back(a3);
112 
113  for(std::size_t i=0; i<str_false.length(); i++)
114  {
115  exprt chr=from_integer(str_false[i], char_type);
116  implies_exprt a4(not_exprt(eq), equal_exprt(res[i], chr));
117  constraints.existential.push_back(a4);
118  }
119 
120  return {from_integer(0, get_return_code_type()), std::move(constraints)};
121 }
122 
132 std::pair<exprt, string_constraintst> add_axioms_for_string_of_int(
133  const array_string_exprt &res,
134  const exprt &input_int,
135  size_t max_size,
136  const namespacet &ns)
137 {
138  const constant_exprt radix=from_integer(10, input_int.type());
140  res, input_int, radix, max_size, ns);
141 }
142 
153 std::pair<exprt, string_constraintst> add_axioms_for_string_of_int_with_radix(
154  const array_string_exprt &res,
155  const exprt &input_int,
156  const exprt &radix,
157  size_t max_size,
158  const namespacet &ns)
159 {
160  PRECONDITION(max_size < std::numeric_limits<size_t>::max());
161  const typet &type=input_int.type();
162  PRECONDITION(type.id()==ID_signedbv);
163 
166  const unsigned long radix_ul = to_integer_or_default(radix, 0, ns);
167  CHECK_RETURN((radix_ul>=2 && radix_ul<=36) || radix_ul==0);
168 
169  if(max_size==0)
170  {
171  max_size=max_printed_string_length(type, radix_ul);
172  CHECK_RETURN(max_size<std::numeric_limits<size_t>::max());
173  }
174 
175  const typet &char_type = res.content().type().subtype();
176  const typecast_exprt radix_as_char(radix, char_type);
177  const typecast_exprt radix_input_type(radix, type);
178  const bool strict_formatting=true;
179 
181  res, radix_as_char, radix_ul, max_size, strict_formatting);
183  input_int,
184  type,
185  strict_formatting,
186  res,
187  max_size,
188  radix_input_type,
189  radix_ul);
190  merge(result2, std::move(result1));
191  return {from_integer(0, get_return_code_type()), std::move(result2)};
192 }
193 
198 static exprt int_of_hex_char(const exprt &chr)
199 {
200  const exprt zero_char = from_integer('0', chr.type());
201  const exprt nine_char = from_integer('9', chr.type());
202  const exprt a_char = from_integer('a', chr.type());
203  return if_exprt(
204  binary_relation_exprt(chr, ID_gt, nine_char),
205  plus_exprt(from_integer(10, chr.type()), minus_exprt(chr, a_char)),
206  minus_exprt(chr, zero_char));
207 }
208 
215 DEPRECATED("use add_axioms_for_string_of_int_with_radix instead")
217  const array_string_exprt &res,
218  const exprt &i)
219 {
220  const typet &type=i.type();
221  PRECONDITION(type.id()==ID_signedbv);
222  string_constraintst constraints;
223  const typet &index_type = res.length().type();
224  const typet &char_type = res.content().type().subtype();
225  exprt sixteen=from_integer(16, index_type);
226  exprt minus_char = from_integer('-', char_type);
227  exprt zero_char = from_integer('0', char_type);
228  exprt nine_char = from_integer('9', char_type);
229  exprt a_char = from_integer('a', char_type);
230  exprt f_char = from_integer('f', char_type);
231 
232  size_t max_size=8;
233  constraints.existential.push_back(
234  and_exprt(length_gt(res, 0), length_le(res, max_size)));
235 
236  for(size_t size=1; size<=max_size; size++)
237  {
238  exprt sum=from_integer(0, type);
239  exprt all_numbers=true_exprt();
240  exprt chr=res[0];
241 
242  for(size_t j=0; j<size; j++)
243  {
244  chr=res[j];
245  exprt chr_int = int_of_hex_char(chr);
246  sum = plus_exprt(mult_exprt(sum, sixteen), typecast_exprt(chr_int, type));
248  and_exprt(
249  binary_relation_exprt(chr, ID_ge, zero_char),
250  binary_relation_exprt(chr, ID_le, nine_char)),
251  and_exprt(
252  binary_relation_exprt(chr, ID_ge, a_char),
253  binary_relation_exprt(chr, ID_le, f_char)));
254  all_numbers=and_exprt(all_numbers, is_number);
255  }
256 
257  const equal_exprt premise = length_eq(res, size);
258  constraints.existential.push_back(
259  implies_exprt(premise, and_exprt(equal_exprt(i, sum), all_numbers)));
260 
261  // disallow 0s at the beginning
262  if(size>1)
263  constraints.existential.push_back(
264  implies_exprt(premise, not_exprt(equal_exprt(res[0], zero_char))));
265  }
266  return {from_integer(0, get_return_code_type()), std::move(constraints)};
267 }
268 
273 std::pair<exprt, string_constraintst> add_axioms_from_int_hex(
275  array_poolt &array_pool)
276 {
277  PRECONDITION(f.arguments().size() == 3);
278  const array_string_exprt res =
279  char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
280  return add_axioms_from_int_hex(res, f.arguments()[2]);
281 }
282 
285 // NOLINTNEXTLINE
287 // NOLINTNEXTLINE
294 std::pair<exprt, string_constraintst> add_axioms_from_char(
296  array_poolt &array_pool)
297 {
298  PRECONDITION(f.arguments().size() == 3);
299  const array_string_exprt res =
300  char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
301  return add_axioms_from_char(res, f.arguments()[2]);
302 }
303 
311 std::pair<exprt, string_constraintst> add_axioms_from_char(
312  const array_string_exprt &res,
313  const exprt &c)
314 {
315  const and_exprt lemma(equal_exprt(res[0], c), length_eq(res, 1));
316  return {from_integer(0, get_return_code_type()), {{lemma}}};
317 }
318 
330  const array_string_exprt &str,
331  const exprt &radix_as_char,
332  const unsigned long radix_ul,
333  const std::size_t max_size,
334  const bool strict_formatting)
335 {
336  string_constraintst constraints;
337  const typet &char_type = str.content().type().subtype();
338  const typet &index_type = str.length().type();
339 
340  const exprt &chr=str[0];
341  const equal_exprt starts_with_minus(chr, from_integer('-', char_type));
342  const equal_exprt starts_with_plus(chr, from_integer('+', char_type));
343  const exprt starts_with_digit=
344  is_digit_with_radix(chr, strict_formatting, radix_as_char, radix_ul);
345 
346  // |str| > 0
347  const exprt non_empty = length_ge(str, from_integer(1, index_type));
348  constraints.existential.push_back(non_empty);
349 
350  if(strict_formatting)
351  {
352  // str[0] = '-' || is_digit_with_radix(str[0], radix)
353  const or_exprt correct_first(starts_with_minus, starts_with_digit);
354  constraints.existential.push_back(correct_first);
355  }
356  else
357  {
358  // str[0] = '-' || str[0] = '+' || is_digit_with_radix(str[0], radix)
359  const or_exprt correct_first(
360  starts_with_minus, starts_with_digit, starts_with_plus);
361  constraints.existential.push_back(correct_first);
362  }
363 
364  // str[0]='+' or '-' ==> |str| > 1
365  const implies_exprt contains_digit(
366  or_exprt(starts_with_minus, starts_with_plus),
367  length_ge(str, from_integer(2, index_type)));
368  constraints.existential.push_back(contains_digit);
369 
370  // |str| <= max_size
371  constraints.existential.push_back(length_le(str, max_size));
372 
373  // forall 1 <= i < |str| . is_digit_with_radix(str[i], radix)
374  // We unfold the above because we know that it will be used for all i up to
375  // str.length(), and str.length() <= max_size
376  for(std::size_t index=1; index<max_size; ++index)
377  {
379  const implies_exprt character_at_index_is_digit(
380  length_ge(str, from_integer(index + 1, index_type)),
382  str[index], strict_formatting, radix_as_char, radix_ul));
383  constraints.existential.push_back(character_at_index_is_digit);
384  }
385 
386  if(strict_formatting)
387  {
388  const exprt zero_char = from_integer('0', char_type);
389 
390  // no_leading_zero : str[0] = '0' => |str| = 1
391  const implies_exprt no_leading_zero(
392  equal_exprt(chr, zero_char), length_eq(str, from_integer(1, index_type)));
393  constraints.existential.push_back(no_leading_zero);
394 
395  // no_leading_zero_after_minus : str[0]='-' => str[1]!='0'
396  implies_exprt no_leading_zero_after_minus(
397  starts_with_minus, not_exprt(equal_exprt(str[1], zero_char)));
398  constraints.existential.push_back(no_leading_zero_after_minus);
399  }
400  return constraints;
401 }
402 
416  const exprt &input_int,
417  const typet &type,
418  const bool strict_formatting,
419  const array_string_exprt &str,
420  const std::size_t max_string_length,
421  const exprt &radix,
422  const unsigned long radix_ul)
423 {
424  string_constraintst constraints;
425  const typet &char_type = str.content().type().subtype();
426 
427  const equal_exprt starts_with_minus(str[0], from_integer('-', char_type));
428  const constant_exprt zero_expr=from_integer(0, type);
429  exprt::operandst digit_constraints;
430 
432  str[0], char_type, type, strict_formatting, radix_ul);
433 
437  constraints.existential.push_back(
438  implies_exprt(length_eq(str, 1), equal_exprt(input_int, sum)));
439 
440  for(size_t size=2; size<=max_string_length; size++)
441  {
442  // sum_0 := numeric value of res[0] (which is 0 if res[0] is '-')
443  // For each 1<=j<max_string_length, we have:
444  // sum_j := radix * sum_{j-1} + numeric value of res[j]
445  // no_overflow_j := sum_{j-1} == (radix * sum_{j-1} / radix)
446  // && sum_j >= sum_{j - 1}
447  // (the first part avoid overflows in the multiplication and the second
448  // one in the addition of the definition of sum_j)
449  // For all 1<=size<=max_string_length we add axioms:
450  // a5 : |res| == size =>
451  // forall max_string_length-2 <= j < size. no_overflow_j
452  // a6 : |res| == size && res[0] is a digit for radix =>
453  // input_int == sum_{size-1}
454  // a7 : |res| == size && res[0] == '-' => input_int == -sum_{size-1}
455 
456  const mult_exprt radix_sum(sum, radix);
457  // new_sum = radix * sum + (numeric value of res[j])
458  const exprt new_sum=plus_exprt(
459  radix_sum,
461  str[size-1], char_type, type, strict_formatting, radix_ul));
462 
463  // An overflow can happen when reaching the last index which can contain
464  // a digit, which is `max_string_length - 2` because of the space left for
465  // a minus sign. That assumes that we were able to identify the radix. If we
466  // weren't then we check for overflow on every index.
467  if(size-1>=max_string_length-2 || radix_ul==0)
468  {
469  const and_exprt no_overflow(
470  equal_exprt(sum, div_exprt(radix_sum, radix)),
471  binary_relation_exprt(new_sum, ID_ge, radix_sum));
472  digit_constraints.push_back(no_overflow);
473  }
474  sum=new_sum;
475 
476  const equal_exprt premise = length_eq(str, size);
477 
478  if(!digit_constraints.empty())
479  {
480  const implies_exprt a5(premise, conjunction(digit_constraints));
481  constraints.existential.push_back(a5);
482  }
483 
484  const implies_exprt a6(
485  and_exprt(premise, not_exprt(starts_with_minus)),
486  equal_exprt(input_int, sum));
487  constraints.existential.push_back(a6);
488 
489  const implies_exprt a7(
490  and_exprt(premise, starts_with_minus),
491  equal_exprt(input_int, unary_minus_exprt(sum)));
492  constraints.existential.push_back(a7);
493  }
494  return constraints;
495 }
496 
507 std::pair<exprt, string_constraintst> add_axioms_for_parse_int(
508  symbol_generatort &fresh_symbol,
510  array_poolt &array_pool,
511  const namespacet &ns)
512 {
513  PRECONDITION(f.arguments().size()==1 || f.arguments().size()==2);
514  const array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]);
515  const typet &type=f.type();
516  PRECONDITION(type.id()==ID_signedbv);
517  const exprt radix=f.arguments().size()==1?
518  static_cast<exprt>(from_integer(10, type)):
519  static_cast<exprt>(typecast_exprt(f.arguments()[1], type));
520  // Most of the time we can evaluate radix as an integer. The value 0 is used
521  // to indicate when we can't tell what the radix is.
522  const unsigned long radix_ul = to_integer_or_default(radix, 0, ns);
523  PRECONDITION((radix_ul>=2 && radix_ul<=36) || radix_ul==0);
524 
525  const symbol_exprt input_int=fresh_symbol("parsed_int", type);
526  const typet &char_type = str.content().type().subtype();
527  const typecast_exprt radix_as_char(radix, char_type);
528  const bool strict_formatting=false;
529 
530  const std::size_t max_string_length=max_printed_string_length(type, radix_ul);
531 
536  auto constraints1 = add_axioms_for_correct_number_format(
537  str, radix_as_char, radix_ul, max_string_length, strict_formatting);
538 
540  input_int,
541  type,
542  strict_formatting,
543  str,
544  max_string_length,
545  radix,
546  radix_ul);
547  merge(constraints2, std::move(constraints1));
548 
549  return {input_int, std::move(constraints2)};
550 }
551 
561  const exprt &chr,
562  const bool strict_formatting,
563  const exprt &radix_as_char,
564  const unsigned long radix_ul)
565 {
566  PRECONDITION((radix_ul>=2 && radix_ul<=36) || radix_ul==0);
567  const typet &char_type=chr.type();
568  const exprt zero_char=from_integer('0', char_type);
569 
570  const and_exprt is_digit_when_radix_le_10(
571  binary_relation_exprt(chr, ID_ge, zero_char),
573  chr, ID_lt, plus_exprt(zero_char, radix_as_char)));
574 
575  if(radix_ul<=10 && radix_ul!=0)
576  {
577  return is_digit_when_radix_le_10;
578  }
579  else
580  {
581  const exprt nine_char=from_integer('9', char_type);
582  const exprt a_char=from_integer('a', char_type);
583  const constant_exprt ten_char_type=from_integer(10, char_type);
584 
585  const minus_exprt radix_minus_ten(radix_as_char, ten_char_type);
586 
587  or_exprt is_digit_when_radix_gt_10(
588  and_exprt(
589  binary_relation_exprt(chr, ID_ge, zero_char),
590  binary_relation_exprt(chr, ID_le, nine_char)),
591  and_exprt(
592  binary_relation_exprt(chr, ID_ge, a_char),
594  chr, ID_lt, plus_exprt(a_char, radix_minus_ten))));
595 
596  if(!strict_formatting)
597  {
598  exprt A_char=from_integer('A', char_type);
599  is_digit_when_radix_gt_10.copy_to_operands(
600  and_exprt(
601  binary_relation_exprt(chr, ID_ge, A_char),
603  chr, ID_lt, plus_exprt(A_char, radix_minus_ten))));
604  }
605 
606  if(radix_ul==0)
607  {
608  return if_exprt(
609  binary_relation_exprt(radix_as_char, ID_le, ten_char_type),
610  is_digit_when_radix_le_10,
611  is_digit_when_radix_gt_10);
612  }
613  else
614  {
615  return std::move(is_digit_when_radix_gt_10);
616  }
617  }
618 }
619 
631  const exprt &chr,
632  const typet &char_type,
633  const typet &type,
634  const bool strict_formatting,
635  const unsigned long radix_ul)
636 {
637  const constant_exprt zero_char=from_integer('0', char_type);
638 
641  const binary_relation_exprt upper_case_lower_case_or_digit(
642  chr, ID_ge, zero_char);
643 
644  if(radix_ul<=10 && radix_ul!=0)
645  {
647  return typecast_exprt(
648  if_exprt(
649  upper_case_lower_case_or_digit,
650  minus_exprt(chr, zero_char),
651  from_integer(0, char_type)),
652  type);
653  }
654  else
655  {
656  const constant_exprt a_char=from_integer('a', char_type);
657  const binary_relation_exprt lower_case(chr, ID_ge, a_char);
658  const constant_exprt A_char=from_integer('A', char_type);
659  const binary_relation_exprt upper_case_or_lower_case(chr, ID_ge, A_char);
660  const constant_exprt ten_int=from_integer(10, char_type);
661 
662  if(strict_formatting)
663  {
666  return typecast_exprt(
667  if_exprt(
668  lower_case,
669  plus_exprt(minus_exprt(chr, a_char), ten_int),
670  if_exprt(
671  upper_case_lower_case_or_digit,
672  minus_exprt(chr, zero_char),
673  from_integer(0, char_type))),
674  type);
675  }
676  else
677  {
681  return typecast_exprt(
682  if_exprt(
683  lower_case,
684  plus_exprt(minus_exprt(chr, a_char), ten_int),
685  if_exprt(
686  upper_case_or_lower_case,
687  plus_exprt(minus_exprt(chr, A_char), ten_int),
688  if_exprt(
689  upper_case_lower_case_or_digit,
690  minus_exprt(chr, zero_char),
691  from_integer(0, char_type)))),
692  type);
693  }
694  }
695 }
696 
704 size_t max_printed_string_length(const typet &type, unsigned long radix_ul)
705 {
706  if(radix_ul==0)
707  {
708  radix_ul=2;
709  }
710  double n_bits=static_cast<double>(to_bitvector_type(type).get_width());
711  double radix=static_cast<double>(radix_ul);
712  bool signed_type=type.id()==ID_signedbv;
731  double max=signed_type?
732  floor(static_cast<double>(n_bits-1)/log2(radix))+2.0:
733  ceil(static_cast<double>(n_bits)/log2(radix));
734  return static_cast<size_t>(max);
735 }
The type of an expression, extends irept.
Definition: type.h:27
Boolean negation.
Definition: std_expr.h:3308
binary_relation_exprt length_ge(const T &lhs, const exprt &rhs)
Definition: string_expr.h:21
Semantic type conversion.
Definition: std_expr.h:2277
std::pair< exprt, string_constraintst > add_axioms_from_bool(const function_application_exprt &f, array_poolt &array_pool)
Add axioms corresponding to the String.valueOf(Z) java function.
Generates string constraints to link results from string functions with their arguments.
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
Application of (mathematical) function.
Definition: std_expr.h:4481
Boolean OR.
Definition: std_expr.h:2531
exprt simplify_expr(const exprt &src, const namespacet &ns)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1158
static exprt int_of_hex_char(const exprt &chr)
Returns the integer value represented by the character.
string_constraintst add_axioms_for_correct_number_format(const array_string_exprt &str, const exprt &radix_as_char, const unsigned long radix_ul, const std::size_t max_size, const bool strict_formatting)
Add axioms making the return value true if the given string is a correct number in the given radix.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:123
Generation of fresh symbols of a given type.
argumentst & arguments()
Definition: std_expr.h:4506
The trinary if-then-else operator.
Definition: std_expr.h:3427
typet & type()
Return the type of the expression.
Definition: expr.h:68
signedbv_typet get_return_code_type()
The Boolean type.
Definition: std_types.h:28
A constant literal expression.
Definition: std_expr.h:4384
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
Correspondance between arrays and pointers string representations.
Collection of constraints of different types: existential formulas, universal formulas,...
Boolean implication.
Definition: std_expr.h:2485
Equality.
Definition: std_expr.h:1484
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:50
const irep_idt & id() const
Definition: irep.h:259
array_string_exprt get_string_expr(array_poolt &pool, const exprt &expr)
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbo...
exprt & content()
Definition: string_expr.h:80
The Boolean constant true.
Definition: std_expr.h:4443
Division.
Definition: std_expr.h:1211
static unsigned long to_integer_or_default(const exprt &expr, unsigned long def, const namespacet &ns)
If the expression is a constant expression then we get the value of it as an unsigned long.
size_t max_printed_string_length(const typet &type, unsigned long radix_ul)
Calculate the string length needed to represent any value of the given type using the given radix.
Boolean AND.
Definition: std_expr.h:2409
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
std::pair< exprt, string_constraintst > add_axioms_from_char(const function_application_exprt &f, array_poolt &array_pool)
Conversion from char to string.
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
binary_relation_exprt length_gt(const T &lhs, const exprt &rhs)
Definition: string_expr.h:28
exprt is_digit_with_radix(const exprt &chr, const bool strict_formatting, const exprt &radix_as_char, const unsigned long radix_ul)
Check if a character is a digit with respect to the given radix, e.g.
bitvector_typet index_type()
Definition: c_types.cpp:16
The unary minus expression.
Definition: std_expr.h:469
string_constraintst add_axioms_for_characters_in_integer_string(const exprt &input_int, const typet &type, const bool strict_formatting, const array_string_exprt &str, const std::size_t max_string_length, const exprt &radix, const unsigned long radix_ul)
Add axioms connecting the characters in the input string to the value of the output integer.
std::vector< exprt > operandst
Definition: expr.h:57
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1159
#define DEPRECATED(msg)
Definition: deprecate.h:23
std::vector< exprt > existential
exprt & length()
Definition: string_expr.h:70
equal_exprt length_eq(const T &lhs, const exprt &rhs)
Definition: string_expr.h:54
const array_string_exprt & char_array_of_pointer(array_poolt &pool, const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
Base class for all expressions.
Definition: expr.h:54
std::pair< exprt, string_constraintst > add_axioms_for_string_of_int_with_radix(const array_string_exprt &res, const exprt &input_int, const exprt &radix, size_t max_size, const namespacet &ns)
Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String....
exprt get_numeric_value_from_character(const exprt &chr, const typet &char_type, const typet &type, const bool strict_formatting, const unsigned long radix_ul)
Get the numeric value of a character, assuming that the radix is large enough.
std::pair< exprt, string_constraintst > add_axioms_for_string_of_int(const array_string_exprt &res, const exprt &input_int, size_t max_size, const namespacet &ns)
Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String....
Binary minus.
Definition: std_expr.h:1106
Expression to hold a symbol (variable)
Definition: std_expr.h:143
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
std::pair< exprt, string_constraintst > add_axioms_from_long(const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
Add axioms corresponding to the String.valueOf(J) java function.
std::pair< exprt, string_constraintst > add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i)
Add axioms stating that the string res corresponds to the integer argument written in hexadecimal.
const typet & subtype() const
Definition: type.h:38
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
binary_relation_exprt length_le(const T &lhs, const exprt &rhs)
Definition: string_expr.h:41
std::pair< exprt, string_constraintst > add_axioms_for_parse_int(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
Integer value represented by a string.
bitvector_typet char_type()
Definition: c_types.cpp:114