Add regression test for recursive generic-parameters

NathanJPhillips · Jun 7, 2018 · d196cf7 · d196cf7
1 parent d7b1572
commit d196cf7
Show file tree

Hide file tree

Showing 4 changed files with 20 additions and 0 deletions.
diff --git a/jbmc/regression/jbmc/generics_recursive_parameters/KeyValue.class b/jbmc/regression/jbmc/generics_recursive_parameters/KeyValue.class
diff --git a/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.class b/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.class
diff --git a/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.java b/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.java
@@ -0,0 +1,11 @@
+class KeyValue<K, V> {
+    KeyValue<K, V> next;
+    KeyValue<V, K> reverse;
+    K key;
+    V value;
+}
+class MutuallyRecursiveGenerics {
+  void f() {
+    KeyValue<String, Integer> example1;
+  }
+}
diff --git a/jbmc/regression/jbmc/generics_recursive_parameters/test.desc b/jbmc/regression/jbmc/generics_recursive_parameters/test.desc
@@ -0,0 +1,9 @@
+CORE
+MutuallyRecursiveGenerics.class
+--cover location --function MutuallyRecursiveGenerics.f
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This failed before due to infinite recursion in the way how the instantiated
+generic parameters were used. cf. TG-3067