53{

56

58

62 {

63

67 if(rem<0)

68 rem=-rem;

69

70 if(rem*2>=p)

71 {

72 if(v<0)

73 --div;

74 else

75 ++div;

76 }

77

78 result=div;

79 }

80 else

81 {

82

83 result=v;

84 }

85

86 v=result;

88}

96{

97 v*=o.v;

98

100

103

105

106 return *this;

107}

110{

111 v += o.v;

112 return *this;

113}

116{

117 v -= o.v;

118 return *this;

119}

122{

124 v/=o.v;

125

126 return *this;

127}

136{

137 std::string dest;

139

142

144 {

145 dest+='-';

147 }

148

151

154

157

160

162

163

167

170

172 dest=" "+dest;

173

174 return dest;

175}

Pre-defined bitvector types.

const fixedbv_typet & to_fixedbv_type(const typet &type)

Cast a typet to a fixedbv_typet.

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

void set_width(std::size_t width)

std::size_t get_width() const

A constant literal expression.

const irep_idt & get_value() const

typet & type()

Return the type of the expression.

std::size_t get_fraction_bits() const

Fixed-width bit-vector with signed fixed-point interpretation.

void set_integer_bits(std::size_t b)

std::size_t get_integer_bits() const

void from_integer(const mp_integer &i)

void from_expr(const constant_exprt &expr)

bool operator==(int i) const

fixedbvt & operator+=(const fixedbvt &other)

mp_integer to_integer() const

fixedbvt & operator*=(const fixedbvt &other)

void round(const fixedbv_spect &dest_spec)

std::string format(const format_spect &format_spec) const

fixedbvt & operator/=(const fixedbvt &other)

fixedbvt & operator-=(const fixedbvt &other)

constant_exprt to_expr() const

const std::string integer2string(const mp_integer &n, unsigned base)

#define PRECONDITION(CONDITION)

API to expression classes.