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 // try a type cast from expr.type() to type
17 //
18 // false: typecast successful, expr modified
19 // true: typecast failed
20 
22  const typet &src_type,
23  const typet &dest_type);
24 
26  const typet &src_type,
27  const typet &dest_type,
28  const namespacet &ns);
29 
31  exprt &expr,
32  const typet &dest_type,
33  const namespacet &ns);
34 
36  exprt &expr1, exprt &expr2,
37  const namespacet &ns);
38 
40 {
41 public:
42  explicit c_typecastt(const namespacet &_ns):ns(_ns)
43  {
44  }
45 
46  virtual ~c_typecastt()
47  {
48  }
49 
50  virtual void implicit_typecast(
51  exprt &expr,
52  const typet &type);
53 
54  virtual void implicit_typecast_arithmetic(
55  exprt &expr);
56 
57  virtual void implicit_typecast_arithmetic(
58  exprt &expr1,
59  exprt &expr2);
60 
61  std::list<std::string> errors;
62  std::list<std::string> warnings;
63 
64 protected:
65  const namespacet &ns;
66 
67  // these are in promotion order
68 
69  enum c_typet { BOOL,
76  INTEGER, // these are unbounded integers, non-standard
77  FIXEDBV, // fixed-point, non-standard
79  RATIONAL, REAL, // infinite precision, non-standard
82 
83  c_typet get_c_type(const typet &type) const;
84 
86  exprt &expr,
87  c_typet c_type);
88 
90 
91  // after follow_with_qualifiers
92  virtual void implicit_typecast_followed(
93  exprt &expr,
94  const typet &src_type,
95  const typet &orig_dest_type,
96  const typet &dest_type);
97 
98  void do_typecast(exprt &dest, const typet &type);
99 
100  c_typet minimum_promotion(const typet &type) const;
101 };
102 
103 #endif // CPROVER_ANSI_C_C_TYPECAST_H
The type of an expression.
Definition: type.h:20
void do_typecast(exprt &dest, const typet &type)
Definition: c_typecast.cpp:696
bool c_implicit_typecast_arithmetic(exprt &expr1, exprt &expr2, const namespacet &ns)
perform arithmetic prompotions and conversions
Definition: c_typecast.cpp:49
virtual void implicit_typecast_followed(exprt &expr, const typet &src_type, const typet &orig_dest_type, const typet &dest_type)
Definition: c_typecast.cpp:461
c_typet get_c_type(const typet &type) const
Definition: c_typecast.cpp:277
virtual ~c_typecastt()
Definition: c_typecast.h:46
bool check_c_implicit_typecast(const typet &src_type, const typet &dest_type)
Definition: c_typecast.cpp:71
const namespacet & ns
Definition: c_typecast.h:65
std::list< std::string > warnings
Definition: c_typecast.h:62
TO_BE_DOCUMENTED.
Definition: namespace.h:62
std::list< std::string > errors
Definition: c_typecast.h:61
c_typecastt(const namespacet &_ns)
Definition: c_typecast.h:42
typet follow_with_qualifiers(const typet &src)
Definition: c_typecast.cpp:253
virtual void implicit_typecast_arithmetic(exprt &expr)
Definition: c_typecast.cpp:441
Base class for all expressions.
Definition: expr.h:46
virtual void implicit_typecast(exprt &expr, const typet &type)
Definition: c_typecast.cpp:447
bool c_implicit_typecast(exprt &expr, const typet &dest_type, const namespacet &ns)
Definition: c_typecast.cpp:26
c_typet minimum_promotion(const typet &type) const
Definition: c_typecast.cpp:408