CBMC
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  const source_locationt &source_location)
25 {
26  PRECONDITION(src.size() >= 2);
27 
28  exprt result;
29 
30  if(src[0]=='L' || src[0]=='u' || src[0]=='U')
31  {
32  PRECONDITION(src[1] == '\'');
33  PRECONDITION(src[src.size() - 1] == '\'');
34 
35  std::basic_string<unsigned int> value=
36  unescape_wide_string(std::string(src, 2, src.size()-3));
37  // the parser rejects empty character constants
38  CHECK_RETURN(!value.empty());
39 
40  // L is wchar_t, u is char16_t, U is char32_t
41  typet type=wchar_t_type();
42 
43  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) * CHAR_BIT);
57  x+=z;
58  }
59 
60  // always wchar_t
61  result=from_integer(x, type);
62  }
63  else
65  "wide literals with " + std::to_string(value.size()) +
66  " characters are not supported",
67  source_location};
68  }
69  else
70  {
71  PRECONDITION(src[0] == '\'');
72  PRECONDITION(src[src.size() - 1] == '\'');
73 
74  std::string value=
75  unescape_string(std::string(src, 1, src.size()-2));
76  // the parser rejects empty character constants
77  CHECK_RETURN(!value.empty());
78 
79  if(value.size() == 1)
80  {
81  typet type=force_integer_type?signed_int_type():char_type();
82  result=from_integer(value[0], type);
83  }
84  else if(value.size()>=2 && value.size()<=4)
85  {
86  mp_integer x=0;
87 
88  for(unsigned i=0; i<value.size(); i++)
89  {
90  mp_integer z=(unsigned char)(value[i]);
91  z = z << ((value.size() - i - 1) * CHAR_BIT);
92  x+=z;
93  }
94 
95  // always integer, never char!
96  result=from_integer(x, signed_int_type());
97  }
98  else
100  "literals with " + std::to_string(value.size()) +
101  " characters are not supported",
102  source_location};
103  }
104 
105  result.add_source_location() = source_location;
106  return result;
107 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
signedbv_typet signed_int_type()
Definition: c_types.cpp:22
bitvector_typet char_type()
Definition: c_types.cpp:106
bitvector_typet wchar_t_type()
Definition: c_types.cpp:141
Base class for all expressions.
Definition: expr.h:56
source_locationt & add_source_location()
Definition: expr.h:236
Thrown when we can't handle something in an input source file.
The type of an expression, extends irept.
Definition: type.h:29
exprt convert_character_literal(const std::string &src, bool force_integer_type, const source_locationt &source_location)
C++ Language Conversion.
BigInt mp_integer
Definition: smt_terms.h:17
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
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.