cprover
Loading...
Searching...
No Matches
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=
17 result.set(ID_C_c_type, ID_gcc_float16);
18 return result;
19}
20
22{
23 // not same as float!
24 floatbv_typet result=
26 result.set(ID_C_c_type, ID_gcc_float32);
27 return result;
28}
29
31{
32 // not same as float!
33 floatbv_typet result=
35 result.set(ID_C_c_type, ID_gcc_float32x);
36 return result;
37}
38
40{
41 // not same as double!
42 floatbv_typet result=
44 result.set(ID_C_c_type, ID_gcc_float64);
45 return result;
46}
47
49{
50 // not same as double!
51 floatbv_typet result=
53 result.set(ID_C_c_type, ID_gcc_float64x);
54 return result;
55}
56
58{
59 // not same as long double!
60 floatbv_typet result=
62 result.set(ID_C_c_type, ID_gcc_float128);
63 return result;
64}
65
67{
68 // not same as long double!
69 floatbv_typet result=
71 result.set(ID_C_c_type, ID_gcc_float128x);
72 return result;
73}
74
76{
77 unsignedbv_typet result(128);
78 result.set(ID_C_c_type, ID_unsigned_int128);
79 return result;
80}
81
83{
84 signedbv_typet result(128);
85 result.set(ID_C_c_type, ID_signed_int128);
86 return result;
87}
Fixed-width bit-vector with IEEE floating-point interpretation.
static ieee_float_spect half_precision()
Definition: ieee_float.h:64
static ieee_float_spect single_precision()
Definition: ieee_float.h:71
static ieee_float_spect quadruple_precision()
Definition: ieee_float.h:83
class floatbv_typet to_type() const
Definition: ieee_float.cpp:25
static ieee_float_spect double_precision()
Definition: ieee_float.h:77
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
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