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 <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{
25public:
30
31 // extensions
41
43
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
100protected:
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)
exprt::operandst c_storage_spect c_storage_spec
ansi_c_convert_typet(message_handlert &_message_handler)
virtual void read(const typet &type)
virtual void write(typet &type)
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