CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
convert_int_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
12#include "convert_int_literal.h"
15
16#include <util/arith_tools.h>
18
19#include <stdexcept>
20
22#define STL_INT_MAX_VALUE 32767LL
24#define STL_INT_MIN_VALUE -32768LL
26#define BASE_10 10u
28#define BASE_16 16u
30#define BASE_2 2u
32#define PREFIX_SEPARATOR '#'
34#define OUT_OF_RANGE_MSG "Int literal out of range"
35
36static long long get_literal_value(const std::string &src, unsigned int base)
37{
38 std::string::size_type offset = src.find_last_of(PREFIX_SEPARATOR);
39 if(offset == std::string::npos)
40 offset = 0u;
41 else
42 ++offset;
43 const std::string literal{src.substr(offset)};
44 return std::stoll(literal, nullptr, base);
45}
46
48{
49 long long literal_value;
50 try
51 {
53 }
54 catch(std::out_of_range &)
55 {
56 throw std::out_of_range{OUT_OF_RANGE_MSG};
57 }
60 else
62}
63
65{
66 long long literal_value;
67 try
68 {
70 }
71 catch(std::out_of_range &)
72 {
73 throw std::out_of_range{OUT_OF_RANGE_MSG};
74 }
77 else
78 throw std::out_of_range{OUT_OF_RANGE_MSG};
79}
80
82{
83 long long literal_value;
84 try
85 {
87 }
88 catch(std::out_of_range &)
89 {
90 throw std::out_of_range{OUT_OF_RANGE_MSG};
91 }
94 else
96}
97
99{
100 long long literal_value;
101 try
102 {
104 }
105 catch(std::out_of_range &)
106 {
107 throw std::out_of_range{OUT_OF_RANGE_MSG};
108 }
111 else
112 throw std::out_of_range{OUT_OF_RANGE_MSG};
113}
114
116{
117 long long literal_value;
118 try
119 {
121 }
122 catch(std::out_of_range &)
123 {
124 throw std::out_of_range{OUT_OF_RANGE_MSG};
125 }
128 else
130}
131
133{
134 long long literal_value;
135 try
136 {
138 }
139 catch(std::out_of_range &)
140 {
141 throw std::out_of_range{OUT_OF_RANGE_MSG};
142 }
145 else
146 throw std::out_of_range{OUT_OF_RANGE_MSG};
147}
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
constant_exprt convert_dint_bit_literal_value(const std::string &src)
Converts a string into the corresponding 'DInt' expression.
constant_exprt convert_dint_dec_literal_value(const std::string &src)
Converts a string into the corresponding 'DInt' expression.
constant_exprt convert_dint_hex_literal_value(const std::string &src)
Converts a string into the corresponding 'DInt' expression.
Statement List Language Conversion.
constant_exprt convert_int_hex_literal(const std::string &src)
Converts a string into the corresponding 'Int' or 'DInt' expression.
constant_exprt convert_int_bit_literal(const std::string &src)
Converts a string into the corresponding 'Int' or 'DInt' expression.
#define BASE_10
Base of decimal integer literals.
static long long get_literal_value(const std::string &src, unsigned int base)
constant_exprt convert_int_bit_literal_value(const std::string &src)
Converts a string into the corresponding 'Int' expression.
#define BASE_2
Base of binary integer literals.
#define BASE_16
Base of hexadecimal integer literals.
constant_exprt convert_int_dec_literal_value(const std::string &src)
Converts a string into the corresponding 'Int' expression.
constant_exprt convert_int_dec_literal(const std::string &src)
Converts a string into the corresponding 'Int' or 'DInt' expression.
#define OUT_OF_RANGE_MSG
Message for the case of a literal being out of range.
constant_exprt convert_int_hex_literal_value(const std::string &src)
Converts a string into the corresponding 'Int' expression.
#define PREFIX_SEPARATOR
Character between a prefix and another prefix or the actual literal.
Statement List Language Conversion.
signedbv_typet get_int_type()
Creates a new type that resembles the 'Int' type of the Siemens PLC languages.
Statement List Type Helper.