CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
convert_dint_literal.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Statement List Language Conversion
4
5Author: Matthias Weiss, matthias.weiss@diffblue.com
6
7\*******************************************************************/
8
11
14
15#include <util/arith_tools.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
45
51static 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
63{
64 try
65 {
66 const long long literal_value = get_literal_value(src, BASE_10);
68 }
69 catch(std::out_of_range &)
70 {
71 throw std::out_of_range{OUT_OF_RANGE_MSG};
72 }
73}
74
76{
77 try
78 {
79 const long long literal_value = get_literal_value(src, BASE_16);
81 }
82 catch(std::out_of_range &)
83 {
84 throw std::out_of_range{OUT_OF_RANGE_MSG};
85 }
86}
87
89{
90 try
91 {
92 const long long literal_value = get_literal_value(src, BASE_2);
94 }
95 catch(std::out_of_range &)
96 {
97 throw std::out_of_range{OUT_OF_RANGE_MSG};
98 }
99}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Pre-defined bitvector types.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A constant literal expression.
Definition std_expr.h:3117
#define BASE_10
Base of decimal double integer literals.
constant_exprt convert_dint_bit_literal_value(const std::string &src)
Converts a string into the corresponding 'DInt' expression.
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.
constant_exprt convert_dint_dec_literal_value(const std::string &src)
Converts a string into the corresponding 'DInt' expression.
#define BASE_2
Base of binary double integer literals.
static constant_exprt convert_dint_literal_value(const long long literal_value)
Converts the value of a literal the corresponding 'DInt' expression.
#define BASE_16
Base of hexadecimal double integer literals.
constant_exprt convert_dint_hex_literal_value(const std::string &src)
Converts a string into the corresponding 'DInt' expression.
#define OUT_OF_RANGE_MSG
Message for the case of a literal being out of range.
#define PREFIX_SEPARATOR
Character between a prefix and another prefix or the actual literal.
Statement List Language Conversion.
signedbv_typet get_dint_type()
Creates a new type that resembles the 'DInt' type of the Siemens PLC languages.
Statement List Type Helper.