Skip to content

Commit 460ff53

Browse files
author
Sonny Martin
committed
Invariant cleanup
1 parent b0a0002 commit 460ff53

File tree

6 files changed

+39
-31
lines changed

6 files changed

+39
-31
lines changed

‎src/util/mp_arith.cpp‎

Lines changed: 11 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -257,9 +257,9 @@ mp_integer arith_left_shift(
257257
std::size_t true_size)
258258
{
259259
PRECONDITION(a.is_long() && b.is_ulong());
260+
PRECONDITION(b <= true_size || a == 0);
261+
260262
ullong_t shift=b.to_ulong();
261-
if(shift>true_size && a!=mp_integer(0))
262-
throw "shift value out of range";
263263

264264
llong_t result=a.to_long()<<shift;
265265
llong_t mask=
@@ -280,8 +280,7 @@ mp_integer arith_right_shift(
280280
PRECONDITION(a.is_long() && b.is_ulong());
281281
llong_t number=a.to_long();
282282
ullong_t shift=b.to_ulong();
283-
if(shift>true_size)
284-
throw "shift value out of range";
283+
DATA_INVARIANT(shift <= true_size, "shift value must be in range");
285284

286285
const llong_t sign = (1LL << (true_size - 1)) & number;
287286
const llong_t pad = (sign == 0) ? 0 : ~((1LL << (true_size - shift)) - 1);
@@ -298,9 +297,9 @@ mp_integer logic_left_shift(
298297
std::size_t true_size)
299298
{
300299
PRECONDITION(a.is_long() && b.is_ulong());
300+
PRECONDITION(b <= true_size || a == 0);
301+
301302
ullong_t shift=b.to_ulong();
302-
if(shift>true_size && a!=mp_integer(0))
303-
throw "shift value out of range";
304303
llong_t result=a.to_long()<<shift;
305304
if(true_size<(sizeof(llong_t)*8))
306305
{
@@ -324,10 +323,9 @@ mp_integer logic_right_shift(
324323
std::size_t true_size)
325324
{
326325
PRECONDITION(a.is_long() && b.is_ulong());
327-
ullong_t shift=b.to_ulong();
328-
if(shift>true_size)
329-
throw "shift value out of range";
326+
PRECONDITION(b <= true_size);
330327

328+
ullong_t shift = b.to_ulong();
331329
ullong_t result=((ullong_t)a.to_long()) >> shift;
332330
return result;
333331
}
@@ -341,10 +339,10 @@ mp_integer rotate_right(
341339
std::size_t true_size)
342340
{
343341
PRECONDITION(a.is_ulong() && b.is_ulong());
342+
PRECONDITION(b <= true_size);
343+
344344
ullong_t number=a.to_ulong();
345345
ullong_t shift=b.to_ulong();
346-
if(shift>true_size)
347-
throw "shift value out of range";
348346

349347
ullong_t revShift=true_size-shift;
350348
const ullong_t filter = 1ULL << (true_size - 1);
@@ -361,10 +359,10 @@ mp_integer rotate_left(
361359
std::size_t true_size)
362360
{
363361
PRECONDITION(a.is_ulong() && b.is_ulong());
362+
PRECONDITION(b <= true_size);
363+
364364
ullong_t number=a.to_ulong();
365365
ullong_t shift=b.to_ulong();
366-
if(shift>true_size)
367-
throw "shift value out of range";
368366

369367
ullong_t revShift=true_size-shift;
370368
const ullong_t filter = 1ULL << (true_size - 1);

‎src/util/namespace.cpp‎

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -80,24 +80,27 @@ const typet &namespace_baset::follow(const typet &src) const
8080
const typet &namespace_baset::follow_tag(const union_tag_typet &src) const
8181
{
8282
const symbolt &symbol=lookup(src.get_identifier());
83-
assert(symbol.is_type);
84-
assert(symbol.type.id()==ID_union || symbol.type.id()==ID_incomplete_union);
83+
CHECK_RETURN(symbol.is_type);
84+
CHECK_RETURN(
85+
symbol.type.id() == ID_union || symbol.type.id() == ID_incomplete_union);
8586
return symbol.type;
8687
}
8788

8889
const typet &namespace_baset::follow_tag(const struct_tag_typet &src) const
8990
{
9091
const symbolt &symbol=lookup(src.get_identifier());
91-
assert(symbol.is_type);
92-
assert(symbol.type.id()==ID_struct || symbol.type.id()==ID_incomplete_struct);
92+
CHECK_RETURN(symbol.is_type);
93+
CHECK_RETURN(
94+
symbol.type.id() == ID_struct || symbol.type.id() == ID_incomplete_struct);
9395
return symbol.type;
9496
}
9597

9698
const typet &namespace_baset::follow_tag(const c_enum_tag_typet &src) const
9799
{
98100
const symbolt &symbol=lookup(src.get_identifier());
99-
assert(symbol.is_type);
100-
assert(symbol.type.id()==ID_c_enum || symbol.type.id()==ID_incomplete_c_enum);
101+
CHECK_RETURN(symbol.is_type);
102+
CHECK_RETURN(
103+
symbol.type.id() == ID_c_enum || symbol.type.id() == ID_incomplete_c_enum);
101104
return symbol.type;
102105
}
103106

‎src/util/namespace.h‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
1010
#ifndef CPROVER_UTIL_NAMESPACE_H
1111
#define CPROVER_UTIL_NAMESPACE_H
1212

13+
#include "invariant.h"
1314
#include "irep.h"
1415

1516
class symbol_tablet;
@@ -33,8 +34,11 @@ class namespace_baset
3334
const symbolt &lookup(const irep_idt &name) const
3435
{
3536
const symbolt *symbol;
36-
if(lookup(name, symbol))
37-
throw "identifier "+id2string(name)+" not found";
37+
bool not_found = lookup(name, symbol);
38+
INVARIANT(
39+
!not_found,
40+
"We are assuming that a name exists in the namespace "
41+
"when this function is called");
3842
return *symbol;
3943
}
4044

‎src/util/pointer_predicates.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -226,7 +226,7 @@ exprt object_lower_bound(
226226
exprt p_offset=pointer_offset(pointer);
227227

228228
exprt zero=from_integer(0, p_offset.type());
229-
assert(zero.is_not_nil());
229+
CHECK_RETURN(zero.is_not_nil());
230230

231231
if(offset.is_not_nil())
232232
{

‎src/util/rational.cpp‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
1010
/// Rational Numbers
1111

1212
#include "rational.h"
13+
#include "invariant.h"
1314

1415
#include <algorithm>
1516
#include <ostream>
@@ -48,7 +49,7 @@ rationalt &rationalt::operator*=(const rationalt &n)
4849

4950
rationalt &rationalt::operator/=(const rationalt &n)
5051
{
51-
assert(!n.numerator.is_zero());
52+
PRECONDITION(!n.numerator.is_zero());
5253
numerator*=n.denominator;
5354
denominator*=n.numerator;
5455
normalize();
@@ -90,7 +91,7 @@ void rationalt::same_denominator(rationalt &n)
9091

9192
void rationalt::invert()
9293
{
93-
assert(numerator!=0);
94+
PRECONDITION(numerator != 0);
9495
std::swap(numerator, denominator);
9596
}
9697

‎src/util/reference_counting.h‎

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com
1414

1515
#include <cassert>
1616

17+
#include "invariant.h"
18+
1719
template<typename T>
1820
// NOLINTNEXTLINE(readability/identifiers)
1921
class reference_counting
@@ -33,7 +35,7 @@ class reference_counting
3335
{
3436
if(d!=nullptr)
3537
{
36-
assert(d->ref_count!=0);
38+
PRECONDITION(d->ref_count != 0);
3739
d->ref_count++;
3840
#ifdef REFERENCE_COUNTING_DEBUG
3941
std::cout << "COPY " << d << " " << d->ref_count << '\n';
@@ -96,9 +98,9 @@ class reference_counting
9698

9799
void copy_from(const reference_counting &other)
98100
{
99-
assert(&other!=this); // check if we assign to ourselves
101+
PRECONDITION(&other != this); // check if we assign to ourselves
100102

101-
#ifdef REFERENCE_COUNTING_DEBUG
103+
#ifdef REFERENCE_COUNTING_DEBUG
102104
std::cout << "COPY " << (&other) << "\n";
103105
#endif
104106

@@ -121,9 +123,9 @@ void reference_counting<T>::remove_ref(dt *old_d)
121123
if(old_d==nullptr)
122124
return;
123125

124-
assert(old_d->ref_count!=0);
126+
PRECONDITION(old_d->ref_count != 0);
125127

126-
#ifdef REFERENCE_COUNTING_DEBUG
128+
#ifdef REFERENCE_COUNTING_DEBUG
127129
std::cout << "R: " << old_d << " " << old_d->ref_count << '\n';
128130
#endif
129131

@@ -172,9 +174,9 @@ void reference_counting<T>::detach()
172174
remove_ref(old_d);
173175
}
174176

175-
assert(d->ref_count==1);
177+
POSTCONDITION(d->ref_count == 1);
176178

177-
#ifdef REFERENCE_COUNTING_DEBUG
179+
#ifdef REFERENCE_COUNTING_DEBUG
178180
std::cout << "DETACH2: " << d << '\n'
179181
#endif
180182
}

0 commit comments

Comments
 (0)