cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
convert_dint_literal.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Statement List Language Conversion
4
5
Author: Matthias Weiss, matthias.weiss@diffblue.com
6
7
\*******************************************************************/
8
11
12
#include "
convert_dint_literal.h
"
13
#include "
statement_list_types.h
"
14
15
#include <
util/arith_tools.h
>
16
#include <
util/bitvector_types.h
>
17
18
#include <stdexcept>
19
21
#define STL_DINT_MAX_VALUE 2147483647LL
23
#define STL_DINT_MIN_VALUE -2147483648LL
25
#define BASE_10 10u
27
#define BASE_16 16u
29
#define BASE_2 2u
31
#define PREFIX_SEPARATOR '#'
33
#define OUT_OF_RANGE_MSG "DInt literal out of range"
34
38
static
constant_exprt
convert_dint_literal_value
(
const
long
long
literal_value)
39
{
40
if
(
STL_DINT_MIN_VALUE <= literal_value && STL_DINT_MAX_VALUE >
= literal_value)
41
return
from_integer
(literal_value,
get_dint_type
());
42
else
43
throw
std::out_of_range{
OUT_OF_RANGE_MSG
};
44
}
45
51
static
long
long
get_literal_value
(
const
std::string &src,
unsigned
int
base)
52
{
53
std::string::size_type offset = src.find_last_of(
PREFIX_SEPARATOR
);
54
if
(offset == std::string::npos)
55
offset = 0u;
56
else
57
++offset;
58
const
std::string literal{src.substr(offset)};
59
return
std::stoll(literal,
nullptr
, base);
60
}
61
62
constant_exprt
convert_dint_dec_literal_value
(
const
std::string &src)
63
{
64
try
65
{
66
const
long
long
literal_value =
get_literal_value
(src,
BASE_10
);
67
return
convert_dint_literal_value
(literal_value);
68
}
69
catch
(std::out_of_range &)
70
{
71
throw
std::out_of_range{
OUT_OF_RANGE_MSG
};
72
}
73
}
74
75
constant_exprt
convert_dint_hex_literal_value
(
const
std::string &src)
76
{
77
try
78
{
79
const
long
long
literal_value =
get_literal_value
(src,
BASE_16
);
80
return
convert_dint_literal_value
(literal_value);
81
}
82
catch
(std::out_of_range &)
83
{
84
throw
std::out_of_range{
OUT_OF_RANGE_MSG
};
85
}
86
}
87
88
constant_exprt
convert_dint_bit_literal_value
(
const
std::string &src)
89
{
90
try
91
{
92
const
long
long
literal_value =
get_literal_value
(src,
BASE_2
);
93
return
convert_dint_literal_value
(literal_value);
94
}
95
catch
(std::out_of_range &)
96
{
97
throw
std::out_of_range{
OUT_OF_RANGE_MSG
};
98
}
99
}
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition
arith_tools.cpp:99
arith_tools.h
bitvector_types.h
Pre-defined bitvector types.
constant_exprt
A constant literal expression.
Definition
std_expr.h:2997
BASE_10
#define BASE_10
Base of decimal double integer literals.
Definition
convert_dint_literal.cpp:25
convert_dint_bit_literal_value
constant_exprt convert_dint_bit_literal_value(const std::string &src)
Converts a string into the corresponding 'DInt' expression.
Definition
convert_dint_literal.cpp:88
get_literal_value
static long long get_literal_value(const std::string &src, unsigned int base)
Removes every prefix from the given string and converts the remaining string to a number.
Definition
convert_dint_literal.cpp:51
convert_dint_dec_literal_value
constant_exprt convert_dint_dec_literal_value(const std::string &src)
Converts a string into the corresponding 'DInt' expression.
Definition
convert_dint_literal.cpp:62
BASE_2
#define BASE_2
Base of binary double integer literals.
Definition
convert_dint_literal.cpp:29
convert_dint_literal_value
static constant_exprt convert_dint_literal_value(const long long literal_value)
Converts the value of a literal the corresponding 'DInt' expression.
Definition
convert_dint_literal.cpp:38
BASE_16
#define BASE_16
Base of hexadecimal double integer literals.
Definition
convert_dint_literal.cpp:27
convert_dint_hex_literal_value
constant_exprt convert_dint_hex_literal_value(const std::string &src)
Converts a string into the corresponding 'DInt' expression.
Definition
convert_dint_literal.cpp:75
OUT_OF_RANGE_MSG
#define OUT_OF_RANGE_MSG
Message for the case of a literal being out of range.
Definition
convert_dint_literal.cpp:33
STL_DINT_MIN_VALUE
#define STL_DINT_MIN_VALUE
Minimum value of double integer literals.
Definition
convert_dint_literal.cpp:23
PREFIX_SEPARATOR
#define PREFIX_SEPARATOR
Character between a prefix and another prefix or the actual literal.
Definition
convert_dint_literal.cpp:31
convert_dint_literal.h
Statement List Language Conversion.
get_dint_type
signedbv_typet get_dint_type()
Creates a new type that resembles the 'DInt' type of the Siemens PLC languages.
Definition
statement_list_types.cpp:21
statement_list_types.h
Statement List Type Helper.
statement-list
converters
convert_dint_literal.cpp
Generated by
1.17.0