diff --git a/regression/cbmc-java/generic_class_bound1/A.class b/regression/cbmc-java/generic_class_bound1/A.class new file mode 100644 index 00000000000..91bb322316e Binary files /dev/null and b/regression/cbmc-java/generic_class_bound1/A.class differ diff --git a/regression/cbmc-java/generic_class_bound1/B.class b/regression/cbmc-java/generic_class_bound1/B.class new file mode 100644 index 00000000000..8e6e449cff3 Binary files /dev/null and b/regression/cbmc-java/generic_class_bound1/B.class differ diff --git a/regression/cbmc-java/generic_class_bound1/C.class b/regression/cbmc-java/generic_class_bound1/C.class new file mode 100644 index 00000000000..7b228a9c4b5 Binary files /dev/null and b/regression/cbmc-java/generic_class_bound1/C.class differ diff --git a/regression/cbmc-java/generic_class_bound1/Gn.class b/regression/cbmc-java/generic_class_bound1/Gn.class new file mode 100644 index 00000000000..5513d09916c Binary files /dev/null and b/regression/cbmc-java/generic_class_bound1/Gn.class differ diff --git a/regression/cbmc-java/generic_class_bound1/Gn.java b/regression/cbmc-java/generic_class_bound1/Gn.java new file mode 100644 index 00000000000..5dfbf4da153 --- /dev/null +++ b/regression/cbmc-java/generic_class_bound1/Gn.java @@ -0,0 +1,15 @@ +interface A{} +interface B{} +interface C{} +interface L extends A,B,C{} + +public class Gn>{ + Gn ex1; + public void foo1(Gn ex1){ + if(ex1 != null) + this.ex1 = ex1; + } + public static void main(String[] args) { + System.out.println("ddfsdf"); + } +} diff --git a/regression/cbmc-java/generic_class_bound1/L.class b/regression/cbmc-java/generic_class_bound1/L.class new file mode 100644 index 00000000000..9c1bc26523e Binary files /dev/null and b/regression/cbmc-java/generic_class_bound1/L.class differ diff --git a/regression/cbmc-java/generic_class_bound1/test.desc b/regression/cbmc-java/generic_class_bound1/test.desc new file mode 100644 index 00000000000..3ac218b6d84 --- /dev/null +++ b/regression/cbmc-java/generic_class_bound1/test.desc @@ -0,0 +1,11 @@ +CORE +Gn.class +--cover location +^EXIT=0$ +^SIGNAL=0$ +.*file Gn.java line 6 function java::Gn.\:\(\)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 +-- diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index 3f61e14ccba..ad928710f5b 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -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 `` for classes +/// or `` for interfaces. /// /// For example for `HashMap` a vector with two elements would be returned /// @@ -607,8 +609,9 @@ std::vector java_generic_type_from_string( const std::string &class_name, const std::string &src) { - /// the class signature is of the form - size_t signature_end=find_closing_delimiter(src, 0, '<', '>'); + /// the class signature is of the form or of + /// the form 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 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)); diff --git a/unit/java_bytecode/java_bytecode_parse_generics/BoundedGenericClasses.java b/unit/java_bytecode/java_bytecode_parse_generics/BoundedGenericClasses.java new file mode 100644 index 00000000000..aef709de3cd --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/BoundedGenericClasses.java @@ -0,0 +1,8 @@ +class C{ +} +interface I{ +} +class interface_bound { +} +class class_bound { +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/C.class b/unit/java_bytecode/java_bytecode_parse_generics/C.class new file mode 100644 index 00000000000..4164c648fa1 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/C.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/I.class b/unit/java_bytecode/java_bytecode_parse_generics/I.class new file mode 100644 index 00000000000..a97d0a359f0 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/I.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/class_bound.class b/unit/java_bytecode/java_bytecode_parse_generics/class_bound.class new file mode 100644 index 00000000000..491247b9fef Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/class_bound.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/interface_bound.class b/unit/java_bytecode/java_bytecode_parse_generics/interface_bound.class new file mode 100644 index 00000000000..bf6552e0cfb Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/interface_bound.class differ