Skip to content

Commit 666bec0

Browse files
Removing comments about lastIndexOf being imprecise
The previous commits now make these functions precise.
1 parent bc3eedc commit 666bec0

File tree

1 file changed

+0
-7
lines changed

1 file changed

+0
-7
lines changed

src/solvers/refinement/string_constraint_generator.h

-7
Original file line numberDiff line numberDiff line change
@@ -194,21 +194,15 @@ class string_constraint_generatort
194194
const exprt &from_index);
195195

196196
// Add axioms corresponding to the String.indexOf:(String;I) java function
197-
// TODO: the specifications are only partial:
198-
// we add axioms stating that the returned value is either -1 or greater than
199-
// from_index and the string beggining there has prefix substring
200197
exprt add_axioms_for_index_of_string(
201198
const string_exprt &haystack,
202199
const string_exprt &needle,
203200
const exprt &from_index);
204201

205202
// Add axioms corresponding to the String.indexOf java functions
206-
// TODO: the specifications are only partial for the ones that look for
207-
// strings
208203
exprt add_axioms_for_index_of(const function_application_exprt &f);
209204

210205
// Add axioms corresponding to the String.lastIndexOf:(String;I) java function
211-
// TODO: the specifications are only partial
212206
exprt add_axioms_for_last_index_of_string(
213207
const string_exprt &str,
214208
const string_exprt &substring,
@@ -221,7 +215,6 @@ class string_constraint_generatort
221215
const exprt &from_index);
222216

223217
// Add axioms corresponding to the String.lastIndexOf java functions
224-
// TODO: the specifications is only partial
225218
exprt add_axioms_for_last_index_of(const function_application_exprt &f);
226219

227220
// TODO: the specifications of these functions is only partial

0 commit comments

Comments
 (0)