Skip to content

Commit a27a935

Browse files
Test with list for --java-assume-inputs-interval
This tests that the option works for a list of interval rather than just a single one.
1 parent ade9e63 commit a27a935

File tree

4 files changed

+35
-0
lines changed

4 files changed

+35
-0
lines changed
Binary file not shown.

jbmc/regression/jbmc/assume-inputs-interval/My.java

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -188,4 +188,22 @@ public void classArrArg(Other other, int [] intArr) {
188188
assert false;
189189
}
190190
}
191+
192+
public static void intervalUnion(int intArg) {
193+
if (intArg == -3) {
194+
assert false;
195+
} else if (intArg == -1) {
196+
assert false;
197+
} else if (intArg == 0) {
198+
assert false;
199+
} else if (intArg == 1) {
200+
assert false;
201+
} else if (intArg == 3) {
202+
assert false;
203+
} else if (intArg == 6) {
204+
assert false;
205+
} else {
206+
assert false;
207+
}
208+
}
191209
}
Binary file not shown.
Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE
2+
My.class
3+
--function My.intervalUnion --java-assume-inputs-interval [-3:-2],[5:],[1:2]
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
\[java::My\.intervalUnion:\(I\)V\.assertion\.1\].[^$]*FAILURE
8+
\[java::My\.intervalUnion:\(I\)V\.assertion\.2\].[^$]*SUCCESS
9+
\[java::My\.intervalUnion:\(I\)V\.assertion\.3\].[^$]*SUCCESS
10+
\[java::My\.intervalUnion:\(I\)V\.assertion\.4\].[^$]*FAILURE
11+
\[java::My\.intervalUnion:\(I\)V\.assertion\.5\].[^$]*SUCCESS
12+
\[java::My\.intervalUnion:\(I\)V\.assertion\.6\].[^$]*FAILURE
13+
\[java::My\.intervalUnion:\(I\)V\.assertion\.7\].[^$]*FAILURE
14+
--
15+
^warning: ignoring
16+
--
17+
Check that --java-assume-inputs-interval works with multiple intervals.

0 commit comments

Comments
 (0)