cprover
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 <algorithm>
19 #include <stdexcept>
20 
22 #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"
35 
39 static constant_exprt convert_dint_literal_value(const long long literal_value)
40 {
41  if(STL_DINT_MIN_VALUE <= literal_value && STL_DINT_MAX_VALUE >= literal_value)
42  return from_integer(literal_value, get_dint_type());
43  else
44  throw std::out_of_range{OUT_OF_RANGE_MSG};
45 }
46 
52 static long long get_literal_value(const std::string &src, unsigned int base)
53 {
54  std::string::size_type offset = src.find_last_of(PREFIX_SEPARATOR);
55  if(offset == std::string::npos)
56  offset = 0u;
57  else
58  ++offset;
59  const std::string literal{src.substr(offset)};
60  return std::stoll(literal, nullptr, base);
61 }
62 
64 {
65  try
66  {
67  const long long literal_value = get_literal_value(src, BASE_10);
68  return convert_dint_literal_value(literal_value);
69  }
70  catch(std::out_of_range &)
71  {
72  throw std::out_of_range{OUT_OF_RANGE_MSG};
73  }
74 }
75 
77 {
78  try
79  {
80  const long long literal_value = get_literal_value(src, BASE_16);
81  return convert_dint_literal_value(literal_value);
82  }
83  catch(std::out_of_range &)
84  {
85  throw std::out_of_range{OUT_OF_RANGE_MSG};
86  }
87 }
88 
90 {
91  try
92  {
93  const long long literal_value = get_literal_value(src, BASE_2);
94  return convert_dint_literal_value(literal_value);
95  }
96  catch(std::out_of_range &)
97  {
98  throw std::out_of_range{OUT_OF_RANGE_MSG};
99  }
100 }
arith_tools.h
PREFIX_SEPARATOR
#define PREFIX_SEPARATOR
Character between a prefix and another prefix or the actual literal.
Definition: convert_dint_literal.cpp:32
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:39
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:52
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
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:34
convert_dint_literal.h
Statement List Language Conversion.
bitvector_types.h
Pre-defined bitvector types.
BASE_2
#define BASE_2
Base of binary double integer literals.
Definition: convert_dint_literal.cpp:30
BASE_16
#define BASE_16
Base of hexadecimal double integer literals.
Definition: convert_dint_literal.cpp:28
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
BASE_10
#define BASE_10
Base of decimal double integer literals.
Definition: convert_dint_literal.cpp:26
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: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
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
Statement List Type Helper.