Skip to content

Commit 47e426f

Browse files
author
Thomas Kiley
authored
Merge pull request diffblue#1442 from andreast271/compilation-NDEBUG-enable
Enable compilation with NDEBUG defined
2 parents 869043a + 764c651 commit 47e426f

33 files changed

+126
-101
lines changed

‎src/ansi-c/c_nondet_symbol_factory.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -236,7 +236,7 @@ exprt c_nondet_symbol_factory(
236236

237237
symbolt *main_symbol_ptr;
238238
bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
239-
assert(!moving_symbol_failed);
239+
CHECK_RETURN(!moving_symbol_failed);
240240

241241
std::vector<symbolt const *> symbols_created;
242242
symbol_exprt main_symbol_expr=(*main_symbol_ptr).symbol_expr();

‎src/ansi-c/c_typecheck_initializer.cpp

+10-7
Original file line numberDiff line numberDiff line change
@@ -33,10 +33,10 @@ void c_typecheck_baset::do_initializer(
3333

3434
if(type.id()==ID_array)
3535
{
36-
// any arrays must have a size
3736
const typet &result_type=follow(result.type());
38-
assert(result_type.id()==ID_array &&
39-
to_array_type(result_type).size().is_not_nil());
37+
DATA_INVARIANT(result_type.id()==ID_array &&
38+
to_array_type(result_type).size().is_not_nil(),
39+
"any array must have a size");
4040

4141
// we don't allow initialisation with symbols of array type
4242
if(result.id()!=ID_array)
@@ -436,9 +436,11 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
436436
throw 0;
437437
}
438438

439-
assert(index<components.size());
440-
assert(components[index].type().id()!=ID_code &&
441-
!components[index].get_is_padding());
439+
DATA_INVARIANT(index<components.size(),
440+
"member designator is bounded by components size");
441+
DATA_INVARIANT(components[index].type().id()!=ID_code &&
442+
!components[index].get_is_padding(),
443+
"member designator points at data member");
442444

443445
dest=&(dest->operands()[index]);
444446
}
@@ -449,7 +451,8 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
449451
const union_typet::componentst &components=
450452
union_type.components();
451453

452-
assert(index<components.size());
454+
DATA_INVARIANT(index<components.size(),
455+
"member designator is bounded by components size");
453456

454457
const union_typet::componentt &component=union_type.components()[index];
455458

‎src/cpp/cpp_typecheck_compound_type.cpp

+3-3
Original file line numberDiff line numberDiff line change
@@ -535,7 +535,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
535535
vt_symb_type.is_type=true;
536536

537537
const bool failed=!symbol_table.insert(std::move(vt_symb_type)).second;
538-
assert(!failed);
538+
CHECK_RETURN(!failed);
539539

540540
// add a virtual-table pointer
541541
struct_typet::componentt compo;
@@ -611,7 +611,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
611611

612612
// add the parameter to the symbol table
613613
const bool failed=!symbol_table.insert(std::move(arg_symb)).second;
614-
assert(!failed);
614+
CHECK_RETURN(!failed);
615615
}
616616

617617
// do the body of the function
@@ -669,7 +669,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
669669
// add the function to the symbol table
670670
{
671671
const bool failed=!symbol_table.insert(std::move(func_symb)).second;
672-
assert(!failed);
672+
CHECK_RETURN(!failed);
673673
}
674674

675675
// next base

‎src/cpp/cpp_typecheck_constructor.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -486,8 +486,8 @@ void cpp_typecheckt::default_assignop_value(
486486

487487
mp_integer size;
488488
bool to_int=to_integer(size_expr, size);
489-
assert(!to_int);
490-
assert(size>=0);
489+
CHECK_RETURN(!to_int);
490+
CHECK_RETURN(size>=0);
491491

492492
exprt::operandst empty_operands;
493493
for(mp_integer i=0; i < size; ++i)

‎src/cpp/cpp_typecheck_initializer.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -215,8 +215,8 @@ void cpp_typecheckt::zero_initializer(
215215
mp_integer size;
216216

217217
bool to_int=to_integer(size_expr, size);
218-
assert(!to_int);
219-
assert(size>=0);
218+
CHECK_RETURN(!to_int);
219+
CHECK_RETURN(size>=0);
220220

221221
exprt::operandst empty_operands;
222222
for(mp_integer i=0; i<size; ++i)

‎src/cpp/cpp_typecheck_resolve.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -2125,7 +2125,8 @@ void cpp_typecheck_resolvet::apply_template_args(
21252125
const struct_typet &struct_type=
21262126
to_struct_type(type_symb.type);
21272127

2128-
assert(struct_type.has_component(new_symbol.name));
2128+
DATA_INVARIANT(struct_type.has_component(new_symbol.name),
2129+
"method should exist in struct");
21292130
member_exprt member(code_type);
21302131
member.set_component_name(new_symbol.name);
21312132
member.struct_op()=*fargs.operands.begin();

‎src/cpp/cpp_typecheck_virtual_table.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -96,6 +96,6 @@ void cpp_typecheckt::do_virtual_table(const symbolt &symbol)
9696
vt_symb_var.value=values;
9797

9898
bool failed=!symbol_table.insert(std::move(vt_symb_var)).second;
99-
assert(!failed);
99+
CHECK_RETURN(!failed);
100100
}
101101
}

‎src/goto-instrument/accelerate/polynomial.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -409,7 +409,7 @@ int monomialt::compare(monomialt &other)
409409
return -1;
410410
}
411411

