Skip to content

Change package to org.cprover for three classes #2941

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Sep 13, 2018
Merged

Change package to org.cprover for three classes #2941

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Binary file removed jbmc/regression/jbmc/overlay-class/annotations/com/diffblue/OverlayClassImplementation.class
View file
Open in desktop
Binary file not shown.
Binary file removed .../regression/jbmc/overlay-class/annotations/com/diffblue/OverlayMethodImplementation.class
View file
Open in desktop
Binary file not shown.
Binary file added jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayClassImplementation.class
View file
Open in desktop
Binary file not shown.
2 changes: 1 addition & 1 deletion .../diffblue/OverlayClassImplementation.java → ...g/cprover/OverlayClassImplementation.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
package com.diffblue;
package org.cprover;

public @interface OverlayClassImplementation {
}
Binary file added jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayMethodImplementation.class
View file
Open in desktop
Binary file not shown.
2 changes: 1 addition & 1 deletion ...diffblue/OverlayMethodImplementation.java → .../cprover/OverlayMethodImplementation.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
package com.diffblue;
package org.cprover;

public @interface OverlayMethodImplementation {
}
Binary file modified jbmc/regression/jbmc/overlay-class/correct-overlay/Test.class
View file
Open in desktop
Binary file not shown.
4 changes: 2 additions & 2 deletions jbmc/regression/jbmc/overlay-class/correct-overlay/Test.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import com.diffblue.OverlayClassImplementation;
import com.diffblue.OverlayMethodImplementation;
import org.cprover.OverlayClassImplementation;
import org.cprover.OverlayMethodImplementation;

@OverlayClassImplementation
public class Test
Expand Down
Binary file modified jbmc/regression/jbmc/overlay-class/unmarked-overlay/Test.class
View file
Open in desktop
Binary file not shown.
4 changes: 2 additions & 2 deletions jbmc/regression/jbmc/overlay-class/unmarked-overlay/Test.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import com.diffblue.OverlayClassImplementation;
import com.diffblue.OverlayMethodImplementation;
import org.cprover.OverlayClassImplementation;
import org.cprover.OverlayMethodImplementation;

public class Test
{
Expand Down
4 changes: 2 additions & 2 deletions jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/java_class_loader.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
6 changes: 3 additions & 3 deletions src/util/irep_ids.def
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down