CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
statement_list_types.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Statement List Type Helper
4
5Author: Matthias Weiss, matthias.weiss@diffblue.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_STATEMENT_LIST_CONVERTERS_STATEMENT_LIST_TYPES_H
13#define CPROVER_STATEMENT_LIST_CONVERTERS_STATEMENT_LIST_TYPES_H
14
15#define STL_INT_WIDTH 16u
16#define STL_DINT_WIDTH 32u
17
34
35#endif // CPROVER_STATEMENT_LIST_CONVERTERS_STATEMENT_LIST_TYPES_H
The Boolean type.
Definition std_types.h:36
Fixed-width bit-vector with IEEE floating-point interpretation.
Fixed-width bit-vector with two's complement interpretation.
class signedbv_typet get_int_type()
Creates a new type that resembles the 'Int' type of the Siemens PLC languages.
class signedbv_typet get_dint_type()
Creates a new type that resembles the 'DInt' type of the Siemens PLC languages.
class floatbv_typet get_real_type()
Creates a new type that resembles the 'Real' type of the Siemens PLC languages.
class bool_typet get_bool_type()
Creates a new type that resembles the 'Bool' type of the Siemens PLC languages.