Merge pull request #1533 from mgudemann/fix/support_class_bounds_generics

TG-1179 Skip '::' instead of just ':' for class bounds in generics

Author: Matthias Güdemann

regression/cbmc-java/generic_class_bound1/A.class

@@ -0,0 +1,15 @@
+interface A{}
+interface B{}
+interface C{}
+interface L<T> extends A,B,C{}
+
+public class Gn<T extends L<? extends B>>{
+	Gn<?> ex1;
+	public void foo1(Gn<?> ex1){
+		if(ex1 != null)
+		this.ex1 = ex1;
+	}
+	public static void main(String[] args) {
+		System.out.println("ddfsdf");
+	}
+}

regression/cbmc-java/generic_class_bound1/B.class

@@ -0,0 +1,11 @@
+CORE
+Gn.class
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+.*file Gn.java line 6 function java::Gn.\<init\>:\(\)V bytecode-index 1 block 1: FAILED
+.*file Gn.java line 9 function java::Gn.foo1:\(LGn;\)V bytecode-index 1 block 1: FAILED
+.*file Gn.java line 10 function java::Gn.foo1:\(LGn;\)V bytecode-index 4 block 2: FAILED
+.*file Gn.java line 11 function java::Gn.foo1:\(LGn;\)V bytecode-index 5 block 3: FAILED
+.*file Gn.java line 13 function java::Gn.main:\(\[Ljava/lang/String;\)V bytecode-index 2 block 1: SATISFIED
+--

regression/cbmc-java/generic_class_bound1/C.class

@@ -599,6 +599,8 @@ char java_char_from_type(const typet &type)
 /// Converts the content of a generic class type into a vector of Java types,
 /// that is each type variable of the class has one entry in the returned
 /// vector.
+/// This also supports parsing of bounds in the form of `<T:CBound>` for classes
+/// or `<T::IBound>` for interfaces.
 ///
 /// For example for `HashMap<K, V>` a vector with two elements would be returned
 ///
@@ -607,8 +609,9 @@ std::vector<typet> java_generic_type_from_string(
   const std::string &class_name,
   const std::string &src)
 {
-  /// the class signature is of the form <TX:Bound_X;:BoundZ;TY:Bound_Y;>
-  size_t signature_end=find_closing_delimiter(src, 0, '<', '>');
+  /// the class signature is of the form <TX:Bound_X;:BoundZ;TY:Bound_Y;> or of
+  /// the form <TX::Bound_X;:BoundZ;TY:Bound_Y;> if Bound_X is an interface
+  size_t signature_end = find_closing_delimiter(src, 0, '<', '>');
   INVARIANT(
     src[0]=='<' && signature_end!=std::string::npos,
     "Class signature has unexpected format");
@@ -625,6 +628,16 @@ std::vector<typet> java_generic_type_from_string(
   {
     size_t bound_sep=signature.find(':');
     INVARIANT(bound_sep!=std::string::npos, "No bound for type variable.");
+
+    // is bound an interface?
+    // in this case the separator is '::'
+    if(signature[bound_sep + 1] == ':')
+    {
+      INVARIANT(
+        signature[bound_sep + 2] != ':', "Unknown bound for type variable.");
+      bound_sep++;
+    }
+
     std::string type_var_name(
       "java::"+class_name+"::"+signature.substr(0, bound_sep));
     std::string bound_type(signature.substr(bound_sep+1, var_sep-bound_sep));

regression/cbmc-java/generic_class_bound1/Gn.class

@@ -0,0 +1,8 @@
+class C{
+}
+interface I{
+}
+class interface_bound<T extends I> {
+}
+class class_bound<T extends C> {
+}