cprover
std_types.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "std_types.h"
10 
11 #include "string2int.h"
12 #include "arith_tools.h"
13 #include "std_expr.h"
14 
16 {
17  const irep_idt integer_bits=get(ID_integer_bits);
18  assert(!integer_bits.empty());
19  return unsafe_string2unsigned(id2string(integer_bits));
20 }
21 
22 std::size_t floatbv_typet::get_f() const
23 {
24  const irep_idt &f=get(ID_f);
25  assert(!f.empty());
27 }
28 
30  const irep_idt &component_name) const
31 {
32  const componentst &c=components();
33 
34  std::size_t number=0;
35 
36  for(componentst::const_iterator
37  it=c.begin();
38  it!=c.end();
39  it++)
40  {
41  if(it->get_name()==component_name)
42  return number;
43 
44  number++;
45  }
46 
47  assert(false);
48  return 0;
49 }
50 
52  const irep_idt &component_name) const
53 {
54  const componentst &c=components();
55 
56  for(componentst::const_iterator
57  it=c.begin();
58  it!=c.end();
59  it++)
60  {
61  if(it->get_name()==component_name)
62  return *it;
63  }
64 
65  return static_cast<const componentt &>(get_nil_irep());
66 }
67 
69  const irep_idt &component_name) const
70 {
71  const exprt c=get_component(component_name);
72  assert(c.is_not_nil());
73  return c.type();
74 }
75 
76 bool struct_typet::is_prefix_of(const struct_typet &other) const
77 {
78  const componentst &ot_components=other.components();
79  const componentst &tt_components=components();
80 
81  if(ot_components.size()<
82  tt_components.size())
83  return false;
84 
85  componentst::const_iterator
86  ot_it=ot_components.begin();
87 
88  for(componentst::const_iterator tt_it=
89  tt_components.begin();
90  tt_it!=tt_components.end();
91  tt_it++)
92  {
93  if(ot_it->type()!=tt_it->type() ||
94  ot_it->get(ID_name)!=tt_it->get(ID_name))
95  {
96  return false; // they just don't match
97  }
98 
99  ot_it++;
100  }
101 
102  return true; // ok, *this is a prefix of ot
103 }
104 
105 bool is_reference(const typet &type)
106 {
107  return type.id()==ID_pointer &&
108  type.get_bool(ID_C_reference);
109 }
110 
111 bool is_rvalue_reference(const typet &type)
112 {
113  return type.id()==ID_pointer &&
114  type.get_bool(ID_C_rvalue_reference);
115 }
116 
118 {
119  set(ID_from, integer2string(from));
120 }
121 
123 {
124  set(ID_to, integer2string(to));
125 }
126 
128 {
129  return string2integer(get_string(ID_from));
130 }
131 
133 {
134  return string2integer(get_string(ID_to));
135 }
136 
138 {
139  return -power(2, get_width()-1);
140 }
141 
143 {
144  return power(2, get_width()-1)-1;
145 }
146 
148 {
149  return to_constant_expr(from_integer(0, *this));
150 }
151 
153 {
154  return to_constant_expr(from_integer(smallest(), *this));
155 }
156 
158 {
159  return to_constant_expr(from_integer(largest(), *this));
160 }
161 
163 {
164  return 0;
165 }
166 
168 {
169  return power(2, get_width())-1;
170 }
171 
173 {
174  return to_constant_expr(from_integer(0, *this));
175 }
176 
178 {
179  return to_constant_expr(from_integer(smallest(), *this));
180 }
181 
183 {
184  return to_constant_expr(from_integer(largest(), *this));
185 }
const irept & get_nil_irep()
Definition: irep.cpp:56
The type of an expression.
Definition: type.h:20
constant_exprt zero_expr() const
Definition: std_types.cpp:172
BigInt mp_integer
Definition: mp_arith.h:19
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
constant_exprt largest_expr() const
Definition: std_types.cpp:182
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:53
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:104
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:66
std::size_t get_integer_bits() const
Definition: std_types.cpp:15
std::vector< componentt > componentst
Definition: std_types.h:240
const componentst & components() const
Definition: std_types.h:242
typet & type()
Definition: expr.h:60
A constant literal expression.
Definition: std_expr.h:3685
Structure type.
Definition: std_types.h:296
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
mp_integer get_to() const
Definition: std_types.cpp:132
const irep_idt & id() const
Definition: irep.h:189
constant_exprt smallest_expr() const
Definition: std_types.cpp:152
API to expression classes.
bool is_reference(const typet &type)
TO_BE_DOCUMENTED.
Definition: std_types.cpp:105
mp_integer smallest() const
Definition: std_types.cpp:162
void set_from(const mp_integer &_from)
Definition: std_types.cpp:117
mp_integer largest() const
Definition: std_types.cpp:167
mp_integer smallest() const
Definition: std_types.cpp:137
typet component_type(const irep_idt &component_name) const
Definition: std_types.cpp:68
std::size_t get_width() const
Definition: std_types.h:1030
std::size_t get_f() const
Definition: std_types.cpp:22
API to type classes.
mp_integer largest() const
Definition: std_types.cpp:142
bool is_prefix_of(const struct_typet &other) const
Definition: std_types.cpp:76
constant_exprt largest_expr() const
Definition: std_types.cpp:157
Base class for all expressions.
Definition: expr.h:46
bool is_rvalue_reference(const typet &type)
TO_BE_DOCUMENTED.
Definition: std_types.cpp:111
std::size_t component_number(const irep_idt &component_name) const
Definition: std_types.cpp:29
constant_exprt smallest_expr() const
Definition: std_types.cpp:177
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
void set_to(const mp_integer &to)
Definition: std_types.cpp:122
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bool empty() const
Definition: dstring.h:61
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
const componentt & get_component(const irep_idt &component_name) const
Definition: std_types.cpp:51
constant_exprt zero_expr() const
Definition: std_types.cpp:147
mp_integer get_from() const
Definition: std_types.cpp:127