Fix invariant: value must be strictly positive

tautschnig · tautschnig · commit 497d2960a0df · 2018-06-23T19:22:48.000+01:00
A value of zero would result in an invalid memory access later on.
diff --git a/src/solvers/refinement/string_constraint_generator_format.cpp b/src/solvers/refinement/string_constraint_generator_format.cpp
@@ -374,7 +374,7 @@ exprt string_constraint_generatort::add_axioms_for_format(
         }
         else
         {
-          INVARIANT(fs.index>=0, "index in format should be positive");
+          INVARIANT(fs.index > 0, "index in format should be positive");
           INVARIANT(
             static_cast<std::size_t>(fs.index)<=args.size(),
             "number of format must match specifiers");

Original file line number	Diff line number	Diff line change
`@@ -374,7 +374,7 @@ exprt string_constraint_generatort::add_axioms_for_format(`
`374`	`374`	`}`
`375`	`375`	`else`
`376`	`376`	`{`
`377`		`- INVARIANT(fs.index>=0, "index in format should be positive");`
	`377`	`+ INVARIANT(fs.index > 0, "index in format should be positive");`
`378`	`378`	`INVARIANT(`
`379`	`379`	`static_cast<std::size_t>(fs.index)<=args.size(),`
`380`	`380`	`"number of format must match specifiers");`