Skip to content

Commit 5d690ec

Browse files
NathanJPhillipsNathanJPhillips
committed
Added regression tests
1 parent 07ab18b commit 5d690ec

18 files changed

+179
-0
lines changed

‎regression/cbmc-java/overlay-class/Test.class

583 Bytes
Binary file not shown.

‎regression/cbmc-java/overlay-class/Test.java

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
public class Test
2+
{
3+
public int x;
4+
5+
public static void main(String[] args)
6+
{
7+
assert(false);
8+
}
9+
10+
public static void notOverlain()
11+
{
12+
assert(true);
13+
}
14+
}

‎regression/cbmc-java/overlay-class/annotations/com/diffblue/OverlayClassImplementation.class

185 Bytes
Binary file not shown.

‎regression/cbmc-java/overlay-class/annotations/com/diffblue/OverlayClassImplementation.java

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
package com.diffblue;
2+
3+
public @interface OverlayClassImplementation {
4+
}

‎regression/cbmc-java/overlay-class/annotations/com/diffblue/OverlayMethodImplementation.class

187 Bytes
Binary file not shown.

‎regression/cbmc-java/overlay-class/annotations/com/diffblue/OverlayMethodImplementation.java

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
package com.diffblue;
2+
3+
public @interface OverlayMethodImplementation {
4+
}

‎regression/cbmc-java/overlay-class/correct-overlay/Test.class

412 Bytes
Binary file not shown.

‎regression/cbmc-java/overlay-class/correct-overlay/Test.java

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
import com.diffblue.OverlayClassImplementation;
2+
import com.diffblue.OverlayMethodImplementation;
3+
4+
@OverlayClassImplementation
5+
public class Test
6+
{
7+
public int x;
8+
9+
@OverlayMethodImplementation
10+
public static void main(String[] args)
11+
{
12+
assert(true);
13+
}
14+
}

‎regression/cbmc-java/overlay-class/correct-test-win.desc

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE OS-WINDOWS
2+
Test.class
3+
--classpath '.;annotations;correct-overlay' --verbosity 10
4+
^Getting class `Test' from file \.\\Test\.class$
5+
^Getting class `Test' from file correct-overlay\\Test\.class$
6+
^Adding symbol from overlay class: field 'x'$
7+
^Adding symbol from overlay class: method 'java::Test\.<init>:\(\)V'$
8+
^Field definition for java::Test\.x already loaded from overlay class$
9+
^Adding symbol from overlay class: method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$
10+
^Method java::Test\.<init>:\(\)V exists in an overlay class without being marked as an overlay and also exists in the underlying class
11+
^Adding symbol: method 'java::Test\.notOverlain:\(\)V'$
12+
^VERIFICATION SUCCESSFUL$
13+
^EXIT=0$
14+
^SIGNAL=0$
15+
--
16+
^Skipping class Test marked with OverlayClassImplementation but found before original definition$
17+
^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$

‎regression/cbmc-java/overlay-class/correct-test.desc

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE OS-LINUX OS-MACOS
2+
Test.class
3+
--classpath .:annotations:correct-overlay --verbosity 10
4+
^Getting class `Test' from file \./Test\.class$
5+
^Getting class `Test' from file correct-overlay/Test\.class$
6+
^Adding symbol from overlay class: field 'x'$
7+
^Adding symbol from overlay class: method 'java::Test\.<init>:\(\)V'$
8+
^Field definition for java::Test\.x already loaded from overlay class$
9+
^Adding symbol from overlay class: method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$
10+
^Method java::Test\.<init>:\(\)V exists in an overlay class without being marked as an overlay and also exists in the underlying class
11+
^Adding symbol: method 'java::Test\.notOverlain:\(\)V'$
12+
^VERIFICATION SUCCESSFUL$
13+
^EXIT=0$
14+
^SIGNAL=0$
15+
--
16+
^Skipping class Test marked with OverlayClassImplementation but found before original definition$
17+
^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$

‎regression/cbmc-java/overlay-class/duplicate-test-win.desc

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE OS-WINDOWS
2+
Test.class
3+
--classpath '.;annotations;.;correct-overlay' --verbosity 10
4+
^Getting class `Test' from file \.\\Test\.class$
5+
^Getting class `Test' from file correct-overlay\\Test\.class$
6+
^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$
7+
^Adding symbol from overlay class: field 'x'$
8+
^Adding symbol from overlay class: method 'java::Test\.<init>:\(\)V'$
9+
^Field definition for java::Test\.x already loaded from overlay class$
10+
^Adding symbol from overlay class: method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$
11+
^Method java::Test\.<init>:\(\)V exists in an overlay class without being marked as an overlay and also exists in the underlying class
12+
^Adding symbol: method 'java::Test\.notOverlain:\(\)V'$
13+
^VERIFICATION SUCCESSFUL$
14+
^EXIT=0$
15+
^SIGNAL=0$
16+
--
17+
^Skipping class Test marked with OverlayClassImplementation but found before original definition$

