CBMC
convert_dint_literal.cpp File Reference

Statement List Language Conversion. More...

#include "convert_dint_literal.h"
#include "statement_list_types.h"
#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <stdexcept>
+ Include dependency graph for convert_dint_literal.cpp:

Go to the source code of this file.

Macros

#define STL_DINT_MAX_VALUE   2147483647LL
 Minimum value of double integer literals. More...
 
#define STL_DINT_MIN_VALUE   -2147483648LL
 Minimum value of double integer literals. More...
 
#define BASE_10   10u
 Base of decimal double integer literals. More...
 
#define BASE_16   16u
 Base of hexadecimal double integer literals. More...
 
#define BASE_2   2u
 Base of binary double integer literals. More...
 
#define PREFIX_SEPARATOR   '#'
 Character between a prefix and another prefix or the actual literal. More...
 
#define OUT_OF_RANGE_MSG   "DInt literal out of range"
 Message for the case of a literal being out of range. More...
 

Functions

static constant_exprt convert_dint_literal_value (const long long literal_value)
 Converts the value of a literal the corresponding 'DInt' expression. More...
 
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. More...
 
constant_exprt convert_dint_dec_literal_value (const std::string &src)
 Converts a string into the corresponding 'DInt' expression. More...
 
constant_exprt convert_dint_hex_literal_value (const std::string &src)
 Converts a string into the corresponding 'DInt' expression. More...
 
constant_exprt convert_dint_bit_literal_value (const std::string &src)
 Converts a string into the corresponding 'DInt' expression. More...
 

Detailed Description

Statement List Language Conversion.

Definition in file convert_dint_literal.cpp.

Macro Definition Documentation

◆ BASE_10

#define BASE_10   10u

Base of decimal double integer literals.

Definition at line 25 of file convert_dint_literal.cpp.

◆ BASE_16

#define BASE_16   16u

Base of hexadecimal double integer literals.

Definition at line 27 of file convert_dint_literal.cpp.

◆ BASE_2

#define BASE_2   2u

Base of binary double integer literals.

Definition at line 29 of file convert_dint_literal.cpp.

◆ OUT_OF_RANGE_MSG

#define OUT_OF_RANGE_MSG   "DInt literal out of range"

Message for the case of a literal being out of range.

Definition at line 33 of file convert_dint_literal.cpp.

◆ PREFIX_SEPARATOR

#define PREFIX_SEPARATOR   '#'

Character between a prefix and another prefix or the actual literal.

Definition at line 31 of file convert_dint_literal.cpp.

◆ STL_DINT_MAX_VALUE

#define STL_DINT_MAX_VALUE   2147483647LL

Minimum value of double integer literals.

Definition at line 21 of file convert_dint_literal.cpp.

◆ STL_DINT_MIN_VALUE

#define STL_DINT_MIN_VALUE   -2147483648LL

Minimum value of double integer literals.

Definition at line 23 of file convert_dint_literal.cpp.

Function Documentation

◆ convert_dint_bit_literal_value()

constant_exprt convert_dint_bit_literal_value ( const std::string &  src)

Converts a string into the corresponding 'DInt' expression.

Parameters
srcString returned by the parser (base 2).
Returns
Constant expression representing the double integer value.

Definition at line 88 of file convert_dint_literal.cpp.

◆ convert_dint_dec_literal_value()

constant_exprt convert_dint_dec_literal_value ( const std::string &  src)

Converts a string into the corresponding 'DInt' expression.

Parameters
srcString returned by the parser (base 10).
Returns
Constant expression representing the double integer value.

Definition at line 62 of file convert_dint_literal.cpp.

◆ convert_dint_hex_literal_value()

constant_exprt convert_dint_hex_literal_value ( const std::string &  src)

Converts a string into the corresponding 'DInt' expression.

Parameters
srcString returned by the parser (base 16).
Returns
Constant expression representing the double integer value.

Definition at line 75 of file convert_dint_literal.cpp.

◆ convert_dint_literal_value()

static constant_exprt convert_dint_literal_value ( const long long  literal_value)
static

Converts the value of a literal the corresponding 'DInt' expression.

Parameters
literal_valueNumeric representation of the literal.
Returns
Constant expression representing the double integer value.

Definition at line 38 of file convert_dint_literal.cpp.

◆ get_literal_value()

static long long get_literal_value ( const std::string &  src,
unsigned int  base 
)
static

Removes every prefix from the given string and converts the remaining string to a number.

Parameters
srcString to extract the number from.
baseBase of the given literal.
Returns
Value of the literal.

Definition at line 51 of file convert_dint_literal.cpp.