Skip to content

Commit 764c651

Browse files
andreast271andreast271
committed
Enable compilation with NDEBUG defined
Compilation used to fail since NDEBUG removes assertions, leading to unused variables. The commit replaces these assertions with INVARIANT or a derivative.
1 parent 99eb662 commit 764c651

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
@@ -537,7 +537,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
537537
vt_symb_type.is_type=true;
538538

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

542542
// add a virtual-table pointer
543543
struct_typet::componentt compo;
@@ -613,7 +613,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
613613

614614
// add the parameter to the symbol table
615615
const bool failed=!symbol_table.insert(std::move(arg_symb)).second;
616-
assert(!failed);
616+
CHECK_RETURN(!failed);
617617
}
618618

619619
// do the body of the function
@@ -671,7 +671,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
671671
// add the function to the symbol table
672672
{
673673
const bool failed=!symbol_table.insert(std::move(func_symb)).second;
674-
assert(!failed);
674+
CHECK_RETURN(!failed);
675675
}
676676

677677
// 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
@@ -1320,8 +1320,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
13201320
"java::org.cprover.CProver.assume:(Z)V")
13211321
{
13221322
const code_typet &code_type=to_code_type(arg0.type());
1323-
// sanity check: function has the right number of args
1324-
assert(code_type.parameters().size()==1);
1323+
INVARIANT(code_type.parameters().size()==1,
1324+
"function expected to have exactly one parameter");
13251325

13261326
exprt operand = pop(1)[0];
13271327
// we may need to adjust the type of the argument
@@ -1384,7 +1384,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
13841384
if(use_this)
13851385
{
13861386
const exprt &this_arg=call.arguments().front();
1387-
assert(this_arg.type().id()==ID_pointer);
1387+
INVARIANT(this_arg.type().id()==ID_pointer,
1388+
"first argument must be a pointer");
13881389
}
13891390

13901391
// do some type adjustment for the arguments,

‎src/java_bytecode/java_bytecode_parser.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -635,7 +635,7 @@ void java_bytecode_parsert::rfields(classt &parsed_class)
635635
size_t flags=(field.is_public?1:0)+
636636
(field.is_protected?1:0)+
637637
(field.is_private?1:0);
638-
assert(flags<=1);
638+
DATA_INVARIANT(flags<=1, "at most one of public, protected, private");
639639

640640
for(std::size_t j=0; j<attributes_count; j++)
641641
rfield_attribute(field);
@@ -1361,7 +1361,7 @@ void java_bytecode_parsert::rmethod(classt &parsed_class)
13611361
size_t flags=(method.is_public?1:0)+
13621362
(method.is_protected?1:0)+
13631363
(method.is_private?1:0);
1364-
assert(flags<=1);
1364+
DATA_INVARIANT(flags<=1, "at most one of public, protected, private");
13651365
u2 attributes_count=read_u2();
13661366

13671367
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)