Skip to content

Commit bdee6fa

Browse files
antlechnerantlechner
committed
Add context-include tests for package and absent prefix
The tests in this commit would have all passed without the previous fixes already and are just added for completeness. The tested prefixes are a prefix of a package and a prefix that does not match anything on the classpath.
1 parent 151da10 commit bdee6fa

File tree

10 files changed

+49
-10
lines changed

10 files changed

+49
-10
lines changed

‎jbmc/regression/jbmc/context-include-exclude/Main.class

-106 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/context-include-exclude/Main.java

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
import org.cprover.MyClass;
2+
import org.cprover.other.MyOther;
23

34
public class Main {
45
public static void main(String[] args) {
@@ -7,9 +8,11 @@ public static void main(String[] args) {
78
MyClass m = new MyClass(y);
89
int z = m.get();
910
int w = MyClass.Inner.doIt(z);
11+
int u = MyOther.identity(w);
1012
assert(x == y);
1113
assert(y == z);
1214
assert(z == w);
15+
assert (w == u);
1316
}
1417

1518
public static int myMethod(int x) {

‎jbmc/regression/jbmc/context-include-exclude/org/cprover/other/MyOther.class

264 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/context-include-exclude/org/cprover/other/MyOther.java

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
package org.cprover.other;
2+
3+
public class MyOther {
4+
5+
public static int identity(int x) { return x; }
6+
}

‎jbmc/regression/jbmc/context-include-exclude/test_exclude_absent.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
Main.class
3+
--context-exclude org.cprover.oh
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
.* line 12 assertion at file Main.java line 12 .*: SUCCESS
7+
.* line 13 assertion at file Main.java line 13 .*: SUCCESS
8+
.* line 14 assertion at file Main.java line 14 .*: SUCCESS
9+
.* line 15 assertion at file Main.java line 15 .*: SUCCESS
10+
--
11+
--
12+
Tests that when --context-exclude is given a package prefix that does not occur
13+
anywhere on the classpath, it has no effect.

‎jbmc/regression/jbmc/context-include-exclude/test_exclude_from_all.desc

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,10 @@ Main.class
33
--context-exclude 'org.cprover.MyClass$Inner.'
44
^EXIT=10$
55
^SIGNAL=0$
6-
.* line 10 assertion at file Main.java line 10 .*: SUCCESS
7-
.* line 11 assertion at file Main.java line 11 .*: SUCCESS
8-
.* line 12 assertion at file Main.java line 12 .*: FAILURE
6+
.* line 12 assertion at file Main.java line 12 .*: SUCCESS
7+
.* line 13 assertion at file Main.java line 13 .*: SUCCESS
8+
.* line 14 assertion at file Main.java line 14 .*: FAILURE
9+
.* line 15 assertion at file Main.java line 15 .*: SUCCESS
910
--
1011
--
1112
Tests that no methods except those in the specified class are excluded.

‎jbmc/regression/jbmc/context-include-exclude/test_exclude_from_include.desc

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,10 @@ Main.class
33
--context-include Main.main --context-include 'Main.<clinit' --context-include org.cprover.MyClass --context-exclude 'org.cprover.MyClass$Inner.'
44
^EXIT=10$
55
^SIGNAL=0$
6-
.* line 10 assertion at file Main.java line 10 .*: FAILURE
7-
.* line 11 assertion at file Main.java line 11 .*: SUCCESS
86
.* line 12 assertion at file Main.java line 12 .*: FAILURE
7+
.* line 13 assertion at file Main.java line 13 .*: SUCCESS
8+
.* line 14 assertion at file Main.java line 14 .*: FAILURE
9+
.* line 15 assertion at file Main.java line 15 .*: FAILURE
910
--
1011
--
1112
Tests that only the specified methods and classes are included, while

‎jbmc/regression/jbmc/context-include-exclude/test_exclude_package_prefix.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
Main.class
3+
--context-include Main --context-include org.cprover --context-exclude org.cprover.ot
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
.* line 12 assertion at file Main.java line 12 .*: SUCCESS
7+
.* line 13 assertion at file Main.java line 13 .*: SUCCESS
8+
.* line 14 assertion at file Main.java line 14 .*: SUCCESS
9+
.* line 15 assertion at file Main.java line 15 .*: FAILURE
10+
--
11+
--
12+
Tests that --context-exclude works with an argument that is the prefix of a
13+
package name.

‎jbmc/regression/jbmc/context-include-exclude/test_include.desc

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,10 @@ Main.class
33
--context-include Main.
44
^EXIT=10$
55
^SIGNAL=0$
6-
.* line 10 assertion at file Main.java line 10 .*: SUCCESS
7-
.* line 11 assertion at file Main.java line 11 .*: FAILURE
8-
.* line 12 assertion at file Main.java line 12 .*: FAILURE
6+
.* line 12 assertion at file Main.java line 12 .*: SUCCESS
7+
.* line 13 assertion at file Main.java line 13 .*: FAILURE
8+
.* line 14 assertion at file Main.java line 14 .*: FAILURE
9+
.* line 15 assertion at file Main.java line 15 .*: FAILURE
910
--
1011
--
1112
Tests that only methods from the specified class are included.

‎jbmc/regression/jbmc/context-include-exclude/test_include_all.desc

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,10 @@ Main.class
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
.* line 10 assertion at file Main.java line 10 .*: SUCCESS
7-
.* line 11 assertion at file Main.java line 11 .*: SUCCESS
86
.* line 12 assertion at file Main.java line 12 .*: SUCCESS
7+
.* line 13 assertion at file Main.java line 13 .*: SUCCESS
8+
.* line 14 assertion at file Main.java line 14 .*: SUCCESS
9+
.* line 15 assertion at file Main.java line 15 .*: SUCCESS
910
--
1011
--
1112
Tests that no methods are excluded.

0 commit comments

Comments
 (0)