CBMC
c_typecast.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_ANSI_C_C_TYPECAST_H
11 #define CPROVER_ANSI_C_C_TYPECAST_H
12 
13 #include <list>
14 #include <string>
15 
16 class exprt;
17 class namespacet;
18 class typet;
19 
20 // try a type cast from expr.type() to type
21 //
22 // false: typecast successful, expr modified
23 // true: typecast failed
24 
26  const typet &src_type,
27  const typet &dest_type);
28 
30  const typet &src_type,
31  const typet &dest_type,
32  const namespacet &ns);
33 
35  exprt &expr,
36  const typet &dest_type,
37  const namespacet &ns);
38 
40  exprt &expr1, exprt &expr2,
41  const namespacet &ns);
42 
44 {
45 public:
46  explicit c_typecastt(const namespacet &_ns):ns(_ns)
47  {
48  }
49 
50  virtual ~c_typecastt()
51  {
52  }
53 
54  virtual void implicit_typecast(
55  exprt &expr,
56  const typet &type);
57 
58  virtual void implicit_typecast_arithmetic(
59  exprt &expr);
60 
61  virtual void implicit_typecast_arithmetic(
62  exprt &expr1,
63  exprt &expr2);
64 
65  std::list<std::string> errors;
66  std::list<std::string> warnings;
67 
68 protected:
69  const namespacet &ns;
70 
71  // these are in promotion order
72 
73  enum c_typet { BOOL,
80  INTEGER, // these are unbounded integers, non-standard
81  FIXEDBV, // fixed-point, non-standard
83  RATIONAL, REAL, // infinite precision, non-standard
86 
87  c_typet get_c_type(const typet &type) const;
88 
90  exprt &expr,
91  c_typet c_type);
92 
94 
95  // after follow_with_qualifiers
96  virtual void implicit_typecast_followed(
97  exprt &expr,
98  const typet &src_type,
99  const typet &orig_dest_type,
100  const typet &dest_type);
101 
102  void do_typecast(exprt &dest, const typet &type);
103 
104  c_typet minimum_promotion(const typet &type) const;
105 };
106 
107 #endif // CPROVER_ANSI_C_C_TYPECAST_H
c_typecastt::ns
const namespacet & ns
Definition: c_typecast.h:69
c_typecastt::LONGLONG
@ LONGLONG
Definition: c_typecast.h:78
c_typecastt
Definition: c_typecast.h:43
typet
The type of an expression, extends irept.
Definition: type.h:28
check_c_implicit_typecast
bool check_c_implicit_typecast(const typet &src_type, const typet &dest_type)
Definition: c_typecast.cpp:72
c_typecastt::COMPLEX
@ COMPLEX
Definition: c_typecast.h:84
c_typecastt::SINGLE
@ SINGLE
Definition: c_typecast.h:82
c_typecastt::INT
@ INT
Definition: c_typecast.h:76
c_typecastt::BOOL
@ BOOL
Definition: c_typecast.h:73
exprt
Base class for all expressions.
Definition: expr.h:55
c_typecastt::minimum_promotion
c_typet minimum_promotion(const typet &type) const
Definition: c_typecast.cpp:462
c_typecastt::UCHAR
@ UCHAR
Definition: c_typecast.h:74
c_typecastt::LONG
@ LONG
Definition: c_typecast.h:77
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
c_typecastt::get_c_type
c_typet get_c_type(const typet &type) const
Definition: c_typecast.cpp:304
c_typecastt::warnings
std::list< std::string > warnings
Definition: c_typecast.h:66
c_typecastt::INTEGER
@ INTEGER
Definition: c_typecast.h:80
c_typecastt::LARGE_SIGNED_INT
@ LARGE_SIGNED_INT
Definition: c_typecast.h:79
c_typecastt::REAL
@ REAL
Definition: c_typecast.h:83
c_typecastt::USHORT
@ USHORT
Definition: c_typecast.h:75
c_typecastt::PTR
@ PTR
Definition: c_typecast.h:85
c_typecastt::implicit_typecast_followed
virtual void implicit_typecast_followed(exprt &expr, const typet &src_type, const typet &orig_dest_type, const typet &dest_type)
Definition: c_typecast.cpp:514
c_typecastt::UINT
@ UINT
Definition: c_typecast.h:76
c_typecastt::LONGDOUBLE
@ LONGDOUBLE
Definition: c_typecast.h:82
c_typecastt::VOIDPTR
@ VOIDPTR
Definition: c_typecast.h:85
c_typecastt::FLOAT128
@ FLOAT128
Definition: c_typecast.h:82
c_typecastt::implicit_typecast_arithmetic
virtual void implicit_typecast_arithmetic(exprt &expr)
Definition: c_typecast.cpp:494
c_implicit_typecast_arithmetic
bool c_implicit_typecast_arithmetic(exprt &expr1, exprt &expr2, const namespacet &ns)
perform arithmetic prompotions and conversions
Definition: c_typecast.cpp:48
c_typecastt::errors
std::list< std::string > errors
Definition: c_typecast.h:65
c_typecastt::ULONGLONG
@ ULONGLONG
Definition: c_typecast.h:78
c_typecastt::LARGE_UNSIGNED_INT
@ LARGE_UNSIGNED_INT
Definition: c_typecast.h:79
c_implicit_typecast
bool c_implicit_typecast(exprt &expr, const typet &dest_type, const namespacet &ns)
Definition: c_typecast.cpp:25
c_typecastt::~c_typecastt
virtual ~c_typecastt()
Definition: c_typecast.h:50
c_typecastt::c_typet
c_typet
Definition: c_typecast.h:73
c_typecastt::SHORT
@ SHORT
Definition: c_typecast.h:75
c_typecastt::CHAR
@ CHAR
Definition: c_typecast.h:74
c_typecastt::OTHER
@ OTHER
Definition: c_typecast.h:85
c_typecastt::ULONG
@ ULONG
Definition: c_typecast.h:77
c_typecastt::implicit_typecast
virtual void implicit_typecast(exprt &expr, const typet &type)
Definition: c_typecast.cpp:500
c_typecastt::follow_with_qualifiers
typet follow_with_qualifiers(const typet &src)
Definition: c_typecast.cpp:278
c_typecastt::do_typecast
void do_typecast(exprt &dest, const typet &type)
Definition: c_typecast.cpp:733
c_typecastt::DOUBLE
@ DOUBLE
Definition: c_typecast.h:82
c_typecastt::c_typecastt
c_typecastt(const namespacet &_ns)
Definition: c_typecast.h:46
c_typecastt::RATIONAL
@ RATIONAL
Definition: c_typecast.h:83
c_typecastt::FIXEDBV
@ FIXEDBV
Definition: c_typecast.h:81