Skip to content

Commit f6bbc9a

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 f6bbc9a

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+
}
Binary file not shown.
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

0 commit comments

Comments
 (0)