Skip to content

Commit 0de60c2

Browse files
committed
ebmc var_map: use ebmc_errort instead of assert(...)
This replaces legacy error reporting via std::cerr and assert(...) by throwing an ebmc_errort() exception.
1 parent 442200f commit 0de60c2

File tree

1 file changed

+12
-19
lines changed

1 file changed

+12
-19
lines changed

src/trans-netlist/var_map.cpp

Lines changed: 12 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -6,13 +6,11 @@ Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

9-
#include <cassert>
10-
#include <iostream>
9+
#include "var_map.h"
1110

11+
#include <ebmc/ebmc_error.h>
1212
#include <solvers/flattening/boolbv_width.h>
1313

14-
#include "var_map.h"
15-
1614
/*******************************************************************\
1715
1816
Function: var_mapt::add
@@ -112,20 +110,19 @@ const var_mapt::vart::bitt &var_mapt::get_bit(
112110

113111
if(it==map.end())
114112
{
115-
std::cerr << "failed to find identifier "
116-
<< id << "[" << bit_nr << "]" << std::endl;
117-
assert(false);
113+
throw ebmc_errort() << "failed to find identifier " << id << '[' << bit_nr
114+
<< "] in var_map";
118115
}
119116

120-
assert(it->second.bits.size()!=0);
117+
if(it->second.bits.size() == 0)
118+
throw ebmc_errort() << "var_map entry with size zero";
121119

122120
if(bit_nr>=it->second.bits.size())
123121
{
124-
std::cerr << "index out of range for "
125-
<< id << "[" << bit_nr << "]" << std::endl;
126-
std::cerr << "available range: 0.."
127-
<< it->second.bits.size()-1 << std::endl;
128-
assert(false);
122+
throw ebmc_errort() << "index out of range for " << id << "[" << bit_nr
123+
<< "]\n"
124+
"available range: 0.."
125+
<< it->second.bits.size() - 1;
129126
}
130127

131128
return it->second.bits[bit_nr];
@@ -150,9 +147,7 @@ var_mapt::vart::vartypet var_mapt::get_type(
150147

151148
if(it==map.end())
152149
{
153-
std::cerr << "failed to find identifier "
154-
<< id << std::endl;
155-
assert(false);
150+
throw ebmc_errort() << "failed to find identifier " << id << " in var_map";
156151
}
157152

158153
return it->second.vartype;
@@ -176,9 +171,7 @@ const bv_varidt &var_mapt::reverse(unsigned v) const
176171

177172
if(it==reverse_map.end())
178173
{
179-
std::cerr << "failed to find variable "
180-
<< v << std::endl;
181-
assert(false);
174+
throw ebmc_errort() << "failed to find variable " << v << " in var_map";
182175
}
183176

184177
return it->second;

0 commit comments

Comments
 (0)