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 <list>
14#include <string>
15
16class exprt;
17class namespacet;
18class 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
41 const namespacet &ns);
42
44{
45public:
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
59 exprt &expr);
60
62 exprt &expr1,
63 exprt &expr2);
64
65 std::list<std::string> errors;
66 std::list<std::string> warnings;
67
68protected:
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,
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
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:564
@ LARGE_UNSIGNED_INT
Definition c_typecast.h:79
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:46
typet follow_with_qualifiers(const typet &src)
void do_typecast(exprt &dest, const typet &type)
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:66
const namespacet & ns
Definition c_typecast.h:69
virtual ~c_typecastt()
Definition c_typecast.h:50
c_typet minimum_promotion(const typet &type) const
std::list< std::string > errors
Definition c_typecast.h:65
Base class for all expressions.
Definition expr.h:54
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