cprover
Loading...
Searching...
No Matches
bitvector_types.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Pre-defined bitvector types
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "bitvector_types.h"
13
14#include "arith_tools.h"
15#include "bv_arithmetic.h"
16#include "std_expr.h"
17#include "string2int.h"
18
20{
21 const irep_idt integer_bits = get(ID_integer_bits);
22 DATA_INVARIANT(!integer_bits.empty(), "integer bits should be set");
23 return unsafe_string2unsigned(id2string(integer_bits));
24}
25
26std::size_t floatbv_typet::get_f() const
27{
28 const irep_idt &f = get(ID_f);
29 DATA_INVARIANT(!f.empty(), "the mantissa should be set");
31}
32
37
42
47
52
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Pre-defined bitvector types.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
mp_integer min_value() const
mp_integer max_value() const
A constant literal expression.
Definition std_expr.h:2807
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
bool empty() const
Definition dstring.h:88
std::size_t get_integer_bits() const
std::size_t get_f() const
constant_exprt largest_expr() const
Return an expression representing the largest value of this type.
mp_integer largest() const
Return the largest value that can be represented using this type.
constant_exprt zero_expr() const
Return an expression representing the zero value of this type.
constant_exprt smallest_expr() const
Return an expression representing the smallest value of this type.
mp_integer smallest() const
Return the smallest value that can be represented using this type.
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:45
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
API to expression classes.
unsigned unsafe_string2unsigned(const std::string &str, int base)