cprover
Loading...
Searching...
No Matches
c_typecast.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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/optional.h>
14
15#include <list>
16#include <string>
17
18class exprt;
19class namespacet;
20class typet;
21
22// try a type cast from expr.type() to type
23//
24// false: typecast successful, expr modified
25// true: typecast failed
26
28 const typet &src_type,
29 const typet &dest_type);
30
32 const typet &src_type,
33 const typet &dest_type,
34 const namespacet &ns);
35
37 exprt &expr,
38 const typet &dest_type,
39 const namespacet &ns);
40
43 const namespacet &ns);
44
46{
47public:
48 explicit c_typecastt(const namespacet &_ns):ns(_ns)
49 {
50 }
51
52 virtual ~c_typecastt()
53 {
54 }
55
56 virtual void implicit_typecast(
57 exprt &expr,
58 const typet &type);
59
61 exprt &expr);
62
64 exprt &expr1,
65 exprt &expr2);
66
67 std::list<std::string> errors;
68 std::list<std::string> warnings;
69
73
74protected:
75 const namespacet &ns;
76
77 // these are in promotion order
78
79 enum c_typet { BOOL,
86 INTEGER, // these are unbounded integers, non-standard
87 FIXEDBV, // fixed-point, non-standard
89 RATIONAL, REAL, // infinite precision, non-standard
92
93 c_typet get_c_type(const typet &type) const;
94
96 exprt &expr,
98
100
101 // after follow_with_qualifiers
102 virtual void implicit_typecast_followed(
103 exprt &expr,
104 const typet &src_type,
105 const typet &orig_dest_type,
106 const typet &dest_type);
107
108 void do_typecast(exprt &dest, const typet &type);
109
110 c_typet minimum_promotion(const typet &type) const;
111};
112
113#endif // CPROVER_ANSI_C_C_TYPECAST_H
bool c_implicit_typecast(exprt &expr, const typet &dest_type, const namespacet &ns)
bool c_implicit_typecast_arithmetic(exprt &expr1, exprt &expr2, const namespacet &ns)
perform arithmetic prompotions and conversions
bool check_c_implicit_typecast(const typet &src_type, const typet &dest_type)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
@ LARGE_UNSIGNED_INT
Definition c_typecast.h:85
virtual void implicit_typecast_followed(exprt &expr, const typet &src_type, const typet &orig_dest_type, const typet &dest_type)
c_typecastt(const namespacet &_ns)
Definition c_typecast.h:48
typet follow_with_qualifiers(const typet &src)
void do_typecast(exprt &dest, const typet &type)
static optionalt< std::string > check_address_can_be_taken(const typet &)
virtual void implicit_typecast(exprt &expr, const typet &type)
c_typet get_c_type(const typet &type) const
virtual void implicit_typecast_arithmetic(exprt &expr)
std::list< std::string > warnings
Definition c_typecast.h:68
const namespacet & ns
Definition c_typecast.h:75
virtual ~c_typecastt()
Definition c_typecast.h:52
c_typet minimum_promotion(const typet &type) const
std::list< std::string > errors
Definition c_typecast.h:67
Base class for all expressions.
Definition expr.h:56
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The type of an expression, extends irept.
Definition type.h:29