cprover
flatten_byte_extract_exceptions.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Byte flattening
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_SOLVERS_FLATTENING_FLATTEN_BYTE_EXTRACT_EXCEPTIONS_H
10 #define CPROVER_SOLVERS_FLATTENING_FLATTEN_BYTE_EXTRACT_EXCEPTIONS_H
11 
12 #include <sstream>
13 #include <stdexcept>
14 #include <string>
15 
16 #include <util/std_expr.h>
17 #include <util/std_types.h>
18 
19 class flatten_byte_extract_exceptiont : public std::runtime_error
20 {
21 public:
22  explicit flatten_byte_extract_exceptiont(const std::string &exception_message)
23  : runtime_error(exception_message)
24  {
25  }
26 };
27 
29 {
30 public:
32  : flatten_byte_extract_exceptiont("cannot unpack array of non-const size"),
35  {
36  std::ostringstream error_message;
37  error_message << runtime_error::what() << "\n";
38  error_message << "array_type: " << array_type.pretty();
39  error_message << "\nmax_bytes: " << max_bytes.pretty();
40  computed_error_message = error_message.str();
41  }
42 
43  const char *what() const optional_noexcept override
44  {
45  return computed_error_message.c_str();
46  }
47 
48 private:
51 
53 };
54 
56 {
57 public:
61  const mp_integer &byte_width)
63  "cannot unpack struct with non-byte aligned components"),
67  {
68  std::ostringstream error_message;
69  error_message << runtime_error::what() << "\n";
70  error_message << "width: " << byte_width << "\n";
71  error_message << "component:" << component.get_name() << "\n";
72  error_message << "struct_type: " << struct_type.pretty();
73  computed_error_message = error_message.str();
74  }
75 
76  const char *what() const optional_noexcept override
77  {
78  return computed_error_message.c_str();
79  }
80 
81 private:
85 
87 };
88 
90 {
91 public:
92 public:
95  "cannot unpack object of non-constant width"),
96  src(src),
98  {
99  std::ostringstream error_message;
100  error_message << runtime_error::what() << "\n";
101  error_message << "array_type: " << src.pretty();
102  error_message << "\nmax_bytes: " << max_bytes.pretty();
103  computed_error_message = error_message.str();
104  }
105 
106  const char *what() const optional_noexcept override
107  {
108  return computed_error_message.c_str();
109  }
110 
111 private:
114 
116 };
117 
119 {
120 public:
124  "byte_extract flatting with non-constant size"),
126  {
127  std::ostringstream error_message;
128  error_message << runtime_error::what() << "\n";
129  error_message << "unpack_expr: " << unpack_expr.pretty();
130  computed_error_message = error_message.str();
131  }
132 
133  const char *what() const optional_noexcept override
134  {
135  return computed_error_message.c_str();
136  }
137 
138 private:
140 
142 };
143 
144 #endif // CPROVER_SOLVERS_FLATTENING_FLATTEN_BYTE_EXTRACT_EXCEPTIONS_H
non_byte_alignedt::non_byte_alignedt
non_byte_alignedt(const struct_typet &struct_type, const struct_union_typet::componentt &component, const mp_integer &byte_width)
Definition: flatten_byte_extract_exceptions.h:58
non_byte_alignedt::struct_type
const struct_typet struct_type
Definition: flatten_byte_extract_exceptions.h:82
flatten_byte_extract_exceptiont
Definition: flatten_byte_extract_exceptions.h:19
non_constant_widtht::max_bytes
exprt max_bytes
Definition: flatten_byte_extract_exceptions.h:113
non_constant_widtht::what
const char * what() const optional_noexcept override
Definition: flatten_byte_extract_exceptions.h:106
non_constant_widtht
Definition: flatten_byte_extract_exceptions.h:89
non_const_byte_extraction_sizet
Definition: flatten_byte_extract_exceptions.h:118
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
non_constant_widtht::src
exprt src
Definition: flatten_byte_extract_exceptions.h:112
non_byte_alignedt::computed_error_message
std::string computed_error_message
Definition: flatten_byte_extract_exceptions.h:86
exprt
Base class for all expressions.
Definition: expr.h:54
non_const_array_sizet::computed_error_message
std::string computed_error_message
Definition: flatten_byte_extract_exceptions.h:52
non_byte_alignedt::byte_width
const mp_integer byte_width
Definition: flatten_byte_extract_exceptions.h:84
non_const_array_sizet::what
const char * what() const optional_noexcept override
Definition: flatten_byte_extract_exceptions.h:43
flatten_byte_extract_exceptiont::flatten_byte_extract_exceptiont
flatten_byte_extract_exceptiont(const std::string &exception_message)
Definition: flatten_byte_extract_exceptions.h:22
non_constant_widtht::computed_error_message
std::string computed_error_message
Definition: flatten_byte_extract_exceptions.h:115
non_const_array_sizet::array_type
array_typet array_type
Definition: flatten_byte_extract_exceptions.h:50
non_const_array_sizet::non_const_array_sizet
non_const_array_sizet(const array_typet &array_type, const exprt &max_bytes)
Definition: flatten_byte_extract_exceptions.h:31
non_constant_widtht::non_constant_widtht
non_constant_widtht(const exprt &src, const exprt &max_bytes)
Definition: flatten_byte_extract_exceptions.h:93
non_const_byte_extraction_sizet::what
const char * what() const optional_noexcept override
Definition: flatten_byte_extract_exceptions.h:133
struct_union_typet::componentt::get_name
const irep_idt & get_name() const
Definition: std_types.h:132
non_const_byte_extraction_sizet::unpack_expr
const byte_extract_exprt unpack_expr
Definition: flatten_byte_extract_exceptions.h:139
std_types.h
non_byte_alignedt::what
const char * what() const optional_noexcept override
Definition: flatten_byte_extract_exceptions.h:76
struct_union_typet::componentt
Definition: std_types.h:121
non_const_array_sizet
Definition: flatten_byte_extract_exceptions.h:28
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:276
array_typet
Arrays with given size.
Definition: std_types.h:1000
non_byte_alignedt
Definition: flatten_byte_extract_exceptions.h:55
byte_extract_exprt
TO_BE_DOCUMENTED.
Definition: byte_operators.h:25
non_const_byte_extraction_sizet::computed_error_message
std::string computed_error_message
Definition: flatten_byte_extract_exceptions.h:141
non_const_byte_extraction_sizet::non_const_byte_extraction_sizet
non_const_byte_extraction_sizet(const byte_extract_exprt &unpack_expr)
Definition: flatten_byte_extract_exceptions.h:121
std_expr.h
non_const_array_sizet::max_bytes
exprt max_bytes
Definition: flatten_byte_extract_exceptions.h:49
non_byte_alignedt::component
const struct_union_typet::componentt component
Definition: flatten_byte_extract_exceptions.h:83