CBMC
convert_dint_literal.h File Reference

Statement List Language Conversion. More...

#include <util/std_expr.h>
+ Include dependency graph for convert_dint_literal.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

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.h.

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.