diff --git a/jbmc/regression/jbmc/overlay-class/annotations/com/diffblue/OverlayClassImplementation.class b/jbmc/regression/jbmc/overlay-class/annotations/com/diffblue/OverlayClassImplementation.class deleted file mode 100644 index 49c5688dd41..00000000000 Binary files a/jbmc/regression/jbmc/overlay-class/annotations/com/diffblue/OverlayClassImplementation.class and /dev/null differ diff --git a/jbmc/regression/jbmc/overlay-class/annotations/com/diffblue/OverlayMethodImplementation.class b/jbmc/regression/jbmc/overlay-class/annotations/com/diffblue/OverlayMethodImplementation.class deleted file mode 100644 index cf6e1900736..00000000000 Binary files a/jbmc/regression/jbmc/overlay-class/annotations/com/diffblue/OverlayMethodImplementation.class and /dev/null differ diff --git a/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayClassImplementation.class b/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayClassImplementation.class new file mode 100644 index 00000000000..6b591d5a926 Binary files /dev/null and b/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayClassImplementation.class differ diff --git a/jbmc/regression/jbmc/overlay-class/annotations/com/diffblue/OverlayClassImplementation.java b/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayClassImplementation.java similarity index 69% rename from jbmc/regression/jbmc/overlay-class/annotations/com/diffblue/OverlayClassImplementation.java rename to jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayClassImplementation.java index 99021b8f6cc..5262c83ab2f 100644 --- a/jbmc/regression/jbmc/overlay-class/annotations/com/diffblue/OverlayClassImplementation.java +++ b/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayClassImplementation.java @@ -1,4 +1,4 @@ -package com.diffblue; +package org.cprover; public @interface OverlayClassImplementation { } diff --git a/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayMethodImplementation.class b/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayMethodImplementation.class new file mode 100644 index 00000000000..07dab94e6eb Binary files /dev/null and b/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayMethodImplementation.class differ diff --git a/jbmc/regression/jbmc/overlay-class/annotations/com/diffblue/OverlayMethodImplementation.java b/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayMethodImplementation.java similarity index 69% rename from jbmc/regression/jbmc/overlay-class/annotations/com/diffblue/OverlayMethodImplementation.java rename to jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayMethodImplementation.java index d3d7211f594..b885d4b6348 100644 --- a/jbmc/regression/jbmc/overlay-class/annotations/com/diffblue/OverlayMethodImplementation.java +++ b/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayMethodImplementation.java @@ -1,4 +1,4 @@ -package com.diffblue; +package org.cprover; public @interface OverlayMethodImplementation { } diff --git a/jbmc/regression/jbmc/overlay-class/correct-overlay/Test.class b/jbmc/regression/jbmc/overlay-class/correct-overlay/Test.class index c6caf42f66e..8f587a9bb7b 100644 Binary files a/jbmc/regression/jbmc/overlay-class/correct-overlay/Test.class and b/jbmc/regression/jbmc/overlay-class/correct-overlay/Test.class differ diff --git a/jbmc/regression/jbmc/overlay-class/correct-overlay/Test.java b/jbmc/regression/jbmc/overlay-class/correct-overlay/Test.java index 7618d61f874..567c87bff93 100644 --- a/jbmc/regression/jbmc/overlay-class/correct-overlay/Test.java +++ b/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 diff --git a/jbmc/regression/jbmc/overlay-class/unmarked-overlay/Test.class b/jbmc/regression/jbmc/overlay-class/unmarked-overlay/Test.class index 9153608f2ba..dbcbb705557 100644 Binary files a/jbmc/regression/jbmc/overlay-class/unmarked-overlay/Test.class and b/jbmc/regression/jbmc/overlay-class/unmarked-overlay/Test.class differ diff --git a/jbmc/regression/jbmc/overlay-class/unmarked-overlay/Test.java b/jbmc/regression/jbmc/overlay-class/unmarked-overlay/Test.java index 5fa843f407d..7ace05a411f 100644 --- a/jbmc/regression/jbmc/overlay-class/unmarked-overlay/Test.java +++ b/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 { diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index f8bc2e396bc..2a8d909d10f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/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. diff --git a/jbmc/src/java_bytecode/java_class_loader.cpp b/jbmc/src/java_bytecode/java_class_loader.cpp index 4bb583edb05..97431351e33 100644 --- a/jbmc/src/java_bytecode/java_class_loader.cpp +++ b/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, diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index cfbfe482ba0..d88dd5fb478 100644 --- a/src/util/irep_ids.def +++ b/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)