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