Skip to content

Commit a13d103

Browse files
NathanJPhillipsNathanJPhillips
committed
Added regression tests
1 parent a2d9412 commit a13d103

19 files changed

+193
-0
lines changed

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

583 Bytes
Binary file not shown.

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

+14
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

+4
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

+4
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

+14
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

+17
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

+17
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

+17
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

+17
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

+16
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

+16
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

+11
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

+16
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

+16
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

‎regression/test.pl

+14
Original file line numberDiff line numberDiff line change
@@ -91,6 +91,7 @@ ($$$$$$$$$)
9191
# not given (implying run all tests) or it matches at least one include-tag.
9292

9393
my $include_tags_length = @$include_tags;
94+
# If any include tags are passed then only include tests including those tags
9495
my $passes_tag_tests = ($include_tags_length == 0);
9596
foreach my $include_tag (@$include_tags) {
9697
if(exists($tags_set{$include_tag})) {
@@ -104,6 +105,19 @@ ($$$$$$$$$)
104105
}
105106
}
106107

108+
# Exclude tests that have an OS- tag that doesn't match the current
109+
# architecture
110+
my $os;
111+
if($^O eq "linux") { $os = "LINUX" }
112+
if($^O eq "cygwin") { $os = "WINDOWS" }
113+
if($^O eq "msys") { $os = "WINDOWS" }
114+
if($^O eq "MSWin32") { $os = "WINDOWS" }
115+
if($^O eq "darwin") { $os = "MACOS" }
116+
117+
if(not exists($tags_set{"OS-" . $os}) and grep { "OS-" eq substr($_, 0, length("OS-")) } @tags) {
118+
$passes_tag_tests = 0;
119+
}
120+
107121
# If the 4th line is activate-multi-line-match we enable multi-line checks
108122
if($grep_options ne "activate-multi-line-match") {
109123
# No such flag, so we add it back in

0 commit comments

Comments
 (0)