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 }
gcc_float32_type
floatbv_typet gcc_float32_type()
Definition: gcc_types.cpp:22
gcc_float64x_type
floatbv_typet gcc_float64x_type()
Definition: gcc_types.cpp:49
gcc_float16_type
floatbv_typet gcc_float16_type()
Definition: gcc_types.cpp:14
gcc_types.h
floatbv_typet
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1379
ieee_float_spect::quadruple_precision
static ieee_float_spect quadruple_precision()
Definition: ieee_float.h:86
ieee_float_spect::half_precision
static ieee_float_spect half_precision()
Definition: ieee_float.h:67
gcc_float128_type
floatbv_typet gcc_float128_type()
Definition: gcc_types.cpp:58
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1216
gcc_float64_type
floatbv_typet gcc_float64_type()
Definition: gcc_types.cpp:40
ieee_float_spect::double_precision
static ieee_float_spect double_precision()
Definition: ieee_float.h:80
gcc_signed_int128_type
signedbv_typet gcc_signed_int128_type()
Definition: gcc_types.cpp:83
ieee_float_spect::to_type
class floatbv_typet to_type() const
Definition: ieee_float.cpp:25
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1265
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
gcc_unsigned_int128_type
unsignedbv_typet gcc_unsigned_int128_type()
Definition: gcc_types.cpp:76
config.h
ieee_float_spect::single_precision
static ieee_float_spect single_precision()
Definition: ieee_float.h:74
c_types.h
gcc_float32x_type
floatbv_typet gcc_float32x_type()
Definition: gcc_types.cpp:31
gcc_float128x_type
floatbv_typet gcc_float128x_type()
Definition: gcc_types.cpp:67