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:
31
32 // extensions
42
44
47 exprt msc_based; // this is Visual Studio
49
50 // contracts
52
53 // storage spec
55
56 // qualifiers
58
59 virtual void write(typet &type);
60
62
63 std::list<typet> other;
64
65 ansi_c_convert_typet(message_handlert &_message_handler, const typet &type)
66 : ansi_c_convert_typet(_message_handler)
67 {
69 read_rec(type);
70 }
71
72protected:
74
75 // Default-initialize all members. To be used by classes deriving from this
76 // one to make sure additional members can be initialized before invoking
77 // read_rec.
78 explicit ansi_c_convert_typet(message_handlert &_message_handler)
79 : unsigned_cnt(0),
80 signed_cnt(0),
81 char_cnt(0),
82 int_cnt(0),
83 short_cnt(0),
84 long_cnt(0),
85 double_cnt(0),
86 float_cnt(0),
87 c_bool_cnt(0),
89 complex_cnt(0),
90 int8_cnt(0),
91 int16_cnt(0),
92 int32_cnt(0),
93 int64_cnt(0),
94 ptr32_cnt(0),
95 ptr64_cnt(0),
104 bv_cnt(0),
105 floatbv_cnt(0),
106 fixedbv_cnt(0),
107 gcc_attribute_mode(static_cast<const typet &>(get_nil_irep())),
108 packed(false),
109 aligned(false),
115 constructor(false),
116 destructor(false),
117 message_handler(_message_handler)
118 {
119 }
120
121 virtual void read_rec(const typet &type);
122 virtual void build_type_with_subtype(typet &type) const;
123 virtual void set_attributes(typet &type) const;
124};
125
126#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:3073
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.