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
22 #define STL_DINT_MIN_VALUE -2147483648LL
24 #define BASE_10 10u
26 #define BASE_16 16u
28 #define BASE_2 2u
30 #define PREFIX_SEPARATOR '#'
32 #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 }
arith_tools.h
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_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
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
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
convert_dint_literal.h
bitvector_types.h
BASE_2
#define BASE_2
Base of binary double integer literals.
Definition: convert_dint_literal.cpp:29
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
BASE_10
#define BASE_10
Base of decimal double integer literals.
Definition: convert_dint_literal.cpp:25
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:100
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:68
constant_exprt
A constant literal expression.
Definition: std_expr.h:2941
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_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