Skip to content

Commit dd5a674

Browse files
author
Joel Allred
committed
Add jbmc string primitives to CProverString
Allows to compile and run jbmc tests.
1 parent 8f6431c commit dd5a674

File tree

2 files changed

+121
-0
lines changed

2 files changed

+121
-0
lines changed
Binary file not shown.

regression/strings-smoke-tests/cprover/CProverString.java

Lines changed: 121 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,29 @@ public static char charAt(String s, int i) {
88
return '\u0000';
99
}
1010

11+
public static int codePointAt(String s, int index) {
12+
return s.codePointAt(index);
13+
}
14+
15+
public static int codePointBefore(String s, int index) {
16+
return s.codePointBefore(index);
17+
}
18+
19+
public static int codePointCount(
20+
String s, int beginIndex, int endIndex) {
21+
return s.codePointCount(beginIndex, endIndex);
22+
}
23+
24+
public static int offsetByCodePoints(
25+
String s, int index, int codePointOffset) {
26+
return s.offsetByCodePoints(index, codePointOffset);
27+
}
28+
29+
public static CharSequence subSequence(
30+
String s, int beginIndex, int endIndex) {
31+
return s.subSequence(beginIndex, endIndex);
32+
}
33+
1134
public static String substring(String s, int i) {
1235
if (i <= 0)
1336
return s;
@@ -26,4 +49,102 @@ public static String substring(String s, int i, int j) {
2649
return "";
2750
return s.substring(i, j);
2851
}
52+
53+
public static StringBuilder append(
54+
StringBuilder sb, CharSequence cs, int i, int j) {
55+
return sb.append(cs, i, j);
56+
}
57+
58+
public static StringBuilder delete(StringBuilder sb, int start, int end) {
59+
return sb.delete(start, end);
60+
}
61+
62+
public static StringBuilder deleteCharAt(StringBuilder sb, int index) {
63+
return sb.deleteCharAt(index);
64+
}
65+
66+
public static StringBuilder insert(
67+
StringBuilder sb, int offset, String str) {
68+
return sb.insert(offset, str);
69+
}
70+
71+
public static StringBuilder insert(
72+
StringBuilder sb, int offset, boolean b) {
73+
return sb.insert(offset, b);
74+
}
75+
76+
public static StringBuilder insert(
77+
StringBuilder sb, int offset, char c) {
78+
return sb.insert(offset, c);
79+
}
80+
81+
public static StringBuilder insert(
82+
StringBuilder sb, int offset, int i) {
83+
return sb.insert(offset, i);
84+
}
85+
86+
public static StringBuilder insert(
87+
StringBuilder sb, int offset, long l) {
88+
return sb.insert(offset, l);
89+
}
90+
91+
public static StringBuilder insert(
92+
StringBuilder sb, int offset, float f) {
93+
return sb.insert(offset, f);
94+
}
95+
96+
public static StringBuilder insert(
97+
StringBuilder sb, int offset, double d) {
98+
return sb.insert(offset, d);
99+
}
100+
101+
public static void setLength(StringBuffer sb, int newLength) {
102+
sb.setLength(newLength);
103+
}
104+
105+
public static char charAt(StringBuffer sb, int index) {
106+
return sb.charAt(index);
107+
}
108+
109+
public static void setCharAt(StringBuffer sb, int index, char c) {
110+
sb.setCharAt(index, c);
111+
}
112+
113+
public static StringBuffer delete(
114+
StringBuffer sb, int start, int end) {
115+
return sb.delete(start, end);
116+
}
117+
118+
public static StringBuffer deleteCharAt(StringBuffer sb, int index) {
119+
return sb.deleteCharAt(index);
120+
}
121+
122+
public static String substring(StringBuffer sb, int start, int end) {
123+
return sb.substring(start, end);
124+
}
125+
126+
public static StringBuffer insert(
127+
StringBuffer sb, int offset, String str) {
128+
return sb.insert(offset, str);
129+
}
130+
131+
public static StringBuffer insert(
132+
StringBuffer sb, int offset, boolean b) {
133+
return sb.insert(offset, b);
134+
}
135+
136+
public static StringBuffer insert(
137+
StringBuffer sb, int offset, char c) {
138+
return sb.insert(offset, c);
139+
}
140+
141+
public static StringBuffer insert(
142+
StringBuffer sb, int offset, int i) {
143+
return sb.insert(offset, i);
144+
}
145+
146+
public static StringBuffer insert(
147+
StringBuffer sb, int offset, long l) {
148+
return sb.insert(offset, l);
149+
}
29150
}

0 commit comments

Comments
 (0)