CBMC
bv_arithmetic.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_UTIL_BV_ARITHMETIC_H
11 #define CPROVER_UTIL_BV_ARITHMETIC_H
12 
13 #include <iosfwd>
14 
15 #include "mp_arith.h"
16 #include "format_spec.h"
17 
18 class constant_exprt;
19 class typet;
20 
21 class bv_spect
22 {
23 public:
24  std::size_t width;
25  bool is_signed;
26 
27  explicit bv_spect(const typet &type)
28  {
29  from_type(type);
30  }
31 
32  void from_type(const typet &type);
33 
34  bv_spect():width(0), is_signed(false)
35  {
36  }
37 
38  mp_integer max_value() const;
39  mp_integer min_value() const;
40 
41  typet to_type() const;
42 
43  bool operator==(const bv_spect &other) const
44  {
45  return width==other.width && is_signed==other.is_signed;
46  }
47 };
48 
50 {
51 public:
53 
54  explicit bv_arithmetict(const bv_spect &_spec):
55  spec(_spec), value(0)
56  {
57  }
58 
60  {
61  }
62 
63  explicit bv_arithmetict(const constant_exprt &expr)
64  {
65  from_expr(expr);
66  }
67 
68  void negate();
69 
70  void make_zero()
71  {
72  value=0;
73  }
74 
75  bool is_zero() const { return value==0; }
76 
77  // performs conversion to bit-vector format
78  void from_integer(const mp_integer &i);
79 
80  // performs conversion from ieee floating point format
81  void change_spec(const bv_spect &dest_spec);
82  mp_integer to_integer() const { return value; }
83 
84  void print(std::ostream &out) const;
85 
86  std::string to_ansi_c_string() const
87  {
88  return format(format_spect());
89  }
90 
91  std::string format(const format_spect &format_spec) const;
92 
93  // expressions
94  constant_exprt to_expr() const;
95  void from_expr(const constant_exprt &expr);
96 
102 
103  bool operator<(const bv_arithmetict &other);
104  bool operator<=(const bv_arithmetict &other);
105  bool operator>(const bv_arithmetict &other);
106  bool operator>=(const bv_arithmetict &other);
107  bool operator==(const bv_arithmetict &other);
108  bool operator!=(const bv_arithmetict &other);
109  bool operator==(int i);
110 
111  std::ostream &operator<<(std::ostream &out)
112  {
113  return out << to_ansi_c_string();
114  }
115 
116  // turn into natural number representation
117  void unpack(const mp_integer &i) { value=i; adjust(); }
118  mp_integer pack() const;
119 
120 protected:
121  // we store negative numbers as such
123 
124  // puts the value back into its range
125  void adjust();
126 };
127 
128 #endif // CPROVER_UTIL_BV_ARITHMETIC_H
bv_arithmetict(const bv_spect &_spec)
Definition: bv_arithmetic.h:54
mp_integer to_integer() const
Definition: bv_arithmetic.h:82
bool operator==(const bv_arithmetict &other)
bool operator>=(const bv_arithmetict &other)
mp_integer value
bool operator<(const bv_arithmetict &other)
void change_spec(const bv_spect &dest_spec)
void unpack(const mp_integer &i)
constant_exprt to_expr() const
void from_integer(const mp_integer &i)
bv_arithmetict & operator*=(const bv_arithmetict &other)
bool operator<=(const bv_arithmetict &other)
void print(std::ostream &out) const
std::string format(const format_spect &format_spec) const
bool is_zero() const
Definition: bv_arithmetic.h:75
bv_arithmetict & operator+=(const bv_arithmetict &other)
bool operator!=(const bv_arithmetict &other)
void from_expr(const constant_exprt &expr)
bv_arithmetict(const constant_exprt &expr)
Definition: bv_arithmetic.h:63
bv_arithmetict & operator%=(const bv_arithmetict &other)
bv_arithmetict & operator-=(const bv_arithmetict &other)
std::ostream & operator<<(std::ostream &out)
std::string to_ansi_c_string() const
Definition: bv_arithmetic.h:86
bv_arithmetict & operator/=(const bv_arithmetict &other)
bool operator>(const bv_arithmetict &other)
mp_integer pack() const
std::size_t width
Definition: bv_arithmetic.h:24
bv_spect(const typet &type)
Definition: bv_arithmetic.h:27
bool operator==(const bv_spect &other) const
Definition: bv_arithmetic.h:43
bool is_signed
Definition: bv_arithmetic.h:25
void from_type(const typet &type)
mp_integer min_value() const
typet to_type() const
mp_integer max_value() const
A constant literal expression.
Definition: std_expr.h:2987
The type of an expression, extends irept.
Definition: type.h:29
BigInt mp_integer
Definition: smt_terms.h:17