Skip to content

Commit 5136721

Browse files
committed
Add test for casting after a clean or soft cast
An upcast can be implemented by &child->base rather than using a typecast_exprt, but in the case of a specialised generic we may still need a cast. Check that a cast is produced when expected.
1 parent a62b5da commit 5136721

File tree

5 files changed

+41
-0
lines changed

5 files changed

+41
-0
lines changed
357 Bytes
Binary file not shown.
Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
2+
public class base<T> { }
3+
4+
class test<T> extends base<T> {
5+
6+
public void main(boolean unknown) {
7+
8+
if(unknown)
9+
callee(getSpecialisedTest());
10+
else
11+
callee2(getUnspecialisedTest());
12+
13+
}
14+
15+
public test<String> getSpecialisedTest() { return new test<String>(); }
16+
public test<T> getUnspecialisedTest() { return new test<T>(); }
17+
18+
public void callee(base<String> b) { assert false; }
19+
public void callee2(base<T> b) { assert false; }
20+
21+
}
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
test.class
3+
--function test.main --show-goto-functions
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
this \. test\.callee:\(Lbase;\)V\(\(struct base \*\)&return_tmp0->@base\);
7+
this \. test\.callee2:\(Lbase;\)V\(&return_tmp1->@base\);
8+
--
9+
callee has a qualified base type, and so requires a cast.
10+
callee2 has the unqualified type that test<T> naturally inherits, so no cast is required.
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
test.class
3+
--function test.main
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
\[java::test\.callee:\(Lbase;\)V\.assertion\.1\] line 18 assertion at file base\.java line 18 function java::test\.callee:\(Lbase;\)V bytecode-index 5: FAILURE
8+
\[java::test\.callee2:\(Lbase;\)V\.assertion\.1\] line 19 assertion at file base\.java line 19 function java::test\.callee2:\(Lbase;\)V bytecode-index 5: FAILURE
9+
--
10+
^warning: ignoring
Binary file not shown.

0 commit comments

Comments
 (0)