cprover
gcc_types.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "gcc_types.h"
10 
11 #include <util/config.h>
12 #include <util/c_types.h>
13 
15 {
16  floatbv_typet result=
18  result.set(ID_C_c_type, ID_gcc_float16);
19  return result;
20 }
21 
23 {
24  // not same as float!
25  floatbv_typet result=
27  result.set(ID_C_c_type, ID_gcc_float32);
28  return result;
29 }
30 
32 {
33  // not same as float!
34  floatbv_typet result=
36  result.set(ID_C_c_type, ID_gcc_float32x);
37  return result;
38 }
39 
41 {
42  // not same as double!
43  floatbv_typet result=
45  result.set(ID_C_c_type, ID_gcc_float64);
46  return result;
47 }
48 
50 {
51  // not same as double!
52  floatbv_typet result=
54  result.set(ID_C_c_type, ID_gcc_float64x);
55  return result;
56 }
57 
59 {
60  // not same as long double!
61  floatbv_typet result=
63  result.set(ID_C_c_type, ID_gcc_float128);
64  return result;
65 }
66 
68 {
69  // not same as long double!
70  floatbv_typet result=
72  result.set(ID_C_c_type, ID_gcc_float128x);
73  return result;
74 }
75 
77 {
78  unsignedbv_typet result(128);
79  result.set(ID_C_c_type, ID_unsigned_int128);
80  return result;
81 }
82 
84 {
85  signedbv_typet result(128);
86  result.set(ID_C_c_type, ID_signed_int128);
87  return result;
88 }
signedbv_typet gcc_signed_int128_type()
Definition: gcc_types.cpp:83
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1223
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1398
unsignedbv_typet gcc_unsigned_int128_type()
Definition: gcc_types.cpp:76
static ieee_float_spect double_precision()
Definition: ieee_float.h:80
class floatbv_typet to_type() const
Definition: ieee_float.cpp:26
floatbv_typet gcc_float128x_type()
Definition: gcc_types.cpp:67
static ieee_float_spect quadruple_precision()
Definition: ieee_float.h:86
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1278
floatbv_typet gcc_float32x_type()
Definition: gcc_types.cpp:31
static ieee_float_spect single_precision()
Definition: ieee_float.h:74
static ieee_float_spect half_precision()
Definition: ieee_float.h:67
floatbv_typet gcc_float16_type()
Definition: gcc_types.cpp:14
floatbv_typet gcc_float32_type()
Definition: gcc_types.cpp:22
floatbv_typet gcc_float64x_type()
Definition: gcc_types.cpp:49
floatbv_typet gcc_float128_type()
Definition: gcc_types.cpp:58
floatbv_typet gcc_float64_type()
Definition: gcc_types.cpp:40
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286