cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
12
#include "
convert_character_literal.h
"
13
14
#include <climits>
15
16
#include <
util/arith_tools.h
>
17
#include <
util/c_types.h
>
18
19
#include "
unescape_string.h
"
20
21
exprt
convert_character_literal
(
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<char32_t> 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
64
throw
invalid_source_file_exceptiont
{
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
99
throw
invalid_source_file_exceptiont
{
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
}
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition
arith_tools.cpp:99
arith_tools.h
signed_int_type
signedbv_typet signed_int_type()
Definition
c_types.cpp:22
char_type
bitvector_typet char_type()
Definition
c_types.cpp:106
wchar_t_type
bitvector_typet wchar_t_type()
Definition
c_types.cpp:141
c_types.h
exprt
Base class for all expressions.
Definition
expr.h:57
exprt::add_source_location
source_locationt & add_source_location()
Definition
expr.h:241
invalid_source_file_exceptiont
Thrown when we can't handle something in an input source file.
Definition
exception_utils.h:172
source_locationt
Definition
source_location.h:20
typet
The type of an expression, extends irept.
Definition
type.h:29
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
convert_character_literal.h
C++ Language Conversion.
mp_integer
BigInt mp_integer
Definition
smt_terms.h:17
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition
invariant.h:495
PRECONDITION
#define PRECONDITION(CONDITION)
Definition
invariant.h:463
unescape_wide_string
std::basic_string< char32_t > unescape_wide_string(const std::string &src)
Definition
unescape_string.cpp:155
unescape_string
std::string unescape_string(const std::string &src)
Definition
unescape_string.cpp:150
unescape_string.h
ANSI-C Language Conversion.
ansi-c
literals
convert_character_literal.cpp
Generated by
1.17.0