Prevent overflow with argument of lastIndexOf

smowton · Dec 8, 2017 · 985684a · 985684a
1 parent 04766b2
commit 985684a
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -348,7 +348,8 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
   axioms.push_back(a3);
 
   const exprt index1 = from_integer(1, index_type);
-  const plus_exprt from_index_plus_one(from_index, index1);
+  const exprt from_index_plus_one =
+    plus_exprt_with_overflow_check(from_index, index1);
   const if_exprt end_index(
     binary_relation_exprt(from_index_plus_one, ID_le, str.length()),
     from_index_plus_one,