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/expr.h>
18 #include <util/message.h>
19 
20 #include "c_qualifiers.h"
21 #include "c_storage_spec.h"
22 
24 {
25 public:
30 
31  // extensions
41 
43 
44  bool packed, aligned;
46  exprt msc_based; // this is Visual Studio
48 
49  // contracts
51 
52  // storage spec
54 
55  // qualifiers
57 
58  virtual void read(const typet &type);
59  virtual void write(typet &type);
60 
62 
63  std::list<typet> other;
64 
65  explicit ansi_c_convert_typet(message_handlert &_message_handler):
66  messaget(_message_handler)
67  // class members are initialized by calling read()
68  {
69  }
70 
71  virtual void clear()
72  {
88 
89  assigns.clear();
90  requires.clear();
91  ensures.clear();
92 
94 
95  other.clear();
98  }
99 
100 protected:
101  virtual void read_rec(const typet &type);
102  virtual void build_type_with_subtype(typet &type) const;
103  virtual void set_attributes(typet &type) const;
104 };
105 
106 #endif // CPROVER_ANSI_C_ANSI_C_CONVERT_TYPE_H
exprt::operandst ensures
virtual void read_rec(const typet &type)
ansi_c_convert_typet(message_handlert &_message_handler)
c_storage_spect c_storage_spec
virtual void read(const typet &type)
virtual void write(typet &type)
exprt::operandst requires
virtual void set_attributes(typet &type) const
Add qualifiers and GCC attributes onto type.
exprt::operandst assigns
source_locationt source_location
virtual void build_type_with_subtype(typet &type) const
Build a vector or complex type with type as subtype.
std::list< typet > other
virtual void clear() override
Definition: c_qualifiers.h:80
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
void make_nil()
Definition: irep.h:454
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
The type of an expression, extends irept.
Definition: type.h:29