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_from_int(res, f.arguments()[2]);
38 }
39 
44 DEPRECATED("should use add_axioms_from_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_from_int_with_radix(
53  res, f.arguments()[2], f.arguments()[3]);
54  else
55  return add_axioms_from_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());
133  return add_axioms_from_int_with_radix(res, input_int, radix, max_size);
134 }
135 
146  const array_string_exprt &res,
147  const exprt &input_int,
148  const exprt &radix,
149  size_t max_size)
150 {
151  PRECONDITION(max_size < std::numeric_limits<size_t>::max());
152  const typet &type=input_int.type();
153  PRECONDITION(type.id()==ID_signedbv);
154 
157  const unsigned long radix_ul=to_integer_or_default(radix, 0);
158  CHECK_RETURN((radix_ul>=2 && radix_ul<=36) || radix_ul==0);
159 
160  if(max_size==0)
161  {
162  max_size=max_printed_string_length(type, radix_ul);
163  CHECK_RETURN(max_size<std::numeric_limits<size_t>::max());
164  }
165 
166  const typet &char_type = res.content().type().subtype();
167  const typecast_exprt radix_as_char(radix, char_type);
168  const typecast_exprt radix_input_type(radix, type);
169  const bool strict_formatting=true;
170 
172  input_int, res, radix_as_char, radix_ul, max_size, strict_formatting);
173 
175  input_int,
176  type,
177  strict_formatting,
178  res,
179  max_size,
180  radix_input_type,
181  radix_ul);
182 
183  return from_integer(0, signedbv_typet(32));
184 }
185 
191 {
192  exprt zero_char=constant_char('0', chr.type());
193  exprt nine_char=constant_char('9', chr.type());
194  exprt a_char=constant_char('a', chr.type());
195  return if_exprt(
196  binary_relation_exprt(chr, ID_gt, nine_char),
197  plus_exprt(constant_char(10, chr.type()), minus_exprt(chr, a_char)),
198  minus_exprt(chr, zero_char));
199 }
200 
207 DEPRECATED("use add_axioms_from_int which takes a radix argument instead")
208 exprt string_constraint_generatort::add_axioms_from_int_hex(
209  const array_string_exprt &res,
210  const exprt &i)
211 {
212  const typet &type=i.type();
213  PRECONDITION(type.id()==ID_signedbv);
214  const typet &index_type = res.length().type();
215  const typet &char_type = res.content().type().subtype();
216  exprt sixteen=from_integer(16, index_type);
217  exprt minus_char=constant_char('-', char_type);
218  exprt zero_char=constant_char('0', char_type);
219  exprt nine_char=constant_char('9', char_type);
220  exprt a_char=constant_char('a', char_type);
221  exprt f_char=constant_char('f', char_type);
222 
223  size_t max_size=8;
224  lemmas.push_back(
225  and_exprt(res.axiom_for_length_gt(0), res.axiom_for_length_le(max_size)));
226 
227  for(size_t size=1; size<=max_size; size++)
228  {
229  exprt sum=from_integer(0, type);
230  exprt all_numbers=true_exprt();
231  exprt chr=res[0];
232 
233  for(size_t j=0; j<size; j++)
234  {
235  chr=res[j];
236  exprt chr_int = int_of_hex_char(chr);
237  sum = plus_exprt(mult_exprt(sum, sixteen), typecast_exprt(chr_int, type));
239  and_exprt(
240  binary_relation_exprt(chr, ID_ge, zero_char),
241  binary_relation_exprt(chr, ID_le, nine_char)),
242  and_exprt(
243  binary_relation_exprt(chr, ID_ge, a_char),
244  binary_relation_exprt(chr, ID_le, f_char)));
245  all_numbers=and_exprt(all_numbers, is_number);
246  }
247 
248  equal_exprt premise(res.axiom_for_has_length(size));
249  lemmas.push_back(
250  implies_exprt(premise, and_exprt(equal_exprt(i, sum), all_numbers)));
251 
252  // disallow 0s at the beginning
253  if(size>1)
254  lemmas.push_back(
255  implies_exprt(premise, not_exprt(equal_exprt(res[0], zero_char))));
256  }
257  return from_integer(0, get_return_code_type());
258 }
259 
265 {
266  PRECONDITION(f.arguments().size() == 3);
267  const array_string_exprt res =
268  char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
269  return add_axioms_from_int_hex(res, f.arguments()[2]);
270 }
271 
276 // NOLINTNEXTLINE
284 {
285  PRECONDITION(f.arguments().size() == 3);
286  const array_string_exprt res =
287  char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
288  return add_axioms_from_char(res, f.arguments()[2]);
289 }
290 
299  const array_string_exprt &res,
300  const exprt &c)
301 {
302  and_exprt lemma(equal_exprt(res[0], c), res.axiom_for_has_length(1));
303  lemmas.push_back(lemma);
304  return from_integer(0, get_return_code_type());
305 }
306 
319  const exprt &input_int,
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  input_int,
519  str,
520  radix_as_char,
521  radix_ul,
522  max_string_length,
523  strict_formatting);
524 
526  input_int,
527  type,
528  strict_formatting,
529  str,
530  max_string_length,
531  radix,
532  radix_ul);
533 
534  return input_int;
535 }
536 
543  const exprt &expr, unsigned long def)
544 {
545  mp_integer mp_radix;
546  bool to_integer_failed=to_integer(simplify_expr(expr, ns), mp_radix);
547  return to_integer_failed?def:integer2ulong(mp_radix);
548 }
549 
559  const exprt &chr,
560  const bool strict_formatting,
561  const exprt &radix_as_char,
562  const unsigned long radix_ul)
563 {
564  PRECONDITION((radix_ul>=2 && radix_ul<=36) || radix_ul==0);
565  const typet &char_type=chr.type();
566  const exprt zero_char=from_integer('0', char_type);
567 
568  const and_exprt is_digit_when_radix_le_10(
569  binary_relation_exprt(chr, ID_ge, zero_char),
571  chr, ID_lt, plus_exprt(zero_char, radix_as_char)));
572 
573  if(radix_ul<=10 && radix_ul!=0)
574  {
575  return is_digit_when_radix_le_10;
576  }
577  else
578  {
579  const exprt nine_char=from_integer('9', char_type);
580  const exprt a_char=from_integer('a', char_type);
581  const constant_exprt ten_char_type=from_integer(10, char_type);
582 
583  const minus_exprt radix_minus_ten(radix_as_char, ten_char_type);
584 
585  or_exprt is_digit_when_radix_gt_10(
586  and_exprt(
587  binary_relation_exprt(chr, ID_ge, zero_char),
588  binary_relation_exprt(chr, ID_le, nine_char)),
589  and_exprt(
590  binary_relation_exprt(chr, ID_ge, a_char),
592  chr, ID_lt, plus_exprt(a_char, radix_minus_ten))));
593 
594  if(!strict_formatting)
595  {
596  exprt A_char=from_integer('A', char_type);
597  is_digit_when_radix_gt_10.copy_to_operands(
598  and_exprt(
599  binary_relation_exprt(chr, ID_ge, A_char),
601  chr, ID_lt, plus_exprt(A_char, radix_minus_ten))));
602  }
603 
604  if(radix_ul==0)
605  {
606  return if_exprt(
607  binary_relation_exprt(radix_as_char, ID_le, ten_char_type),
608  is_digit_when_radix_le_10,
609  is_digit_when_radix_gt_10);
610  }
611  else
612  {
613  return is_digit_when_radix_gt_10;
614  }
615  }
616 }
617 
629  const exprt &chr,
630  const typet &char_type,
631  const typet &type,
632  const bool strict_formatting,
633  const unsigned long radix_ul)
634 {
635  const constant_exprt zero_char=from_integer('0', char_type);
636 
639  const binary_relation_exprt upper_case_lower_case_or_digit(
640  chr, ID_ge, zero_char);
641 
642  if(radix_ul<=10 && radix_ul!=0)
643  {
645  return typecast_exprt(
646  if_exprt(
647  upper_case_lower_case_or_digit,
648  minus_exprt(chr, zero_char),
649  from_integer(0, char_type)),
650  type);
651  }
652  else
653  {
654  const constant_exprt a_char=from_integer('a', char_type);
655  const binary_relation_exprt lower_case(chr, ID_ge, a_char);
656  const constant_exprt A_char=from_integer('A', char_type);
657  const binary_relation_exprt upper_case_or_lower_case(chr, ID_ge, A_char);
658  const constant_exprt ten_int=from_integer(10, char_type);
659 
660  if(strict_formatting)
661  {
664  return typecast_exprt(
665  if_exprt(
666  lower_case,
667  plus_exprt(minus_exprt(chr, a_char), ten_int),
668  if_exprt(
669  upper_case_lower_case_or_digit,
670  minus_exprt(chr, zero_char),
671  from_integer(0, char_type))),
672  type);
673  }
674  else
675  {
679  return typecast_exprt(
680  if_exprt(
681  lower_case,
682  plus_exprt(minus_exprt(chr, a_char), ten_int),
683  if_exprt(
684  upper_case_or_lower_case,
685  plus_exprt(minus_exprt(chr, A_char), ten_int),
686  if_exprt(
687  upper_case_lower_case_or_digit,
688  minus_exprt(chr, zero_char),
689  from_integer(0, char_type)))),
690  type);
691  }
692  }
693 }
694 
702 size_t max_printed_string_length(const typet &type, unsigned long radix_ul)
703 {
704  if(radix_ul==0)
705  {
706  radix_ul=2;
707  }
708  double n_bits=static_cast<double>(to_bitvector_type(type).get_width());
709  double radix=static_cast<double>(radix_ul);
710  bool signed_type=type.id()==ID_signedbv;
729  double max=signed_type?
730  floor(static_cast<double>(n_bits-1)/log2(radix))+2.0:
731  ceil(static_cast<double>(n_bits)/log2(radix));
732  return static_cast<size_t>(max);
733 }
The type of an expression.
Definition: type.h:22
Boolean negation.
Definition: std_expr.h:3230
semantic type conversion
Definition: std_expr.h:2111
BigInt mp_integer
Definition: mp_arith.h:22
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:4531
boolean OR
Definition: std_expr.h:2391
exprt add_axioms_from_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...
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:1150
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:4564
The trinary if-then-else operator.
Definition: std_expr.h:3361
typet & type()
Definition: expr.h:56
The proper Booleans.
Definition: std_types.h:34
A constant literal expression.
Definition: std_expr.h:4424
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
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)
Add axioms stating that the string res corresponds to the integer argument written in hexadecimal...
const irep_idt & id() const
Definition: irep.h:189
The boolean constant true.
Definition: std_expr.h:4488
division (integer and real)
Definition: std_expr.h:1075
DEPRECATED("use instrument_cover_goals(goto_programt &goto_program," "const cover_instrumenterst &instrumenters," "message_handlert &message_handler, const irep_idt mode) instead") void instrument_cover_goals(const symbol_tablet &symbol_table
Instruments goto program for a given coverage criterion.
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:1262
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
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
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:1129
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
void add_axioms_for_correct_number_format(const exprt &input_int, 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...
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...