Skip to content

Commit b1bf1ef

Browse files
committed
Adding tests for string.Equals constant short-circuit
1 parent 8615e3b commit b1bf1ef

File tree

3 files changed

+20
-0
lines changed

3 files changed

+20
-0
lines changed
Binary file not shown.
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
package string_refinement;
2+
3+
public class RefineStrings {
4+
public void constantComparison() {
5+
String helloWorld = "Hello world";
6+
assert helloWorld.equals(helloWorld());
7+
}
8+
9+
public String helloWorld() {
10+
return "Hello world";
11+
}
12+
}
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
RefineStrings.class
3+
--function string_refinement.RefineStrings.constantComparison --show-vcc --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
5+
--
6+
.*cprover_string_startswith_func*.
7+
--
8+
All instances of cprover_string_startswith_func can be calculated as false or true, so there should be no instances of this call.

0 commit comments

Comments
 (0)