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 <list>
16 
17 #include <util/message.h>
18 
19 #include "c_qualifiers.h"
20 #include "c_storage_spec.h"
21 
23 {
24 public:
29 
30  // extensions
40 
42 
43  bool packed, aligned;
45  exprt msc_based; // this is Visual Studio
47 
48  // storage spec
50 
51  // qualifiers
53 
54  virtual void read(const typet &type);
55  virtual void write(typet &type);
56 
58 
59  std::list<typet> other;
60 
61  explicit ansi_c_convert_typet(message_handlert &_message_handler):
62  messaget(_message_handler)
63  // class members are initialized by calling read()
64  {
65  }
66 
67  virtual void clear()
68  {
84 
86 
87  other.clear();
90  }
91 
92 protected:
93  virtual void read_rec(const typet &type);
94  virtual void build_type_with_subtype(typet &type) const;
95  virtual void set_attributes(typet &type) const;
96 };
97 
98 #endif // CPROVER_ANSI_C_ANSI_C_CONVERT_TYPE_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
ansi_c_convert_typet::int8_cnt
unsigned int8_cnt
Definition: ansi_c_convert_type.h:31
ansi_c_convert_typet::gcc_attribute_mode
typet gcc_attribute_mode
Definition: ansi_c_convert_type.h:41
ansi_c_convert_typet::clear
virtual void clear()
Definition: ansi_c_convert_type.h:67
ansi_c_convert_typet::set_attributes
virtual void set_attributes(typet &type) const
Add qualifiers and GCC attributes onto type.
Definition: ansi_c_convert_type.cpp:615
ansi_c_convert_typet::msc_based
exprt msc_based
Definition: ansi_c_convert_type.h:45
irept::make_nil
void make_nil()
Definition: irep.h:475
typet
The type of an expression, extends irept.
Definition: type.h:29
c_storage_spec.h
ansi_c_convert_typet::gcc_float32x_cnt
unsigned gcc_float32x_cnt
Definition: ansi_c_convert_type.h:34
ansi_c_convert_typet::write
virtual void write(typet &type)
Definition: ansi_c_convert_type.cpp:254
ansi_c_convert_typet::source_location
source_locationt source_location
Definition: ansi_c_convert_type.h:57
ansi_c_convert_typet::vector_size
exprt vector_size
Definition: ansi_c_convert_type.h:44
ansi_c_convert_typet::c_qualifiers
c_qualifierst c_qualifiers
Definition: ansi_c_convert_type.h:52
ansi_c_convert_typet::int_cnt
unsigned int_cnt
Definition: ansi_c_convert_type.h:26
exprt
Base class for all expressions.
Definition: expr.h:53
ansi_c_convert_typet::signed_cnt
unsigned signed_cnt
Definition: ansi_c_convert_type.h:25
c_qualifiers.h
ansi_c_convert_typet::gcc_float64x_cnt
unsigned gcc_float64x_cnt
Definition: ansi_c_convert_type.h:35
c_qualifierst::clear
virtual void clear() override
Definition: c_qualifiers.h:79
ansi_c_convert_typet
Definition: ansi_c_convert_type.h:23
ansi_c_convert_typet::ptr64_cnt
unsigned ptr64_cnt
Definition: ansi_c_convert_type.h:32
ansi_c_convert_typet::double_cnt
unsigned double_cnt
Definition: ansi_c_convert_type.h:27
ansi_c_convert_typet::fixedbv_cnt
unsigned fixedbv_cnt
Definition: ansi_c_convert_type.h:39
ansi_c_convert_typet::int64_cnt
unsigned int64_cnt
Definition: ansi_c_convert_type.h:31
ansi_c_convert_typet::gcc_float64_cnt
unsigned gcc_float64_cnt
Definition: ansi_c_convert_type.h:35
ansi_c_convert_typet::c_bool_cnt
unsigned c_bool_cnt
Definition: ansi_c_convert_type.h:27
ansi_c_convert_typet::gcc_float32_cnt
unsigned gcc_float32_cnt
Definition: ansi_c_convert_type.h:34
ansi_c_convert_typet::gcc_int128_cnt
unsigned gcc_int128_cnt
Definition: ansi_c_convert_type.h:37
ansi_c_convert_typet::int32_cnt
unsigned int32_cnt
Definition: ansi_c_convert_type.h:31
ansi_c_convert_typet::bv_cnt
unsigned bv_cnt
Definition: ansi_c_convert_type.h:38
ansi_c_convert_typet::char_cnt
unsigned char_cnt
Definition: ansi_c_convert_type.h:25
ansi_c_convert_typet::complex_cnt
unsigned complex_cnt
Definition: ansi_c_convert_type.h:28
ansi_c_convert_typet::proper_bool_cnt
unsigned proper_bool_cnt
Definition: ansi_c_convert_type.h:28
ansi_c_convert_typet::gcc_float128_cnt
unsigned gcc_float128_cnt
Definition: ansi_c_convert_type.h:36
ansi_c_convert_typet::short_cnt
unsigned short_cnt
Definition: ansi_c_convert_type.h:26
ansi_c_convert_typet::constructor
bool constructor
Definition: ansi_c_convert_type.h:46
ansi_c_convert_typet::gcc_float16_cnt
unsigned gcc_float16_cnt
Definition: ansi_c_convert_type.h:33
ansi_c_convert_typet::aligned
bool aligned
Definition: ansi_c_convert_type.h:43
c_qualifierst
Definition: c_qualifiers.h:61
message_handlert
Definition: message.h:28
ansi_c_convert_typet::other
std::list< typet > other
Definition: ansi_c_convert_type.h:59
c_storage_spect
Definition: c_storage_spec.h:16
ansi_c_convert_typet::bv_width
exprt bv_width
Definition: ansi_c_convert_type.h:44
ansi_c_convert_typet::c_storage_spec
c_storage_spect c_storage_spec
Definition: ansi_c_convert_type.h:49
ansi_c_convert_typet::long_cnt
unsigned long_cnt
Definition: ansi_c_convert_type.h:26
source_locationt
Definition: source_location.h:20
ansi_c_convert_typet::destructor
bool destructor
Definition: ansi_c_convert_type.h:46
ansi_c_convert_typet::floatbv_cnt
unsigned floatbv_cnt
Definition: ansi_c_convert_type.h:39
c_storage_spect::clear
void clear()
Definition: c_storage_spec.h:29
ansi_c_convert_typet::build_type_with_subtype
virtual void build_type_with_subtype(typet &type) const
Build a vector or complex type with type as subtype.
Definition: ansi_c_convert_type.cpp:595
ansi_c_convert_typet::unsigned_cnt
unsigned unsigned_cnt
Definition: ansi_c_convert_type.h:25
ansi_c_convert_typet::int16_cnt
unsigned int16_cnt
Definition: ansi_c_convert_type.h:31
ansi_c_convert_typet::alignment
exprt alignment
Definition: ansi_c_convert_type.h:44
ansi_c_convert_typet::packed
bool packed
Definition: ansi_c_convert_type.h:43
ansi_c_convert_typet::gcc_float128x_cnt
unsigned gcc_float128x_cnt
Definition: ansi_c_convert_type.h:36
ansi_c_convert_typet::read
virtual void read(const typet &type)
Definition: ansi_c_convert_type.cpp:26
ansi_c_convert_typet::ansi_c_convert_typet
ansi_c_convert_typet(message_handlert &_message_handler)
Definition: ansi_c_convert_type.h:61
ansi_c_convert_typet::ptr32_cnt
unsigned ptr32_cnt
Definition: ansi_c_convert_type.h:32
message.h
ansi_c_convert_typet::float_cnt
unsigned float_cnt
Definition: ansi_c_convert_type.h:27
ansi_c_convert_typet::fraction_width
exprt fraction_width
Definition: ansi_c_convert_type.h:44
ansi_c_convert_typet::read_rec
virtual void read_rec(const typet &type)
Definition: ansi_c_convert_type.cpp:33