cprover
Loading...
Searching...
No Matches
ansi_c_convert_type.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: ANSI-C Language Conversion
4
5Author: 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/std_expr.h>
16
17#include "c_qualifiers.h"
18#include "c_storage_spec.h"
19
20#include <list>
21
23
25{
26public:
29
30 // extensions
40
42
45 exprt msc_based; // this is Visual Studio
47
48 // contracts
50
51 // storage spec
53
54 // qualifiers
56
57 virtual void write(typet &type);
58
60
61 std::list<typet> other;
62
63 ansi_c_convert_typet(message_handlert &_message_handler, const typet &type)
64 : ansi_c_convert_typet(_message_handler)
65 {
67 read_rec(type);
68 }
69
70protected:
72
73 // Default-initialize all members. To be used by classes deriving from this
74 // one to make sure additional members can be initialized before invoking
75 // read_rec.
76 explicit ansi_c_convert_typet(message_handlert &_message_handler)
77 : unsigned_cnt(0),
78 signed_cnt(0),
79 char_cnt(0),
80 int_cnt(0),
81 short_cnt(0),
82 long_cnt(0),
83 double_cnt(0),
84 float_cnt(0),
85 c_bool_cnt(0),
87 complex_cnt(0),
88 bitint_cnt(0),
89 int8_cnt(0),
90 int16_cnt(0),
91 int32_cnt(0),
92 int64_cnt(0),
93 ptr32_cnt(0),
94 ptr64_cnt(0),
103 bv_cnt(0),
104 floatbv_cnt(0),
105 fixedbv_cnt(0),
106 gcc_attribute_mode(static_cast<const typet &>(get_nil_irep())),
107 packed(false),
108 aligned(false),
114 constructor(false),
115 destructor(false),
116 message_handler(_message_handler)
117 {
118 }
119
120 virtual void read_rec(const typet &type);
121 virtual void build_type_with_subtype(typet &type) const;
122 virtual void set_attributes(typet &type) const;
123};
124
125#endif // CPROVER_ANSI_C_ANSI_C_CONVERT_TYPE_H
virtual void read_rec(const typet &type)
ansi_c_convert_typet(message_handlert &_message_handler)
c_storage_spect c_storage_spec
exprt::operandst c_ensures
virtual void write(typet &type)
message_handlert & message_handler
virtual void set_attributes(typet &type) const
Add qualifiers and GCC attributes onto type.
exprt::operandst c_requires
ansi_c_convert_typet(message_handlert &_message_handler, const typet &type)
source_locationt source_location
exprt::operandst c_assigns
virtual void build_type_with_subtype(typet &type) const
Build a vector or complex type with type as subtype.
std::list< typet > other
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
The NIL expression.
Definition std_expr.h:3086
The type of an expression, extends irept.
Definition type.h:29
const source_locationt & source_location() const
Definition type.h:72
const irept & get_nil_irep()
Definition irep.cpp:19
API to expression classes.