Skip to content

Commit e7a4733

Browse files
tautschnigDaniel Kroening
authored and
Daniel Kroening
committed
Support typecast from bv_typet to pointer_typet
The fixes in 848e633 result in type casts from bv_typet to various other bitvector types being generated. Most cases were addressed in that commit, but support for casting to pointers was omitted. This follow-up commit fixes this, and adds a test specifically covering this case.
1 parent 2a0cb4e commit e7a4733

File tree

3 files changed

+40
-5
lines changed

3 files changed

+40
-5
lines changed

regression/cbmc/Typecast3/main.c

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
#include <assert.h>
2+
#include <stdlib.h>
3+
4+
int main()
5+
{
6+
int **s = malloc(sizeof(int *));
7+
for(int i = 0; i < sizeof(int *); ++i)
8+
{
9+
// A correct program would use (char *)s, but updating the pointer allows us
10+
// to reproduce a bug in CBMC (missing support for typecasts from bv_typet
11+
// to pointers).
12+
*((char *)&s + i) = 0;
13+
}
14+
assert(s[0] == 0);
15+
}

regression/cbmc/Typecast3/test.desc

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
CORE
2+
main.c
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
^warning: ignoring
9+
--
10+
This test makes sure we support bv_typet -> pointer type casts, avoiding
11+
warnings like:
12+
13+
warning: ignoring typecast
14+
* type: pointer
15+
* width: 64
16+
0: signedbv
17+
* width: 32
18+
* #c_type: signed_int
19+
0: typecast
20+
* type: bv
21+
* width: 64

src/solvers/flattening/bv_pointers.cpp

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -253,11 +253,10 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
253253

254254
if(op_type.id()==ID_pointer)
255255
return convert_bv(op);
256-
else if(op_type.id()==ID_signedbv ||
257-
op_type.id()==ID_unsignedbv ||
258-
op_type.id()==ID_bool ||
259-
op_type.id()==ID_c_enum ||
260-
op_type.id()==ID_c_enum_tag)
256+
else if(
257+
op_type.id() == ID_signedbv || op_type.id() == ID_unsignedbv ||
258+
op_type.id() == ID_bool || op_type.id() == ID_c_enum ||
259+
op_type.id() == ID_c_enum_tag || op_type.id() == ID_bv)
261260
{
262261
// Cast from integer to pointer.
263262
// We just do a zero extension.

0 commit comments

Comments
 (0)