cprover
Loading...
Searching...
No Matches
convert_character_literal.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C Language Conversion
4
5Author: 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)
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::basic_string< unsigned int > unescape_wide_string(const std::string &src)
std::string unescape_string(const std::string &src)
ANSI-C Language Conversion.