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  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  // 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  assert(src[0]=='\'');
72  assert(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 }
mp_integer
BigInt mp_integer
Definition: smt_terms.h:17
arith_tools.h
convert_character_literal
exprt convert_character_literal(const std::string &src, bool force_integer_type, const source_locationt &source_location)
Definition: convert_character_literal.cpp:21
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
typet
The type of an expression, extends irept.
Definition: type.h:28
exprt
Base class for all expressions.
Definition: expr.h:55
invalid_source_file_exceptiont
Thrown when we can't handle something in an input source file.
Definition: exception_utils.h:171
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:58
signed_int_type
signedbv_typet signed_int_type()
Definition: c_types.cpp:40
wchar_t_type
bitvector_typet wchar_t_type()
Definition: c_types.cpp:159
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:124
source_locationt
Definition: source_location.h:18
unescape_string.h
convert_character_literal.h
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:100
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:216
unescape_string
std::string unescape_string(const std::string &src)
Definition: unescape_string.cpp:151
c_types.h