CBMC
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 
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 
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 
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 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Pre-defined bitvector types.
A constant literal expression.
Definition: std_expr.h:2995
#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.
#define size_type
Definition: unistd.c:347