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 
29 {
30  PRECONDITION(f.arguments().size() == 3 || f.arguments().size() == 4);
31  const array_string_exprt res =
33  if(f.arguments().size() == 4)
35  res, f.arguments()[2], f.arguments()[3]);
36  else // f.arguments.size()==3
37  return add_axioms_for_string_of_int(res, f.arguments()[2]);
38 }
39 
44 DEPRECATED("should use add_axioms_for_string_of_int instead")
45 exprt string_constraint_generatort::add_axioms_from_long(
47 {
48  PRECONDITION(f.arguments().size() == 3 || f.arguments().size() == 4);
49  const array_string_exprt res =
50  char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
51  if(f.arguments().size() == 4)
52  return add_axioms_for_string_of_int_with_radix(
53  res, f.arguments()[2], f.arguments()[3]);
54  else
55  return add_axioms_for_string_of_int(res, f.arguments()[2]);
56 }
57 
62 DEPRECATED("This is Java specific and should be implemented in Java instead")
63 exprt string_constraint_generatort::add_axioms_from_bool(
65 {
66  PRECONDITION(f.arguments().size() == 3);
67  const array_string_exprt res =
68  char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
69  return add_axioms_from_bool(res, f.arguments()[2]);
70 }
71 
78 DEPRECATED("This is Java specific and should be implemented in Java instead")
79 exprt string_constraint_generatort::add_axioms_from_bool(
80  const array_string_exprt &res,
81  const exprt &b)
82 {
83  const typet &char_type = res.content().type().subtype();
84  PRECONDITION(b.type()==bool_typet() || b.type().id()==ID_c_bool);
85 
86  typecast_exprt eq(b, bool_typet());
87 
88  // We add axioms:
89  // a1 : eq => res = |"true"|
90  // a2 : forall i < |"true"|. eq => res[i]="true"[i]
91  // a3 : !eq => res = |"false"|
92  // a4 : forall i < |"false"|. !eq => res[i]="false"[i]
93 
94  std::string str_true="true";
95  implies_exprt a1(eq, res.axiom_for_has_length(str_true.length()));
96  lemmas.push_back(a1);
97 
98  for(std::size_t i=0; i<str_true.length(); i++)
99  {
100  exprt chr=from_integer(str_true[i], char_type);
101  implies_exprt a2(eq, equal_exprt(res[i], chr));
102  lemmas.push_back(a2);
103  }
104 
105  std::string str_false="false";
106  implies_exprt a3(not_exprt(eq), res.axiom_for_has_length(str_false.length()));
107  lemmas.push_back(a3);
108 
109  for(std::size_t i=0; i<str_false.length(); i++)
110  {
111  exprt chr=from_integer(str_false[i], char_type);
112  implies_exprt a4(not_exprt(eq), equal_exprt(res[i], chr));
113  lemmas.push_back(a4);
114  }
115 
116  return from_integer(0, signedbv_typet(32));
117 }
118 
128  const array_string_exprt &res,
129  const exprt &input_int,
130  size_t max_size)
131 {
132  const constant_exprt radix=from_integer(10, input_int.type());
134  res, input_int, radix, max_size);
135 }
136 
147  const array_string_exprt &res,
148  const exprt &input_int,
149  const exprt &radix,
150  size_t max_size)
151 {
152  PRECONDITION(max_size < std::numeric_limits<size_t>::max());
153  const typet &type=input_int.type();
154  PRECONDITION(type.id()==ID_signedbv);
155 
158  const unsigned long radix_ul=to_integer_or_default(radix, 0);
159  CHECK_RETURN((radix_ul>=2 && radix_ul<=36) || radix_ul==0);
160 
161  if(max_size==0)
162  {
163  max_size=max_printed_string_length(type, radix_ul);
164  CHECK_RETURN(max_size<std::numeric_limits<size_t>::max());
165  }
166 
167  const typet &char_type = res.content().type().subtype();
168  const typecast_exprt radix_as_char(radix, char_type);
169  const typecast_exprt radix_input_type(radix, type);
170  const bool strict_formatting=true;
171 
173  res, radix_as_char, radix_ul, max_size, strict_formatting);
174 
176  input_int,
177  type,
178  strict_formatting,
179  res,
180  max_size,
181  radix_input_type,
182  radix_ul);
183 
184  return from_integer(0, signedbv_typet(32));
185 }
186 
192 {
193  exprt zero_char=constant_char('0', chr.type());
194  exprt nine_char=constant_char('9', chr.type());
195  exprt a_char=constant_char('a', chr.type());
196  return if_exprt(
197  binary_relation_exprt(chr, ID_gt, nine_char),
198  plus_exprt(constant_char(10, chr.type()), minus_exprt(chr, a_char)),
199  minus_exprt(chr, zero_char));
200 }
201 
209  "use add_axioms_for_string_of_int which takes a radix argument instead")
210 exprt string_constraint_generatort::add_axioms_from_int_hex(
211  const array_string_exprt &res,
212  const exprt &i)
213 {
214  const typet &type=i.type();
215  PRECONDITION(type.id()==ID_signedbv);
216  const typet &index_type = res.length().type();
217  const typet &char_type = res.content().type().subtype();
218  exprt sixteen=from_integer(16, index_type);
219  exprt minus_char=constant_char('-', char_type);
220  exprt zero_char=constant_char('0', char_type);
221  exprt nine_char=constant_char('9', char_type);
222  exprt a_char=constant_char('a', char_type);
223  exprt f_char=constant_char('f', char_type);
224 
225  size_t max_size=8;
226  lemmas.push_back(
227  and_exprt(res.axiom_for_length_gt(0), res.axiom_for_length_le(max_size)));
228 
229  for(size_t size=1; size<=max_size; size++)
230  {
231  exprt sum=from_integer(0, type);
232  exprt all_numbers=true_exprt();
233  exprt chr=res[0];
234 
235  for(size_t j=0; j<size; j++)
236  {
237  chr=res[j];
238  exprt chr_int = int_of_hex_char(chr);
239  sum = plus_exprt(mult_exprt(sum, sixteen), typecast_exprt(chr_int, type));
241  and_exprt(
242  binary_relation_exprt(chr, ID_ge, zero_char),
243  binary_relation_exprt(chr, ID_le, nine_char)),
244  and_exprt(
245  binary_relation_exprt(chr, ID_ge, a_char),
246  binary_relation_exprt(chr, ID_le, f_char)));
247  all_numbers=and_exprt(all_numbers, is_number);
248  }
249 
250  equal_exprt premise(res.axiom_for_has_length(size));
251  lemmas.push_back(
252  implies_exprt(premise, and_exprt(equal_exprt(i, sum), all_numbers)));
253 
254  // disallow 0s at the beginning
255  if(size>1)
256  lemmas.push_back(
257  implies_exprt(premise, not_exprt(equal_exprt(res[0], zero_char))));
258  }
259  return from_integer(0, get_return_code_type());
260 }
261 
267 {
268  PRECONDITION(f.arguments().size() == 3);
269  const array_string_exprt res =
270  char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
271  return add_axioms_from_int_hex(res, f.arguments()[2]);
272 }
273 
278 // NOLINTNEXTLINE
286 {
287  PRECONDITION(f.arguments().size() == 3);
288  const array_string_exprt res =
289  char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
290  return add_axioms_from_char(res, f.arguments()[2]);
291 }
292 
301  const array_string_exprt &res,
302  const exprt &c)
303 {
304  and_exprt lemma(equal_exprt(res[0], c), res.axiom_for_has_length(1));
305  lemmas.push_back(lemma);
306  return from_integer(0, get_return_code_type());
307 }
308 
320  const array_string_exprt &str,
321  const exprt &radix_as_char,
322  const unsigned long radix_ul,
323  const std::size_t max_size,
324  const bool strict_formatting)
325 {
326  const typet &char_type = str.content().type().subtype();
327  const typet &index_type = str.length().type();
328 
329  const exprt &chr=str[0];
330  const equal_exprt starts_with_minus(chr, constant_char('-', char_type));
331  const equal_exprt starts_with_plus(chr, constant_char('+', char_type));
332  const exprt starts_with_digit=
333  is_digit_with_radix(chr, strict_formatting, radix_as_char, radix_ul);
334 
335  // |str| > 0
336  const exprt non_empty=str.axiom_for_length_ge(from_integer(1, index_type));
337  lemmas.push_back(non_empty);
338 
339  if(strict_formatting)
340  {
341  // str[0] = '-' || is_digit_with_radix(str[0], radix)
342  const or_exprt correct_first(starts_with_minus, starts_with_digit);
343  lemmas.push_back(correct_first);
344  }
345  else
346  {
347  // str[0] = '-' || str[0] = '+' || is_digit_with_radix(str[0], radix)
348  const or_exprt correct_first(
349  starts_with_minus, starts_with_digit, starts_with_plus);
350  lemmas.push_back(correct_first);
351  }
352 
353  // str[0]='+' or '-' ==> |str| > 1
354  const implies_exprt contains_digit(
355  or_exprt(starts_with_minus, starts_with_plus),
357  lemmas.push_back(contains_digit);
358 
359  // |str| <= max_size
360  lemmas.push_back(str.axiom_for_length_le(max_size));
361 
362  // forall 1 <= i < |str| . is_digit_with_radix(str[i], radix)
363  // We unfold the above because we know that it will be used for all i up to
364  // str.length(), and str.length() <= max_size
365  for(std::size_t index=1; index<max_size; ++index)
366  {
368  const implies_exprt character_at_index_is_digit(
371  str[index], strict_formatting, radix_as_char, radix_ul));
372  lemmas.push_back(character_at_index_is_digit);
373  }
374 
375  if(strict_formatting)
376  {
377  const exprt zero_char=constant_char('0', char_type);
378 
379  // no_leading_zero : str[0] = '0' => |str| = 1
380  const implies_exprt no_leading_zero(
381  equal_exprt(chr, zero_char),
383  lemmas.push_back(no_leading_zero);
384 
385  // no_leading_zero_after_minus : str[0]='-' => str[1]!='0'
386  implies_exprt no_leading_zero_after_minus(
387  starts_with_minus, not_exprt(equal_exprt(str[1], zero_char)));
388  lemmas.push_back(no_leading_zero_after_minus);
389  }
390 }
391 
405  const exprt &input_int,
406  const typet &type,
407  const bool strict_formatting,
408  const array_string_exprt &str,
409  const std::size_t max_string_length,
410  const exprt &radix,
411  const unsigned long radix_ul)
412 {
413  const typet &char_type = str.content().type().subtype();
414 
415  const equal_exprt starts_with_minus(str[0], constant_char('-', char_type));
416  const constant_exprt zero_expr=from_integer(0, type);
417  exprt::operandst digit_constraints;
418 
420  str[0], char_type, type, strict_formatting, radix_ul);
421 
425  lemmas.push_back(
426  implies_exprt(str.axiom_for_has_length(1), equal_exprt(input_int, sum)));
427 
428  for(size_t size=2; size<=max_string_length; size++)
429  {
430  // sum_0 := numeric value of res[0] (which is 0 if res[0] is '-')
431  // For each 1<=j<max_string_length, we have:
432  // sum_j := radix * sum_{j-1} + numeric value of res[j]
433  // no_overflow_j := sum_{j-1} == (radix * sum_{j-1} / radix)
434  // && sum_j >= sum_{j - 1}
435  // (the first part avoid overflows in the multiplication and the second
436  // one in the addition of the definition of sum_j)
437  // For all 1<=size<=max_string_length we add axioms:
438  // a5 : |res| == size =>
439  // forall max_string_length-2 <= j < size. no_overflow_j
440  // a6 : |res| == size && res[0] is a digit for radix =>
441  // input_int == sum_{size-1}
442  // a7 : |res| == size && res[0] == '-' => input_int == -sum_{size-1}
443 
444  const mult_exprt radix_sum(sum, radix);
445  // new_sum = radix * sum + (numeric value of res[j])
446  const exprt new_sum=plus_exprt(
447  radix_sum,
449  str[size-1], char_type, type, strict_formatting, radix_ul));
450 
451  // An overflow can happen when reaching the last index which can contain
452  // a digit, which is `max_string_length - 2` because of the space left for
453  // a minus sign. That assumes that we were able to identify the radix. If we
454  // weren't then we check for overflow on every index.
455  if(size-1>=max_string_length-2 || radix_ul==0)
456  {
457  const and_exprt no_overflow(
458  equal_exprt(sum, div_exprt(radix_sum, radix)),
459  binary_relation_exprt(new_sum, ID_ge, radix_sum));
460  digit_constraints.push_back(no_overflow);
461  }
462  sum=new_sum;
463 
464  const equal_exprt premise=str.axiom_for_has_length(size);
465 
466  if(!digit_constraints.empty())
467  {
468  const implies_exprt a5(premise, conjunction(digit_constraints));
469  lemmas.push_back(a5);
470  }
471 
472  const implies_exprt a6(
473  and_exprt(premise, not_exprt(starts_with_minus)),
474  equal_exprt(input_int, sum));
475  lemmas.push_back(a6);
476 
477  const implies_exprt a7(
478  and_exprt(premise, starts_with_minus),
479  equal_exprt(input_int, unary_minus_exprt(sum)));
480  lemmas.push_back(a7);
481  }
482 }
483 
493 {
494  PRECONDITION(f.arguments().size()==1 || f.arguments().size()==2);
495  const array_string_exprt str = get_string_expr(f.arguments()[0]);
496  const typet &type=f.type();
497  PRECONDITION(type.id()==ID_signedbv);
498  const exprt radix=f.arguments().size()==1?
499  static_cast<exprt>(from_integer(10, type)):
500  static_cast<exprt>(typecast_exprt(f.arguments()[1], type));
501  // Most of the time we can evaluate radix as an integer. The value 0 is used
502  // to indicate when we can't tell what the radix is.
503  const unsigned long radix_ul=to_integer_or_default(radix, 0);
504  PRECONDITION((radix_ul>=2 && radix_ul<=36) || radix_ul==0);
505 
506  const symbol_exprt input_int=fresh_symbol("parsed_int", type);
507  const typet &char_type = str.content().type().subtype();
508  const typecast_exprt radix_as_char(radix, char_type);
509  const bool strict_formatting=false;
510 
511  const std::size_t max_string_length=max_printed_string_length(type, radix_ul);
512 
518  str,
519  radix_as_char,
520  radix_ul,
521  max_string_length,
522  strict_formatting);
523 
525  input_int,
526  type,
527  strict_formatting,
528  str,
529  max_string_length,
530  radix,
531  radix_ul);
532 
533  return input_int;
534 }
535 
542  const exprt &expr, unsigned long def)
543 {
544  mp_integer mp_radix;
545  bool to_integer_failed=to_integer(simplify_expr(expr, ns), mp_radix);
546  return to_integer_failed?def:integer2ulong(mp_radix);
547 }
548 
558  const exprt &chr,
559  const bool strict_formatting,
560  const exprt &radix_as_char,
561  const unsigned long radix_ul)
562 {
563  PRECONDITION((radix_ul>=2 && radix_ul<=36) || radix_ul==0);
564  const typet &char_type=chr.type();
565  const exprt zero_char=from_integer('0', char_type);
566 
567  const and_exprt is_digit_when_radix_le_10(
568  binary_relation_exprt(chr, ID_ge, zero_char),
570  chr, ID_lt, plus_exprt(zero_char, radix_as_char)));
571 
572  if(radix_ul<=10 && radix_ul!=0)
573  {
574  return is_digit_when_radix_le_10;
575  }
576  else
577  {
578  const exprt nine_char=from_integer('9', char_type);
579  const exprt a_char=from_integer('a', char_type);
580  const constant_exprt ten_char_type=from_integer(10, char_type);
581 
582  const minus_exprt radix_minus_ten(radix_as_char, ten_char_type);
583 
584  or_exprt is_digit_when_radix_gt_10(
585  and_exprt(
586  binary_relation_exprt(chr, ID_ge, zero_char),
587  binary_relation_exprt(chr, ID_le, nine_char)),
588  and_exprt(
589  binary_relation_exprt(chr, ID_ge, a_char),
591  chr, ID_lt, plus_exprt(a_char, radix_minus_ten))));
592 
593  if(!strict_formatting)
594  {
595  exprt A_char=from_integer('A', char_type);
596  is_digit_when_radix_gt_10.copy_to_operands(
597  and_exprt(
598  binary_relation_exprt(chr, ID_ge, A_char),
600  chr, ID_lt, plus_exprt(A_char, radix_minus_ten))));
601  }
602 
603  if(radix_ul==0)
604  {
605  return if_exprt(
606  binary_relation_exprt(radix_as_char, ID_le, ten_char_type),
607  is_digit_when_radix_le_10,
608  is_digit_when_radix_gt_10);
609  }
610  else
611  {
612  return is_digit_when_radix_gt_10;
613  }
614  }
615 }
616 
628  const exprt &chr,
629  const typet &char_type,
630  const typet &type,
631  const bool strict_formatting,
632  const unsigned long radix_ul)
633 {
634  const constant_exprt zero_char=from_integer('0', char_type);
635 
638  const binary_relation_exprt upper_case_lower_case_or_digit(
639  chr, ID_ge, zero_char);
640 
641  if(radix_ul<=10 && radix_ul!=0)
642  {
644  return typecast_exprt(
645  if_exprt(
646  upper_case_lower_case_or_digit,
647  minus_exprt(chr, zero_char),
648  from_integer(0, char_type)),
649  type);
650  }
651  else
652  {
653  const constant_exprt a_char=from_integer('a', char_type);
654  const binary_relation_exprt lower_case(chr, ID_ge, a_char);
655  const constant_exprt A_char=from_integer('A', char_type);
656  const binary_relation_exprt upper_case_or_lower_case(chr, ID_ge, A_char);
657  const constant_exprt ten_int=from_integer(10, char_type);
658 
659  if(strict_formatting)
660  {
663  return typecast_exprt(
664  if_exprt(
665  lower_case,
666  plus_exprt(minus_exprt(chr, a_char), ten_int),
667  if_exprt(
668  upper_case_lower_case_or_digit,
669  minus_exprt(chr, zero_char),
670  from_integer(0, char_type))),
671  type);
672  }
673  else
674  {
678  return typecast_exprt(
679  if_exprt(
680  lower_case,
681  plus_exprt(minus_exprt(chr, a_char), ten_int),
682  if_exprt(
683  upper_case_or_lower_case,
684  plus_exprt(minus_exprt(chr, A_char), ten_int),
685  if_exprt(
686  upper_case_lower_case_or_digit,
687  minus_exprt(chr, zero_char),
688  from_integer(0, char_type)))),
689  type);
690  }
691  }
692 }
693 
701 size_t max_printed_string_length(const typet &type, unsigned long radix_ul)
702 {
703  if(radix_ul==0)
704  {
705  radix_ul=2;
706  }
707  double n_bits=static_cast<double>(to_bitvector_type(type).get_width());
708  double radix=static_cast<double>(radix_ul);
709  bool signed_type=type.id()==ID_signedbv;
728  double max=signed_type?
729  floor(static_cast<double>(n_bits-1)/log2(radix))+2.0:
730  ceil(static_cast<double>(n_bits)/log2(radix));
731  return static_cast<size_t>(max);
732 }
The type of an expression.
Definition: type.h:22
Boolean negation.
Definition: std_expr.h:3228
semantic type conversion
Definition: std_expr.h:2111
BigInt mp_integer
Definition: mp_arith.h:22
void 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...
Generates string constraints to link results from string functions with their arguments.
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
binary_relation_exprt axiom_for_length_ge(const string_exprt &rhs) const
Definition: string_expr.h:57
void 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...
application of (mathematical) function
Definition: std_expr.h:4529
boolean OR
Definition: std_expr.h:2391
exprt simplify_expr(const exprt &src, const namespacet &ns)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1159
exprt add_axioms_from_int(const function_application_exprt &f)
Convert an integer to a string.
mp_integer::ullong_t integer2ulong(const mp_integer &n)
Definition: mp_arith.cpp:189
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
equal_exprt axiom_for_has_length(const exprt &rhs) const
Definition: string_expr.h:125
argumentst & arguments()
Definition: std_expr.h:4562
The trinary if-then-else operator.
Definition: std_expr.h:3359
typet & type()
Definition: expr.h:56
The proper Booleans.
Definition: std_types.h:34
A constant literal expression.
Definition: std_expr.h:4422
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:266
boolean implication
Definition: std_expr.h:2339
equality
Definition: std_expr.h:1354
exprt conjunction(const exprt::operandst &op)
Definition: std_expr.cpp:48
exprt add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i)
exprt add_axioms_for_string_of_int_with_radix(const array_string_exprt &res, const exprt &input_int, const exprt &radix, size_t max_size=0)
Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String...
const irep_idt & id() const
Definition: irep.h:259
The boolean constant true.
Definition: std_expr.h:4486
division (integer and real)
Definition: std_expr.h:1075
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...
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1271
exprt add_axioms_for_parse_int(const function_application_exprt &f)
Integer value represented by a string.
boolean AND
Definition: std_expr.h:2255
binary_relation_exprt axiom_for_length_le(const string_exprt &rhs) const
Definition: string_expr.h:88
exprt add_axioms_for_string_of_int(const array_string_exprt &res, const exprt &input_int, size_t max_size=0)
Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String...
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
The plus expression.
Definition: std_expr.h:893
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:444
std::size_t get_width() const
Definition: std_types.h:1138
std::vector< exprt > operandst
Definition: expr.h:45
binary multiplication
Definition: std_expr.h:1017
unsigned long to_integer_or_default(const exprt &expr, unsigned long def)
If the expression is a constant expression then we get the value of it as an unsigned long...
static constant_exprt constant_char(int i, const typet &char_type)
generate constant character expression with character type.
bool is_number(const typet &type)
Definition: type.cpp:25
Base class for all expressions.
Definition: expr.h:42
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.
binary minus
Definition: std_expr.h:959
Expression to hold a symbol (variable)
Definition: std_expr.h:90
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
DEPRECATED("use add_axioms_for_string_of_int which takes a radix argument instead") exprt string_constraint_generatort
Add axioms stating that the string res corresponds to the integer argument written in hexadecimal...
const array_string_exprt & char_array_of_pointer(const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
const typet & subtype() const
Definition: type.h:33
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
exprt add_axioms_from_char(const function_application_exprt &f)
Conversion from char to string.
static exprt int_of_hex_char(const exprt &chr)
Returns the integer value represented by the character.
bitvector_typet char_type()
Definition: c_types.cpp:114
array_string_exprt get_string_expr(const exprt &expr)
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbo...