@@ -27,7 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com
27
27
28
28
void inv_object_storet::output (std::ostream &out) const
29
29
{
30
- for (unsigned i=0 ; i<entries.size (); i++)
30
+ for (std:: size_t i=0 ; i<entries.size (); i++)
31
31
out << " STORE " << i << " : " << to_string (i, " " ) << ' \n ' ;
32
32
}
33
33
@@ -61,7 +61,7 @@ unsigned inv_object_storet::add(const exprt &expr)
61
61
62
62
assert (s!=" " );
63
63
64
- unsigned n=map.number (s);
64
+ mapt::number_type n=map.number (s);
65
65
66
66
if (n>=entries.size ())
67
67
{
@@ -188,11 +188,11 @@ void invariant_sett::add(
188
188
unsigned f_r=eq_set.find (p.first );
189
189
unsigned s_r=eq_set.find (p.second );
190
190
191
- for (unsigned f=0 ; f<eq_set.size (); f++)
191
+ for (std:: size_t f=0 ; f<eq_set.size (); f++)
192
192
{
193
193
if (eq_set.find (f)==f_r)
194
194
{
195
- for (unsigned s=0 ; s<eq_set.size (); s++)
195
+ for (std:: size_t s=0 ; s<eq_set.size (); s++)
196
196
if (eq_set.find (s)==s_r)
197
197
dest.insert (std::pair<unsigned , unsigned >(f, s));
198
198
}
@@ -209,7 +209,7 @@ void invariant_sett::add_eq(const std::pair<unsigned, unsigned> &p)
209
209
bool constant_seen=false ;
210
210
mp_integer c;
211
211
212
- for (unsigned i=0 ; i<eq_set.size (); i++)
212
+ for (std:: size_t i=0 ; i<eq_set.size (); i++)
213
213
{
214
214
if (eq_set.find (i)==r)
215
215
{
@@ -319,12 +319,12 @@ void invariant_sett::output(
319
319
INVARIANT_STRUCTURED (
320
320
object_store!=nullptr , nullptr_exceptiont, " Object store is null" );
321
321
322
- for (unsigned i=0 ; i<eq_set.size (); i++)
322
+ for (std:: size_t i=0 ; i<eq_set.size (); i++)
323
323
if (eq_set.is_root (i) &&
324
324
eq_set.count (i)>=2 )
325
325
{
326
326
bool first=true ;
327
- for (unsigned j=0 ; j<eq_set.size (); j++)
327
+ for (std:: size_t j=0 ; j<eq_set.size (); j++)
328
328
if (eq_set.find (j)==i)
329
329
{
330
330
if (first)
@@ -367,7 +367,7 @@ void invariant_sett::add_type_bounds(const exprt &expr, const typet &type)
367
367
368
368
if (type.id ()==ID_unsignedbv)
369
369
{
370
- unsigned op_width=to_unsignedbv_type (type).get_width ();
370
+ std:: size_t op_width=to_unsignedbv_type (type).get_width ();
371
371
372
372
if (op_width<=8 )
373
373
{
@@ -852,7 +852,7 @@ exprt invariant_sett::get_constant(const exprt &expr) const
852
852
unsigned r=eq_set.find (a);
853
853
854
854
// is it a constant?
855
- for (unsigned i=0 ; i<eq_set.size (); i++)
855
+ for (std:: size_t i=0 ; i<eq_set.size (); i++)
856
856
if (eq_set.find (i)==r)
857
857
{
858
858
const exprt &e=object_store->get_expr (i);
@@ -938,8 +938,8 @@ bool invariant_sett::make_union(const invariant_sett &other)
938
938
eq_set.intersection (other.eq_set );
939
939
940
940
// inequalities
941
- unsigned old_ne_set=ne_set.size ();
942
- unsigned old_le_set=le_set.size ();
941
+ std:: size_t old_ne_set=ne_set.size ();
942
+ std:: size_t old_le_set=le_set.size ();
943
943
944
944
intersection (ne_set, other.ne_set );
945
945
intersection (le_set, other.le_set );
0 commit comments