cprover
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 <util/namespace.h>
14 #include <util/expr.h>
15 
16 #include <list>
17 
18 // try a type cast from expr.type() to type
19 //
20 // false: typecast successful, expr modified
21 // true: typecast failed
22 
24  const typet &src_type,
25  const typet &dest_type);
26 
28  const typet &src_type,
29  const typet &dest_type,
30  const namespacet &ns);
31 
33  exprt &expr,
34  const typet &dest_type,
35  const namespacet &ns);
36 
38  exprt &expr1, exprt &expr2,
39  const namespacet &ns);
40 
42 {
43 public:
44  explicit c_typecastt(const namespacet &_ns):ns(_ns)
45  {
46  }
47 
48  virtual ~c_typecastt()
49  {
50  }
51 
52  virtual void implicit_typecast(
53  exprt &expr,
54  const typet &type);
55 
56  virtual void implicit_typecast_arithmetic(
57  exprt &expr);
58 
59  virtual void implicit_typecast_arithmetic(
60  exprt &expr1,
61  exprt &expr2);
62 
63  std::list<std::string> errors;
64  std::list<std::string> warnings;
65 
66 protected:
67  const namespacet &ns;
68 
69  // these are in promotion order
70 
71  enum c_typet { BOOL,
78  INTEGER, // these are unbounded integers, non-standard
79  FIXEDBV, // fixed-point, non-standard
81  RATIONAL, REAL, // infinite precision, non-standard
84 
85  c_typet get_c_type(const typet &type) const;
86 
88  exprt &expr,
89  c_typet c_type);
90 
92 
93  // after follow_with_qualifiers
94  virtual void implicit_typecast_followed(
95  exprt &expr,
96  const typet &src_type,
97  const typet &orig_dest_type,
98  const typet &dest_type);
99 
100  void do_typecast(exprt &dest, const typet &type);
101 
102  c_typet minimum_promotion(const typet &type) const;
103 };
104 
105 #endif // CPROVER_ANSI_C_C_TYPECAST_H
c_typecastt::ns
const namespacet & ns
Definition: c_typecast.h:67
c_typecastt::LONGLONG
@ LONGLONG
Definition: c_typecast.h:76
c_typecastt
Definition: c_typecast.h:42
typet
The type of an expression, extends irept.
Definition: type.h:29
check_c_implicit_typecast
bool check_c_implicit_typecast(const typet &src_type, const typet &dest_type)
Definition: c_typecast.cpp:71
c_typecastt::COMPLEX
@ COMPLEX
Definition: c_typecast.h:82
c_typecastt::SINGLE
@ SINGLE
Definition: c_typecast.h:80
c_typecastt::INT
@ INT
Definition: c_typecast.h:74
c_typecastt::BOOL
@ BOOL
Definition: c_typecast.h:71
exprt
Base class for all expressions.
Definition: expr.h:53
c_typecastt::minimum_promotion
c_typet minimum_promotion(const typet &type) const
Definition: c_typecast.cpp:438
namespace.h
c_typecastt::UCHAR
@ UCHAR
Definition: c_typecast.h:72
expr.h
c_typecastt::LONG
@ LONG
Definition: c_typecast.h:75
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
c_typecastt::get_c_type
c_typet get_c_type(const typet &type) const
Definition: c_typecast.cpp:282
c_typecastt::warnings
std::list< std::string > warnings
Definition: c_typecast.h:64
c_typecastt::INTEGER
@ INTEGER
Definition: c_typecast.h:78
c_typecastt::LARGE_SIGNED_INT
@ LARGE_SIGNED_INT
Definition: c_typecast.h:77
c_typecastt::REAL
@ REAL
Definition: c_typecast.h:81
c_typecastt::USHORT
@ USHORT
Definition: c_typecast.h:73
c_typecastt::PTR
@ PTR
Definition: c_typecast.h:83
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:490
c_typecastt::UINT
@ UINT
Definition: c_typecast.h:74
c_typecastt::LONGDOUBLE
@ LONGDOUBLE
Definition: c_typecast.h:80
c_typecastt::VOIDPTR
@ VOIDPTR
Definition: c_typecast.h:83
c_typecastt::FLOAT128
@ FLOAT128
Definition: c_typecast.h:80
c_typecastt::implicit_typecast_arithmetic
virtual void implicit_typecast_arithmetic(exprt &expr)
Definition: c_typecast.cpp:470
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:49
c_typecastt::errors
std::list< std::string > errors
Definition: c_typecast.h:63
c_typecastt::ULONGLONG
@ ULONGLONG
Definition: c_typecast.h:76
c_typecastt::LARGE_UNSIGNED_INT
@ LARGE_UNSIGNED_INT
Definition: c_typecast.h:77
c_implicit_typecast
bool c_implicit_typecast(exprt &expr, const typet &dest_type, const namespacet &ns)
Definition: c_typecast.cpp:26
c_typecastt::~c_typecastt
virtual ~c_typecastt()
Definition: c_typecast.h:48
c_typecastt::c_typet
c_typet
Definition: c_typecast.h:71
c_typecastt::SHORT
@ SHORT
Definition: c_typecast.h:73
c_typecastt::CHAR
@ CHAR
Definition: c_typecast.h:72
c_typecastt::OTHER
@ OTHER
Definition: c_typecast.h:83
c_typecastt::ULONG
@ ULONG
Definition: c_typecast.h:75
c_typecastt::implicit_typecast
virtual void implicit_typecast(exprt &expr, const typet &type)
Definition: c_typecast.cpp:476
c_typecastt::follow_with_qualifiers
typet follow_with_qualifiers(const typet &src)
Definition: c_typecast.cpp:256
c_typecastt::do_typecast
void do_typecast(exprt &dest, const typet &type)
Definition: c_typecast.cpp:723
c_typecastt::DOUBLE
@ DOUBLE
Definition: c_typecast.h:80
c_typecastt::c_typecastt
c_typecastt(const namespacet &_ns)
Definition: c_typecast.h:44
c_typecastt::RATIONAL
@ RATIONAL
Definition: c_typecast.h:81
c_typecastt::FIXEDBV
@ FIXEDBV
Definition: c_typecast.h:79