CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
gcc_types.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "gcc_types.h"
10
11#include <util/ieee_float.h>
12
14{
15 floatbv_typet result=
18 return result;
19}
20
22{
23 // not same as float!
24 floatbv_typet result=
27 return result;
28}
29
31{
32 // not same as float!
33 floatbv_typet result=
36 return result;
37}
38
40{
41 // not same as double!
42 floatbv_typet result=
45 return result;
46}
47
49{
50 // not same as double!
51 floatbv_typet result=
54 return result;
55}
56
58{
59 // not same as long double!
60 floatbv_typet result=
63 return result;
64}
65
67{
68 // not same as long double!
69 floatbv_typet result=
72 return result;
73}
74
76{
77 unsignedbv_typet result(128);
79 return result;
80}
81
83{
84 signedbv_typet result(128);
86 return result;
87}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Fixed-width bit-vector with IEEE floating-point interpretation.
static ieee_float_spect half_precision()
Definition ieee_float.h:63
static ieee_float_spect single_precision()
Definition ieee_float.h:70
static ieee_float_spect quadruple_precision()
Definition ieee_float.h:82
static ieee_float_spect double_precision()
Definition ieee_float.h:76
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
Fixed-width bit-vector with two's complement interpretation.
Fixed-width bit-vector with unsigned binary interpretation.
floatbv_typet gcc_float32_type()
Definition gcc_types.cpp:21
floatbv_typet gcc_float16_type()
Definition gcc_types.cpp:13
floatbv_typet gcc_float64_type()
Definition gcc_types.cpp:39
signedbv_typet gcc_signed_int128_type()
Definition gcc_types.cpp:82
floatbv_typet gcc_float32x_type()
Definition gcc_types.cpp:30
floatbv_typet gcc_float64x_type()
Definition gcc_types.cpp:48
floatbv_typet gcc_float128x_type()
Definition gcc_types.cpp:66
unsignedbv_typet gcc_unsigned_int128_type()
Definition gcc_types.cpp:75
floatbv_typet gcc_float128_type()
Definition gcc_types.cpp:57