‎regression/cbmc-java/overlay-class/duplicate-test.desc

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE OS-LINUX OS-MACOS
2+
Test.class
3+
--classpath .:annotations:.:correct-overlay --verbosity 10
4+
^Getting class `Test' from file \./Test\.class$
5+
^Getting class `Test' from file correct-overlay/Test\.class$
6+
^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$
7+
^Adding symbol from overlay class: field 'x'$
8+
^Adding symbol from overlay class: method 'java::Test\.<init>:\(\)V'$
9+
^Field definition for java::Test\.x already loaded from overlay class$
10+
^Adding symbol from overlay class: method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$
11+
^Method java::Test\.<init>:\(\)V exists in an overlay class without being marked as an overlay and also exists in the underlying class
12+
^Adding symbol: method 'java::Test\.notOverlain:\(\)V'$
13+
^VERIFICATION SUCCESSFUL$
14+
^EXIT=0$
15+
^SIGNAL=0$
16+
--
17+
^Skipping class Test marked with OverlayClassImplementation but found before original definition$

‎regression/cbmc-java/overlay-class/misordered-test-win.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE OS-WINDOWS
2+
Test.class
3+
--classpath 'annotations;correct-overlay;.' --verbosity 10
4+
^Getting class `Test' from file correct-overlay\\Test\.class$
5+
^Getting class `Test' from file \.\\Test\.class$
6+
^Skipping class Test marked with OverlayClassImplementation but found before original definition$
7+
^Adding symbol: field 'x'$
8+
^Adding symbol: method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$
9+
^Adding symbol: method 'java::Test\.notOverlain:\(\)V'$
10+
^VERIFICATION FAILED$
11+
^EXIT=10$
12+
^SIGNAL=0$
13+
--
14+
^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$
15+
^Adding symbol from overlay class
16+
exists in an overlay class without being marked as an overlay and also exists in the underlying class

‎regression/cbmc-java/overlay-class/misordered-test.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE OS-LINUX OS-MACOS
2+
Test.class
3+
--classpath annotations:correct-overlay:. --verbosity 10
4+
^Getting class `Test' from file correct-overlay/Test\.class$
5+
^Getting class `Test' from file \./Test\.class$
6+
^Skipping class Test marked with OverlayClassImplementation but found before original definition$
7+
^Adding symbol: field 'x'$
8+
^Adding symbol: method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$
9+
^Adding symbol: method 'java::Test\.notOverlain:\(\)V'$
10+
^VERIFICATION FAILED$
11+
^EXIT=10$
12+
^SIGNAL=0$
13+
--
14+
^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$
15+
^Adding symbol from overlay class
16+
exists in an overlay class without being marked as an overlay and also exists in the underlying class

‎regression/cbmc-java/overlay-class/unmarked-overlay/Test.class

601 Bytes
Binary file not shown.

‎regression/cbmc-java/overlay-class/unmarked-overlay/Test.java

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
import com.diffblue.OverlayClassImplementation;
2+
import com.diffblue.OverlayMethodImplementation;
3+
4+
public class Test
5+
{
6+
@OverlayMethodImplementation
7+
public static void main(String[] args)
8+
{
9+
assert(false);
10+
}
11+
}

‎regression/cbmc-java/overlay-class/unmarked-test-win.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE OS-WINDOWS
2+
Test.class
3+
--classpath '.;annotations;unmarked-overlay' --verbosity 10
4+
^Getting class `Test' from file \.\\Test\.class$
5+
^Getting class `Test' from file unmarked-overlay\\Test\.class$
6+
^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$
7+
^Adding symbol: field 'x'$
8+
^Adding symbol: method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$
9+
^Adding symbol: method 'java::Test\.notOverlain:\(\)V'$
10+
^VERIFICATION FAILED$
11+
^EXIT=10$
12+
^SIGNAL=0$
13+
--
14+
^Skipping class Test marked with OverlayClassImplementation but found before original definition$
15+
^Adding symbol from overlay class
16+
exists in an overlay class without being marked as an overlay and also exists in the underlying class

‎regression/cbmc-java/overlay-class/unmarked-test.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE OS-LINUX OS-MACOS
2+
Test.class
3+
--classpath .:annotations:unmarked-overlay --verbosity 10
4+
^Getting class `Test' from file \./Test\.class$
5+
^Getting class `Test' from file unmarked-overlay/Test\.class$
6+
^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$
7+
^Adding symbol: field 'x'$
8+
^Adding symbol: method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$
9+
^Adding symbol: method 'java::Test\.notOverlain:\(\)V'$
10+
^VERIFICATION FAILED$
11+
^EXIT=10$
12+
^SIGNAL=0$
13+
--
14+
^Skipping class Test marked with OverlayClassImplementation but found before original definition$
15+
^Adding symbol from overlay class
16+
exists in an overlay class without being marked as an overlay and also exists in the underlying class

0 commit comments

Comments
 (0)