Change package to org.cprover for three classes

Change from com.diffblue to org.cprover for IgnoredMethodImplementation,
OverlayClassImplementation and OverlayMethodImplementation.

Author: Owen

jbmc/regression/jbmc/overlay-class/correct-overlay/Test.java

@@ -1,5 +1,5 @@
-import com.diffblue.OverlayClassImplementation;
-import com.diffblue.OverlayMethodImplementation;
+import org.cprover.OverlayClassImplementation;
+import org.cprover.OverlayMethodImplementation;
 
 @OverlayClassImplementation
 public class Test

jbmc/regression/jbmc/overlay-class/unmarked-overlay/Test.java

@@ -1,5 +1,5 @@
-import com.diffblue.OverlayClassImplementation;
-import com.diffblue.OverlayMethodImplementation;
+import org.cprover.OverlayClassImplementation;
+import org.cprover.OverlayMethodImplementation;
 
 public class Test
 {

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -53,10 +53,10 @@ class java_bytecode_convert_classt:public messaget
   /// \remarks
   ///   Allows multiple definitions of the same class to appear on the
   ///   classpath, so long as all but the first definition are marked with the
-  ///   attribute `\@java::com.diffblue.OverlayClassImplementation`.
+  ///   attribute `\@java::org.cprover.OverlayClassImplementation`.
   ///   Overlay class definitions can contain methods with the same signature
   ///   as methods in the original class, so long as these are marked with the
-  ///   attribute `\@java::com.diffblue.OverlayMethodImplementation`; such
+  ///   attribute `\@java::org.cprover.OverlayMethodImplementation`; such
   ///   overlay methods are replaced in the original file with the version
   ///   found in the last overlay on the classpath. Later definitions can
   ///   also contain new supporting methods and fields that are merged in.

jbmc/src/java_bytecode/java_class_loader.cpp

@@ -88,7 +88,7 @@ static bool is_overlay_class(const java_bytecode_parse_treet::classt &c)
 /// \remarks
 ///   Allows multiple definitions of the same class to appear on the
 ///   classpath, so long as all but the first definition are marked with the
-///   attribute `\@java::com.diffblue.OverlayClassImplementation`.
+///   attribute `\@java::org.cprover.OverlayClassImplementation`.
 java_class_loadert::parse_tree_with_overlayst &
 java_class_loadert::get_parse_tree(
   java_class_loader_limitt &class_loader_limit,

src/util/irep_ids.def

@@ -668,9 +668,9 @@ IREP_ID_ONE(havoc_object)
 IREP_ID_TWO(overflow_shl, overflow-shl)
 IREP_ID_TWO(C_no_initialization_required, #no_initialization_required)
 IREP_ID_TWO(C_no_nondet_initialization, #no_nondet_initialization)
-IREP_ID_TWO(overlay_class, java::com.diffblue.OverlayClassImplementation)
-IREP_ID_TWO(overlay_method, java::com.diffblue.OverlayMethodImplementation)
-IREP_ID_TWO(ignored_method, java::com.diffblue.IgnoredMethodImplementation)
+IREP_ID_TWO(overlay_class, java::org.cprover.OverlayClassImplementation)
+IREP_ID_TWO(overlay_method, java::org.cprover.OverlayMethodImplementation)
+IREP_ID_TWO(ignored_method, java::org.cprover.IgnoredMethodImplementation)
 IREP_ID_ONE(is_annotation)
 IREP_ID_TWO(C_annotations, #annotations)
 IREP_ID_ONE(final)