CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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 <optional>
15#include <string>
16
17class exprt;
18class namespacet;
19class typet;
20
21// try a type cast from expr.type() to type
22//
23// false: typecast successful, expr modified
24// true: typecast failed
25
27 const typet &src_type,
28 const typet &dest_type);
29
31 const typet &src_type,
32 const typet &dest_type,
33 const namespacet &ns);
34
36 exprt &expr,
37 const typet &dest_type,
38 const namespacet &ns);
39
42 const namespacet &ns);
43
45{
46public:
47 explicit c_typecastt(const namespacet &_ns):ns(_ns)
48 {
49 }
50
51 virtual ~c_typecastt()
52 {
53 }
54
55 virtual void implicit_typecast(
56 exprt &expr,
57 const typet &type);
58
60 exprt &expr);
61
63 exprt &expr1,
64 exprt &expr2);
65
66 std::list<std::string> errors;
67 std::list<std::string> warnings;
68
71 static std::optional<std::string> check_address_can_be_taken(const typet &);
72
73protected:
74 const namespacet &ns;
75
76 // these are in promotion order
77
78 enum c_typet { BOOL,
85 INTEGER, // these are unbounded integers, non-standard
86 FIXEDBV, // fixed-point, non-standard
88 RATIONAL, REAL, // infinite precision, non-standard
91
92 c_typet get_c_type(const typet &type) const;
93
95 exprt &expr,
97
99
100 // after follow_with_qualifiers
101 virtual void implicit_typecast_followed(
102 exprt &expr,
103 const typet &src_type,
104 const typet &orig_dest_type,
105 const typet &dest_type);
106
107 void do_typecast(exprt &dest, const typet &type);
108
109 c_typet minimum_promotion(const typet &type) const;
110};
111
112#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:562
@ LARGE_UNSIGNED_INT
Definition c_typecast.h:84
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:47
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:67
const namespacet & ns
Definition c_typecast.h:74
static std::optional< std::string > check_address_can_be_taken(const typet &)
virtual ~c_typecastt()
Definition c_typecast.h:51
c_typet minimum_promotion(const typet &type) const
std::list< std::string > errors
Definition c_typecast.h:66
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