File tree 4 files changed +55
-57
lines changed
jbmc/regression/jbmc-strings
ConstantEvaluationCompareTo
ConstantEvaluationEndsWith
ConstantEvaluationIsEmpty
4 files changed +55
-57
lines changed Original file line number Diff line number Diff line change 1
1
public class Main {
2
- public void constantCharAt () {
3
- StringBuilder sb = new StringBuilder ("abc" );
4
- char c = sb .charAt (1 );
5
- assert c == 'b' ;
6
- }
2
+ public void constantCharAt () {
3
+ StringBuilder sb = new StringBuilder ("abc" );
4
+ char c = sb .charAt (1 );
5
+ assert c == 'b' ;
6
+ }
7
7
}
Original file line number Diff line number Diff line change 1
1
public class Main {
2
- public void constantCompareToPass () {
3
- String s1 = "ab" ;
4
- String s2 = "abc" ;
5
- assert s1 .compareTo (s2 ) == -1 ;
6
- assert s2 .compareTo (s1 ) == 1 ;
7
- s1 = "abc" ;
8
- s2 = "abc" ;
9
- assert s1 .compareTo (s2 ) == 0 ;
10
- s1 = "abyz" ;
11
- s2 = "adyz" ;
12
- assert s1 .compareTo (s2 ) == -2 ;
13
- }
2
+ public void constantCompareToPass () {
3
+ String s1 = "ab" ;
4
+ String s2 = "abc" ;
5
+ assert s1 .compareTo (s2 ) == -1 ;
6
+ assert s2 .compareTo (s1 ) == 1 ;
7
+ s1 = "abc" ;
8
+ s2 = "abc" ;
9
+ assert s1 .compareTo (s2 ) == 0 ;
10
+ s1 = "abyz" ;
11
+ s2 = "adyz" ;
12
+ assert s1 .compareTo (s2 ) == -2 ;
13
+ }
14
14
15
- public void constantCompareToFail1 () {
16
- String s1 = "ab" ;
17
- String s2 = "abc" ;
18
- assert s1 .compareTo (s2 ) != -1 ;
19
- }
15
+ public void constantCompareToFail1 () {
16
+ String s1 = "ab" ;
17
+ String s2 = "abc" ;
18
+ assert s1 .compareTo (s2 ) != -1 ;
19
+ }
20
20
21
- public void constantCompareToFail2 () {
22
- String s1 = "ab" ;
23
- String s2 = "abc" ;
24
- assert s2 .compareTo (s1 ) != 1 ;
25
- }
21
+ public void constantCompareToFail2 () {
22
+ String s1 = "ab" ;
23
+ String s2 = "abc" ;
24
+ assert s2 .compareTo (s1 ) != 1 ;
25
+ }
26
26
27
- public void constantCompareToFail3 () {
28
- String s1 = "abc" ;
29
- String s2 = "abc" ;
30
- assert s1 .compareTo (s2 ) != 0 ;
31
- }
27
+ public void constantCompareToFail3 () {
28
+ String s1 = "abc" ;
29
+ String s2 = "abc" ;
30
+ assert s1 .compareTo (s2 ) != 0 ;
31
+ }
32
32
33
- public void constantCompareToFail4 () {
34
- String s1 = "abyz" ;
35
- String s2 = "adyz" ;
36
- assert s1 .compareTo (s2 ) != -2 ;
37
- }
38
-
33
+ public void constantCompareToFail4 () {
34
+ String s1 = "abyz" ;
35
+ String s2 = "adyz" ;
36
+ assert s1 .compareTo (s2 ) != -2 ;
37
+ }
39
38
}
Original file line number Diff line number Diff line change 1
1
public class Main {
2
- public void constantEndsWithPass () {
3
- String s1 = "abc" ;
4
- String s2 = "bc" ;
5
- assert s1 .endsWith (s2 );
6
- }
2
+ public void constantEndsWithPass () {
3
+ String s1 = "abc" ;
4
+ String s2 = "bc" ;
5
+ assert s1 .endsWith (s2 );
6
+ }
7
7
8
- public void constantEndsWithFail () {
9
- String s1 = "abc" ;
10
- String s2 = "d" ;
11
- assert s1 .endsWith (s2 );
12
- }
8
+ public void constantEndsWithFail () {
9
+ String s1 = "abc" ;
10
+ String s2 = "d" ;
11
+ assert s1 .endsWith (s2 );
12
+ }
13
13
}
Original file line number Diff line number Diff line change 1
1
public class Main {
2
- public void constantIsEmptyPass () {
3
- String s = "" ;
4
- assert s .isEmpty ();
5
- }
6
-
7
- public void constantIsEmptyFail () {
8
- String s = "abc" ;
9
- assert s .isEmpty ();
10
- }
2
+ public void constantIsEmptyPass () {
3
+ String s = "" ;
4
+ assert s .isEmpty ();
5
+ }
11
6
7
+ public void constantIsEmptyFail () {
8
+ String s = "abc" ;
9
+ assert s .isEmpty ();
10
+ }
12
11
}
You can’t perform that action at this time.
0 commit comments