From 599de0271b0a03b60eb9252314fd15fea484e66b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Feb 2015 14:04:56 -0800 Subject: [PATCH] feat(frontends/lean/parse_tactic_location): validate occurrence index --- src/frontends/lean/parse_tactic_location.cpp | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/src/frontends/lean/parse_tactic_location.cpp b/src/frontends/lean/parse_tactic_location.cpp index 285d33b214..af68b8775d 100644 --- a/src/frontends/lean/parse_tactic_location.cpp +++ b/src/frontends/lean/parse_tactic_location.cpp @@ -22,10 +22,17 @@ static occurrence parse_occurrence(parser & p) { throw parser_error("invalid tactic location, cannot mix positive and negative occurrences", p.pos()); has_neg = true; p.next(); - occs.push_back(p.parse_small_nat()); + auto pos = p.pos(); + unsigned i = p.parse_small_nat(); + if (i == 0) + throw parser_error("invalid tactic location, first occurrence is 1", pos); + occs.push_back(i); } else { - auto pos = p.pos(); - occs.push_back(p.parse_small_nat()); + auto pos = p.pos(); + unsigned i = p.parse_small_nat(); + if (i == 0) + throw parser_error("invalid tactic location, first occurrence is 1", pos); + occs.push_back(i); if (has_neg) throw parser_error("invalid tactic location, cannot mix positive and negative occurrences", pos); has_pos = true;