Skip to content

Commit e3ed492

Browse files
committed
Fix typet::check usage to work with latest API
Fixes the build breakage caused by merging an old PR. We nowadays require a validation mode.
1 parent 075d97a commit e3ed492

File tree

2 files changed

+9
-7
lines changed

2 files changed

+9
-7
lines changed

src/util/std_types.h

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1130,7 +1130,8 @@ class bv_typet:public bitvector_typet
11301130
const typet &type,
11311131
const validation_modet vm = validation_modet::INVARIANT)
11321132
{
1133-
DATA_CHECK(!type.get(ID_width).empty(), "bitvector type must have width");
1133+
DATA_CHECK(
1134+
vm, !type.get(ID_width).empty(), "bitvector type must have width");
11341135
}
11351136
};
11361137

@@ -1241,7 +1242,7 @@ class signedbv_typet:public bitvector_typet
12411242
const validation_modet vm = validation_modet::INVARIANT)
12421243
{
12431244
DATA_CHECK(
1244-
!type.get(ID_width).empty(), "signed bitvector type must have width");
1245+
vm, !type.get(ID_width).empty(), "signed bitvector type must have width");
12451246
}
12461247
};
12471248

@@ -1305,7 +1306,7 @@ class fixedbv_typet:public bitvector_typet
13051306
const validation_modet vm = validation_modet::INVARIANT)
13061307
{
13071308
DATA_CHECK(
1308-
!type.get(ID_width).empty(), "fixed bitvector type must have width");
1309+
vm, !type.get(ID_width).empty(), "fixed bitvector type must have width");
13091310
}
13101311
};
13111312

@@ -1367,7 +1368,7 @@ class floatbv_typet:public bitvector_typet
13671368
const validation_modet vm = validation_modet::INVARIANT)
13681369
{
13691370
DATA_CHECK(
1370-
!type.get(ID_width).empty(), "float bitvector type must have width");
1371+
vm, !type.get(ID_width).empty(), "float bitvector type must have width");
13711372
}
13721373
};
13731374

@@ -1469,7 +1470,7 @@ class pointer_typet:public bitvector_typet
14691470
const typet &type,
14701471
const validation_modet vm = validation_modet::INVARIANT)
14711472
{
1472-
DATA_CHECK(!type.get(ID_width).empty(), "pointer must have width");
1473+
DATA_CHECK(vm, !type.get(ID_width).empty(), "pointer must have width");
14731474
}
14741475
};
14751476

@@ -1567,7 +1568,7 @@ class c_bool_typet:public bitvector_typet
15671568
const typet &type,
15681569
const validation_modet vm = validation_modet::INVARIANT)
15691570
{
1570-
DATA_CHECK(!type.get(ID_width).empty(), "C bool type must have width");
1571+
DATA_CHECK(vm, !type.get(ID_width).empty(), "C bool type must have width");
15711572
}
15721573
};
15731574

src/util/type.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -88,7 +88,8 @@ class typet:public irept
8888
///
8989
/// The validation mode indicates whether well-formedness check failures are
9090
/// reported via DATA_INVARIANT violations or exceptions.
91-
static void check(const typet &, const validation_modet)
91+
static void
92+
check(const typet &, const validation_modet = validation_modet::INVARIANT)
9293
{
9394
}
9495

0 commit comments

Comments
 (0)