cprover
ansi_c_convert_type.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: ANSI-C Language Conversion
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_ANSI_C_ANSI_C_CONVERT_TYPE_H
13
#define CPROVER_ANSI_C_ANSI_C_CONVERT_TYPE_H
14
15
#include <
util/message.h
>
16
17
#include "
c_qualifiers.h
"
18
#include "
c_storage_spec.h
"
19
20
class
ansi_c_convert_typet
:
public
messaget
21
{
22
public
:
23
unsigned
unsigned_cnt
,
signed_cnt
,
char_cnt
,
24
int_cnt
,
short_cnt
,
long_cnt
,
25
double_cnt
,
float_cnt
,
c_bool_cnt
,
26
proper_bool_cnt
,
complex_cnt
;
27
28
// extensions
29
unsigned
int8_cnt
,
int16_cnt
,
int32_cnt
,
int64_cnt
,
30
ptr32_cnt
,
ptr64_cnt
,
31
gcc_float16_cnt
,
32
gcc_float32_cnt
,
gcc_float32x_cnt
,
33
gcc_float64_cnt
,
gcc_float64x_cnt
,
34
gcc_float128_cnt
,
gcc_float128x_cnt
,
35
gcc_int128_cnt
,
36
bv_cnt
,
37
floatbv_cnt
,
fixedbv_cnt
;
38
39
typet
gcc_attribute_mode
;
40
41
bool
packed
,
aligned
;
42
exprt
vector_size
,
alignment
,
bv_width
,
fraction_width
;
43
exprt
msc_based
;
// this is Visual Studio
44
bool
constructor
,
destructor
;
45
46
// storage spec
47
c_storage_spect
c_storage_spec
;
48
49
// qualifiers
50
c_qualifierst
c_qualifiers
;
51
52
void
read
(
const
typet
&type);
53
void
write
(
typet
&type);
54
55
source_locationt
source_location
;
56
57
std::list<typet>
other
;
58
59
explicit
ansi_c_convert_typet
(
message_handlert
&_message_handler):
60
messaget
(_message_handler)
61
// class members are initialized by calling read()
62
{
63
}
64
65
void
clear
()
66
{
67
unsigned_cnt
=
signed_cnt
=
char_cnt
=
int_cnt
=
short_cnt
=
68
long_cnt
=
double_cnt
=
float_cnt
=
c_bool_cnt
=
proper_bool_cnt
=
complex_cnt
=
69
int8_cnt
=
int16_cnt
=
int32_cnt
=
int64_cnt
=
70
ptr32_cnt
=
ptr64_cnt
=
71
gcc_float16_cnt
=
72
gcc_float32_cnt
=
gcc_float32x_cnt
=
73
gcc_float64_cnt
=
gcc_float64x_cnt
=
74
gcc_float128_cnt
=
gcc_float128x_cnt
=
75
gcc_int128_cnt
=
bv_cnt
=
floatbv_cnt
=
fixedbv_cnt
=0;
76
vector_size
.
make_nil
();
77
alignment
.
make_nil
();
78
bv_width
.
make_nil
();
79
fraction_width
.
make_nil
();
80
msc_based
.
make_nil
();
81
gcc_attribute_mode
.
make_nil
();
82
83
packed
=
aligned
=
constructor
=
destructor
=
false
;
84
85
other
.clear();
86
c_storage_spec
.
clear
();
87
c_qualifiers
.
clear
();
88
}
89
90
protected
:
91
void
read_rec
(
const
typet
&type);
92
};
93
94
#endif // CPROVER_ANSI_C_ANSI_C_CONVERT_TYPE_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition:
message.h:144
ansi_c_convert_typet::int8_cnt
unsigned int8_cnt
Definition:
ansi_c_convert_type.h:29
ansi_c_convert_typet::gcc_attribute_mode
typet gcc_attribute_mode
Definition:
ansi_c_convert_type.h:39
ansi_c_convert_typet::msc_based
exprt msc_based
Definition:
ansi_c_convert_type.h:43
irept::make_nil
void make_nil()
Definition:
irep.h:315
typet
The type of an expression, extends irept.
Definition:
type.h:27
c_storage_spec.h
ansi_c_convert_typet::gcc_float32x_cnt
unsigned gcc_float32x_cnt
Definition:
ansi_c_convert_type.h:29
ansi_c_convert_typet::write
void write(typet &type)
Definition:
ansi_c_convert_type.cpp:255
ansi_c_convert_typet::source_location
source_locationt source_location
Definition:
ansi_c_convert_type.h:55
ansi_c_convert_typet::vector_size
exprt vector_size
Definition:
ansi_c_convert_type.h:42
ansi_c_convert_typet::c_qualifiers
c_qualifierst c_qualifiers
Definition:
ansi_c_convert_type.h:50
ansi_c_convert_typet::int_cnt
unsigned int_cnt
Definition:
ansi_c_convert_type.h:23
exprt
Base class for all expressions.
Definition:
expr.h:54
ansi_c_convert_typet::signed_cnt
unsigned signed_cnt
Definition:
ansi_c_convert_type.h:23
c_qualifiers.h
ansi_c_convert_typet::gcc_float64x_cnt
unsigned gcc_float64x_cnt
Definition:
ansi_c_convert_type.h:29
c_qualifierst::clear
virtual void clear() override
Definition:
c_qualifiers.h:79
ansi_c_convert_typet
Definition:
ansi_c_convert_type.h:20
ansi_c_convert_typet::ptr64_cnt
unsigned ptr64_cnt
Definition:
ansi_c_convert_type.h:29
ansi_c_convert_typet::double_cnt
unsigned double_cnt
Definition:
ansi_c_convert_type.h:23
ansi_c_convert_typet::fixedbv_cnt
unsigned fixedbv_cnt
Definition:
ansi_c_convert_type.h:29
ansi_c_convert_typet::int64_cnt
unsigned int64_cnt
Definition:
ansi_c_convert_type.h:29
ansi_c_convert_typet::gcc_float64_cnt
unsigned gcc_float64_cnt
Definition:
ansi_c_convert_type.h:29
ansi_c_convert_typet::c_bool_cnt
unsigned c_bool_cnt
Definition:
ansi_c_convert_type.h:23
ansi_c_convert_typet::gcc_float32_cnt
unsigned gcc_float32_cnt
Definition:
ansi_c_convert_type.h:29
ansi_c_convert_typet::gcc_int128_cnt
unsigned gcc_int128_cnt
Definition:
ansi_c_convert_type.h:29
ansi_c_convert_typet::int32_cnt
unsigned int32_cnt
Definition:
ansi_c_convert_type.h:29
ansi_c_convert_typet::bv_cnt
unsigned bv_cnt
Definition:
ansi_c_convert_type.h:29
ansi_c_convert_typet::char_cnt
unsigned char_cnt
Definition:
ansi_c_convert_type.h:23
ansi_c_convert_typet::complex_cnt
unsigned complex_cnt
Definition:
ansi_c_convert_type.h:23
ansi_c_convert_typet::proper_bool_cnt
unsigned proper_bool_cnt
Definition:
ansi_c_convert_type.h:23
ansi_c_convert_typet::gcc_float128_cnt
unsigned gcc_float128_cnt
Definition:
ansi_c_convert_type.h:29
ansi_c_convert_typet::short_cnt
unsigned short_cnt
Definition:
ansi_c_convert_type.h:23
ansi_c_convert_typet::constructor
bool constructor
Definition:
ansi_c_convert_type.h:44
ansi_c_convert_typet::gcc_float16_cnt
unsigned gcc_float16_cnt
Definition:
ansi_c_convert_type.h:29
ansi_c_convert_typet::aligned
bool aligned
Definition:
ansi_c_convert_type.h:41
c_qualifierst
Definition:
c_qualifiers.h:60
message_handlert
Definition:
message.h:24
ansi_c_convert_typet::other
std::list< typet > other
Definition:
ansi_c_convert_type.h:57
c_storage_spect
Definition:
c_storage_spec.h:15
ansi_c_convert_typet::bv_width
exprt bv_width
Definition:
ansi_c_convert_type.h:42
ansi_c_convert_typet::c_storage_spec
c_storage_spect c_storage_spec
Definition:
ansi_c_convert_type.h:47
ansi_c_convert_typet::long_cnt
unsigned long_cnt
Definition:
ansi_c_convert_type.h:23
source_locationt
Definition:
source_location.h:20
ansi_c_convert_typet::destructor
bool destructor
Definition:
ansi_c_convert_type.h:44
ansi_c_convert_typet::floatbv_cnt
unsigned floatbv_cnt
Definition:
ansi_c_convert_type.h:29
c_storage_spect::clear
void clear()
Definition:
c_storage_spec.h:29
ansi_c_convert_typet::unsigned_cnt
unsigned unsigned_cnt
Definition:
ansi_c_convert_type.h:23
ansi_c_convert_typet::int16_cnt
unsigned int16_cnt
Definition:
ansi_c_convert_type.h:29
ansi_c_convert_typet::clear
void clear()
Definition:
ansi_c_convert_type.h:65
ansi_c_convert_typet::alignment
exprt alignment
Definition:
ansi_c_convert_type.h:42
ansi_c_convert_typet::packed
bool packed
Definition:
ansi_c_convert_type.h:41
ansi_c_convert_typet::gcc_float128x_cnt
unsigned gcc_float128x_cnt
Definition:
ansi_c_convert_type.h:29
ansi_c_convert_typet::read
void read(const typet &type)
Definition:
ansi_c_convert_type.cpp:25
ansi_c_convert_typet::ansi_c_convert_typet
ansi_c_convert_typet(message_handlert &_message_handler)
Definition:
ansi_c_convert_type.h:59
ansi_c_convert_typet::ptr32_cnt
unsigned ptr32_cnt
Definition:
ansi_c_convert_type.h:29
message.h
ansi_c_convert_typet::float_cnt
unsigned float_cnt
Definition:
ansi_c_convert_type.h:23
ansi_c_convert_typet::fraction_width
exprt fraction_width
Definition:
ansi_c_convert_type.h:42
ansi_c_convert_typet::read_rec
void read_rec(const typet &type)
Definition:
ansi_c_convert_type.cpp:32
ansi-c
ansi_c_convert_type.h
Generated by
1.8.16