cprover
convert_character_literal.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C Language Conversion
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <cassert>
15 
16 #include <util/arith_tools.h>
17 #include <util/c_types.h>
18 #include <util/std_expr.h>
19 
20 #include "unescape_string.h"
21 
23  const std::string &src,
24  bool force_integer_type)
25 {
26  assert(src.size()>=2);
27 
28  exprt result;
29 
30  if(src[0]=='L' || src[0]=='u' || src[0]=='U')
31  {
32  assert(src[1]=='\'');
33  assert(src[src.size()-1]=='\'');
34 
35  std::basic_string<unsigned int> value=
36  unescape_wide_string(std::string(src, 2, src.size()-3));
37 
38  // L is wchar_t, u is char16_t, U is char32_t
39  typet type=wchar_t_type();
40 
41  if(value.empty())
42  throw "empty wide character literal";
43  else if(value.size()==1)
44  {
45  result=from_integer(value[0], type);
46  }
47  else if(value.size()>=2 && value.size()<=4)
48  {
49  // TODO: need to double-check. GCC seems to say that each
50  // character is wchar_t wide.
51  mp_integer x=0;
52 
53  for(unsigned i=0; i<value.size(); i++)
54  {
55  mp_integer z=(unsigned char)(value[i]);
56  z=z<<((value.size()-i-1)*8);
57  x+=z;
58  }
59 
60  // always wchar_t
61  result=from_integer(x, type);
62  }
63  else
64  throw "wide literals with "+std::to_string(value.size())+
65  " characters are not supported";
66  }
67  else
68  {
69  assert(src[0]=='\'');
70  assert(src[src.size()-1]=='\'');
71 
72  std::string value=
73  unescape_string(std::string(src, 1, src.size()-2));
74 
75  if(value.empty())
76  throw "empty character literal";
77  else if(value.size()==1)
78  {
79  typet type=force_integer_type?signed_int_type():char_type();
80  result=from_integer(value[0], type);
81  }
82  else if(value.size()>=2 && value.size()<=4)
83  {
84  mp_integer x=0;
85 
86  for(unsigned i=0; i<value.size(); i++)
87  {
88  mp_integer z=(unsigned char)(value[i]);
89  z=z<<((value.size()-i-1)*8);
90  x+=z;
91  }
92 
93  // always integer, never char!
94  result=from_integer(x, signed_int_type());
95  }
96  else
97  throw "literals with "+std::to_string(value.size())+
98  " characters are not supported";
99  }
100 
101  return result;
102 }
arith_tools.h
typet
The type of an expression, extends irept.
Definition: type.h:29
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
exprt
Base class for all expressions.
Definition: expr.h:53
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
signed_int_type
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
wchar_t_type
bitvector_typet wchar_t_type()
Definition: c_types.cpp:149
unescape_wide_string
std::basic_string< unsigned int > unescape_wide_string(const std::string &src)
Definition: unescape_string.cpp:156
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
unescape_string.h
ANSI-C Language Conversion.
convert_character_literal.h
C++ Language Conversion.
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
convert_character_literal
exprt convert_character_literal(const std::string &src, bool force_integer_type)
Definition: convert_character_literal.cpp:22
std_expr.h
API to expression classes.
unescape_string
std::string unescape_string(const std::string &src)
Definition: unescape_string.cpp:151
c_types.h