412-
assert(!"NOTREACHEDBITCHES");
412+
UNREACHABLE;
413413
}
414414

415415
int polynomialt::max_degree(const exprt &var)

‎src/goto-instrument/accelerate/util.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -117,5 +117,6 @@ typet join_types(const typet &t1, const typet &t2)
117117
std::cerr << "Tried to join types: "
118118
<< t1.pretty() << " and " << t2.pretty()
119119
<< '\n';
120-
assert(!"Couldn't join types");
120+
121+
INVARIANT(false, "failed to join types");
121122
}

‎src/goto-instrument/full_slicer.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -185,7 +185,8 @@ void full_slicert::add_jumps(
185185
if(cfg[entry->second].node_required)
186186
{
187187
const irep_idt id2=goto_programt::get_function_id(*d_it);
188-
assert(id==id2);
188+
INVARIANT(id==id2,
189+
"goto/jump expected to be within a single function");
189190

190191
cfg_post_dominatorst::cfgt::entry_mapt::const_iterator e2=
191192
pd.cfg.entry_map.find(*d_it);

‎src/goto-instrument/unwind.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -119,7 +119,7 @@ class goto_unwindt
119119
const unsigned location_number)
120120
{
121121
auto r=location_map.insert(std::make_pair(target, location_number));
122-
assert(r.second); // did not exist yet
122+
INVARIANT(r.second, "target already exists");
123123
}
124124

125125
typedef std::map<goto_programt::const_targett, unsigned> location_mapt;

‎src/goto-instrument/wmm/event_graph.h

+3-3
Original file line numberDiff line numberDiff line change
@@ -406,9 +406,9 @@ class event_grapht
406406

407407
event_idt add_node()
408408
{
409-
const event_idt po_no = po_graph.add_node();
410-
const event_idt com_no = com_graph.add_node();
411-
assert(po_no == com_no);
409+
const event_idt po_no=po_graph.add_node();
410+
const event_idt com_no=com_graph.add_node();
411+
INVARIANT(po_no==com_no, "node added with same id in both graphs");
412412
return po_no;
413413
}
414414

‎src/goto-symex/symex_dereference.cpp

+3-2
Original file line numberDiff line numberDiff line change
@@ -221,8 +221,9 @@ exprt goto_symext::address_arithmetic(
221221
throw "goto_symext::address_arithmetic does not handle "+expr.id_string();
222222

223223
const typet &expr_type=ns.follow(expr.type());
224-
assert((expr_type.id()==ID_array && !keep_array) ||
225-
base_type_eq(pointer_type(expr_type), result.type(), ns));
224+
INVARIANT((expr_type.id()==ID_array && !keep_array) ||
225+
base_type_eq(pointer_type(expr_type), result.type(), ns),
226+
"either non-persistent array or pointer to result");
226227

227228
return result;
228229
}

‎src/java_bytecode/java_bytecode_convert_method.cpp

+4-3
Original file line numberDiff line numberDiff line change
@@ -1329,8 +1329,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
13291329
"java::org.cprover.CProver.assume:(Z)V")
13301330
{
13311331
const code_typet &code_type=to_code_type(arg0.type());
1332-
// sanity check: function has the right number of args
1333-
assert(code_type.parameters().size()==1);
1332+
INVARIANT(code_type.parameters().size()==1,
1333+
"function expected to have exactly one parameter");
13341334

13351335
exprt operand = pop(1)[0];
13361336
// we may need to adjust the type of the argument
@@ -1393,7 +1393,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
13931393
if(use_this)
13941394
{
13951395
const exprt &this_arg=call.arguments().front();
1396-
assert(this_arg.type().id()==ID_pointer);
1396+
INVARIANT(this_arg.type().id()==ID_pointer,
1397+
"first argument must be a pointer");
13971398
}
13981399

13991400
// do some type adjustment for the arguments,

‎src/java_bytecode/java_bytecode_parser.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -666,7 +666,7 @@ void java_bytecode_parsert::rfields(classt &parsed_class)
666666
size_t flags=(field.is_public?1:0)+
667667
(field.is_protected?1:0)+
668668
(field.is_private?1:0);
669-
assert(flags<=1);
669+
DATA_INVARIANT(flags<=1, "at most one of public, protected, private");
670670

671671
for(std::size_t j=0; j<attributes_count; j++)
672672
rfield_attribute(field);
@@ -1411,7 +1411,7 @@ void java_bytecode_parsert::rmethod(classt &parsed_class)
14111411
size_t flags=(method.is_public?1:0)+
14121412
(method.is_protected?1:0)+
14131413
(method.is_private?1:0);
1414-
assert(flags<=1);
1414+
DATA_INVARIANT(flags<=1, "at most one of public, protected, private");
14151415
u2 attributes_count=read_u2();
14161416

14171417
for(std::size_t j=0; j<attributes_count; j++)

‎src/pointer-analysis/value_set.cpp

+15-11
Original file line numberDiff line numberDiff line change
@@ -369,8 +369,9 @@ void value_sett::get_value_set_rec(
369369

370370
const typet &type=ns.follow(expr.op0().type());
371371

372-
assert(type.id()==ID_array ||
373-
type.id()==ID_incomplete_array);
372+
DATA_INVARIANT(type.id()==ID_array ||
373+
type.id()==ID_incomplete_array,
374+
"operand 0 of index expression must be an array");
374375

375376
get_value_set_rec(expr.op0(), dest, "[]"+suffix, original_type, ns);
376377
}
@@ -380,10 +381,11 @@ void value_sett::get_value_set_rec(
380381

381382
const typet &type=ns.follow(expr.op0().type());
382383

383-
assert(type.id()==ID_struct ||
384-
type.id()==ID_union ||
385-
type.id()==ID_incomplete_struct ||
386-
type.id()==ID_incomplete_union);
384+
DATA_INVARIANT(type.id()==ID_struct ||
385+
type.id()==ID_union ||
386+
type.id()==ID_incomplete_struct ||
387+
type.id()==ID_incomplete_union,
388+
"operand 0 of member expression must be struct or union");
387389

388390
const std::string &component_name=
389391
expr.get_string(ID_component_name);
@@ -1360,7 +1362,8 @@ void value_sett::assign_rec(
13601362

13611363
const typet &type=ns.follow(lhs.op0().type());
13621364

1363-
assert(type.id()==ID_array || type.id()==ID_incomplete_array);
1365+
DATA_INVARIANT(type.id()==ID_array || type.id()==ID_incomplete_array,
1366+
"operand 0 of index expression must be an array");
13641367

13651368
assign_rec(lhs.op0(), values_rhs, "[]"+suffix, ns, true);
13661369
}
@@ -1373,10 +1376,11 @@ void value_sett::assign_rec(
13731376

13741377
const typet &type=ns.follow(lhs.op0().type());
13751378

1376-
assert(type.id()==ID_struct ||
1377-
type.id()==ID_union ||
1378-
type.id()==ID_incomplete_struct ||
1379-
type.id()==ID_incomplete_union);
1379+
DATA_INVARIANT(type.id()==ID_struct ||
1380+
type.id()==ID_union ||
1381+
type.id()==ID_incomplete_struct ||
1382+
type.id()==ID_incomplete_union,
1383+
"operand 0 of member expression must be struct or union");
13801384

13811385
assign_rec(
13821386
lhs.op0(), values_rhs, "."+component_name+suffix, ns, add_to_sets);

‎src/pointer-analysis/value_set_fi.cpp

+18-14
Original file line numberDiff line numberDiff line change
@@ -412,9 +412,10 @@ void value_set_fit::get_value_set_rec(
412412

413413
const typet &type=ns.follow(expr.op0().type());
414414

415-
assert(type.id()==ID_array ||
416-
type.id()==ID_incomplete_array ||
417-
type.id()=="#REF#");
415+
DATA_INVARIANT(type.id()==ID_array ||
416+
type.id()==ID_incomplete_array ||
417+
type.id()=="#REF#",
418+
"operand 0 of index expression must be an array");
418419

419420
get_value_set_rec(expr.op0(), dest, "[]"+suffix,
420421
original_type, ns, recursion_set);
@@ -429,10 +430,11 @@ void value_set_fit::get_value_set_rec(
429430
{
430431
const typet &type=ns.follow(expr.op0().type());
431432

432-
assert(type.id()==ID_struct ||
433-
type.id()==ID_union ||
434-
type.id()==ID_incomplete_struct ||
435-
type.id()==ID_incomplete_union);
433+
DATA_INVARIANT(type.id()==ID_struct ||
434+
type.id()==ID_union ||
435+
type.id()==ID_incomplete_struct ||
436+
type.id()==ID_incomplete_union,
437+
"operand 0 of member expression must be struct or union");
436438

437439
const std::string &component_name=
438440
expr.get_string(ID_component_name);
@@ -1290,9 +1292,10 @@ void value_set_fit::assign_rec(
12901292

12911293
const typet &type=ns.follow(lhs.op0().type());
12921294

1293-
assert(type.id()==ID_array ||
1294-
type.id()==ID_incomplete_array ||
1295-
type.id()=="#REF#");
1295+
DATA_INVARIANT(type.id()==ID_array ||
1296+
type.id()==ID_incomplete_array ||
1297+
type.id()=="#REF#",
1298+
"operand 0 of index expression must be an array");
12961299

12971300
assign_rec(lhs.op0(), values_rhs, "[]"+suffix, ns, recursion_set);
12981301
}
@@ -1308,10 +1311,11 @@ void value_set_fit::assign_rec(
13081311

13091312
const typet &type=ns.follow(lhs.op0().type());
13101313

1311-
assert(type.id()==ID_struct ||
1312-
type.id()==ID_union ||
1313-
type.id()==ID_incomplete_struct ||
1314-
type.id()==ID_incomplete_union);
1314+
DATA_INVARIANT(type.id()==ID_struct ||
1315+
type.id()==ID_union ||
1316+
type.id()==ID_incomplete_struct ||
1317+
type.id()==ID_incomplete_union,
1318+
"operand 0 of member expression must be struct or union");
13151319

13161320
assign_rec(lhs.op0(), values_rhs, "."+component_name+suffix,
13171321
ns, recursion_set);

‎src/pointer-analysis/value_set_fivr.cpp

+18-14
Original file line numberDiff line numberDiff line change
@@ -525,9 +525,10 @@ void value_set_fivrt::get_value_set_rec(
525525

526526
const typet &type=ns.follow(expr.op0().type());
527527

528-
assert(type.id()==ID_array ||
529-
type.id()==ID_incomplete_array ||
530-
type.id()=="#REF#");
528+
DATA_INVARIANT(type.id()==ID_array ||
529+
type.id()==ID_incomplete_array ||
530+
type.id()=="#REF#",
531+
"operand 0 of index expression must be an array");
531532

532533
get_value_set_rec(expr.op0(), dest, "[]"+suffix,
533534
original_type, ns, recursion_set);
@@ -542,10 +543,11 @@ void value_set_fivrt::get_value_set_rec(
542543
{
543544
const typet &type=ns.follow(expr.op0().type());
544545

545-
assert(type.id()==ID_struct ||
546-
type.id()==ID_union ||
547-
type.id()==ID_incomplete_struct ||
548-
type.id()==ID_incomplete_union);
546+
DATA_INVARIANT(type.id()==ID_struct ||
547+
type.id()==ID_union ||
548+
type.id()==ID_incomplete_struct ||
549+
type.id()==ID_incomplete_union,
550+
"operand 0 of member expression must be struct or union");
549551

550552
const std::string &component_name=
551553
expr.get_string(ID_component_name);
@@ -1427,9 +1429,10 @@ void value_set_fivrt::assign_rec(
14271429

14281430
const typet &type=ns.follow(lhs.op0().type());
14291431

1430-
assert(type.id()==ID_array ||
1431-
type.id()==ID_incomplete_array ||
1432-
type.id()=="#REF#");
1432+
DATA_INVARIANT(type.id()==ID_array ||
1433+
type.id()==ID_incomplete_array ||
1434+
type.id()=="#REF#",
1435+
"operand 0 of index expression must be an array");
14331436

14341437
assign_rec(
14351438
lhs.op0(), values_rhs, "[]"+suffix, ns, recursion_set, add_to_sets);
@@ -1446,10 +1449,11 @@ void value_set_fivrt::assign_rec(
14461449

14471450
const typet &type=ns.follow(lhs.op0().type());
14481451

1449-
assert(type.id()==ID_struct ||
1450-
type.id()==ID_union ||
1451-
type.id()==ID_incomplete_struct ||
1452-
type.id()==ID_incomplete_union);
1452+
DATA_INVARIANT(type.id()==ID_struct ||
1453+
type.id()==ID_union ||
1454+
type.id()==ID_incomplete_struct ||
1455+
type.id()==ID_incomplete_union,
1456+
"operand 0 of member expression must be struct or union");
14531457

14541458
assign_rec(lhs.op0(), values_rhs, "."+component_name+suffix,
14551459
ns, recursion_set, add_to_sets);

0 commit comments

Comments
 (0)