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