Skip to content

Commit

Permalink
Fix invariant: value must be strictly positive
Browse files Browse the repository at this point in the history
A value of zero would result in an invalid memory access later on.
  • Loading branch information
tautschnig committed Jun 23, 2018
1 parent b8743fa commit 497d296
Showing 1 changed file with 1 addition and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -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");
Expand Down

0 comments on commit 497d296

Please sign in to comment.