cprover
convert_int_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_int_literal.h"
13 #include "convert_dint_literal.h"
14 #include "statement_list_types.h"
15 
16 #include <util/arith_tools.h>
17 #include <util/bitvector_types.h>
18 
19 #include <algorithm>
20 #include <stdexcept>
21 
23 #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"
36 
37 static long long get_literal_value(const std::string &src, unsigned int base)
38 {
39  std::string::size_type offset = src.find_last_of(PREFIX_SEPARATOR);
40  if(offset == std::string::npos)
41  offset = 0u;
42  else
43  ++offset;
44  const std::string literal{src.substr(offset)};
45  return std::stoll(literal, nullptr, base);
46 }
47 
48 constant_exprt convert_int_dec_literal(const std::string &src)
49 {
50  long long literal_value;
51  try
52  {
53  literal_value = get_literal_value(src, BASE_10);
54  }
55  catch(std::out_of_range &)
56  {
57  throw std::out_of_range{OUT_OF_RANGE_MSG};
58  }
59  if(STL_INT_MIN_VALUE <= literal_value && STL_INT_MAX_VALUE >= literal_value)
61  else
63 }
64 
66 {
67  long long literal_value;
68  try
69  {
70  literal_value = get_literal_value(src, BASE_10);
71  }
72  catch(std::out_of_range &)
73  {
74  throw std::out_of_range{OUT_OF_RANGE_MSG};
75  }
76  if(STL_INT_MIN_VALUE <= literal_value && STL_INT_MAX_VALUE >= literal_value)
77  return from_integer(literal_value, get_int_type());
78  else
79  throw std::out_of_range{OUT_OF_RANGE_MSG};
80 }
81 
82 constant_exprt convert_int_hex_literal(const std::string &src)
83 {
84  long long literal_value;
85  try
86  {
87  literal_value = get_literal_value(src, BASE_16);
88  }
89  catch(std::out_of_range &)
90  {
91  throw std::out_of_range{OUT_OF_RANGE_MSG};
92  }
93  if(STL_INT_MIN_VALUE <= literal_value && STL_INT_MAX_VALUE >= literal_value)
95  else
97 }
98 
100 {
101  long long literal_value;
102  try
103  {
104  literal_value = get_literal_value(src, BASE_16);
105  }
106  catch(std::out_of_range &)
107  {
108  throw std::out_of_range{OUT_OF_RANGE_MSG};
109  }
110  if(STL_INT_MIN_VALUE <= literal_value && STL_INT_MAX_VALUE >= literal_value)
111  return from_integer(literal_value, get_int_type());
112  else
113  throw std::out_of_range{OUT_OF_RANGE_MSG};
114 }
115 
117 {
118  long long literal_value;
119  try
120  {
121  literal_value = get_literal_value(src, BASE_2);
122  }
123  catch(std::out_of_range &)
124  {
125  throw std::out_of_range{OUT_OF_RANGE_MSG};
126  }
127  if(STL_INT_MIN_VALUE <= literal_value && STL_INT_MAX_VALUE >= literal_value)
128  return convert_int_bit_literal_value(src);
129  else
130  return convert_dint_bit_literal_value(src);
131 }
132 
134 {
135  long long literal_value;
136  try
137  {
138  literal_value = get_literal_value(src, BASE_2);
139  }
140  catch(std::out_of_range &)
141  {
142  throw std::out_of_range{OUT_OF_RANGE_MSG};
143  }
144  if(STL_INT_MIN_VALUE <= literal_value && STL_INT_MAX_VALUE >= literal_value)
145  return from_integer(literal_value, get_int_type());
146  else
147  throw std::out_of_range{OUT_OF_RANGE_MSG};
148 }
BASE_16
#define BASE_16
Base of hexadecimal integer literals.
Definition: convert_int_literal.cpp:29
arith_tools.h
BASE_2
#define BASE_2
Base of binary integer literals.
Definition: convert_int_literal.cpp:31
get_literal_value
static long long get_literal_value(const std::string &src, unsigned int base)
Definition: convert_int_literal.cpp:37
OUT_OF_RANGE_MSG
#define OUT_OF_RANGE_MSG
Message for the case of a literal being out of range.
Definition: convert_int_literal.cpp:35
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:63
convert_int_dec_literal_value
constant_exprt convert_int_dec_literal_value(const std::string &src)
Converts a string into the corresponding 'Int' expression.
Definition: convert_int_literal.cpp:65
convert_int_literal.h
Statement List Language Conversion.
PREFIX_SEPARATOR
#define PREFIX_SEPARATOR
Character between a prefix and another prefix or the actual literal.
Definition: convert_int_literal.cpp:33
convert_dint_literal.h
Statement List Language Conversion.
convert_int_bit_literal
constant_exprt convert_int_bit_literal(const std::string &src)
Converts a string into the corresponding 'Int' or 'DInt' expression.
Definition: convert_int_literal.cpp:116
bitvector_types.h
Pre-defined bitvector types.
BASE_10
#define BASE_10
Base of decimal integer literals.
Definition: convert_int_literal.cpp:27
get_int_type
signedbv_typet get_int_type()
Creates a new type that resembles the 'Int' type of the Siemens PLC languages.
Definition: statement_list_types.cpp:17
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:76
convert_int_hex_literal_value
constant_exprt convert_int_hex_literal_value(const std::string &src)
Converts a string into the corresponding 'Int' expression.
Definition: convert_int_literal.cpp:99
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:100
convert_int_dec_literal
constant_exprt convert_int_dec_literal(const std::string &src)
Converts a string into the corresponding 'Int' or 'DInt' expression.
Definition: convert_int_literal.cpp:48
convert_int_bit_literal_value
constant_exprt convert_int_bit_literal_value(const std::string &src)
Converts a string into the corresponding 'Int' expression.
Definition: convert_int_literal.cpp:133
convert_int_hex_literal
constant_exprt convert_int_hex_literal(const std::string &src)
Converts a string into the corresponding 'Int' or 'DInt' expression.
Definition: convert_int_literal.cpp:82
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
constant_exprt
A constant literal expression.
Definition: std_expr.h:2667
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:89
statement_list_types.h
Statement List Type Helper.