We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 3d299a5 commit a284810Copy full SHA for a284810
jbmc/regression/jbmc/return-generic-member/Generic.class
366 Bytes
jbmc/regression/jbmc/return-generic-member/Test.class
453 Bytes
jbmc/regression/jbmc/return-generic-member/Test.java
@@ -0,0 +1,11 @@
1
+public class Test {
2
+
3
+ public Generic<Integer> field;
4
5
+ public Generic<Integer> main() {
6
+ return field;
7
+ }
8
9
+}
10
11
+class Generic<T> { }
jbmc/regression/jbmc/return-generic-member/test.desc
@@ -0,0 +1,13 @@
+CORE
+Test.class
+--function Test.main --validate-goto-model
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+This test ensures that the member_exprt generated to return a qualified generic
+field has the correct type, otherwise we'll fail model validation.
12
+Prior to ec4160829cc9c22ff71e647dd2894439720ad89c we would have created a
13
+non-matching type (Generic<Integer> vs. Generic)
0 commit comments