michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/parse_tactic_location): validate occurrence index

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-04 14:04:56 -08:00
parent 09818adf90
commit 599de0271b
1 changed files with 10 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/frontends/lean/parse_tactic_location.cpp
View file

@ -22,10 +22,17 @@ static occurrence parse_occurrence(parser & p) {
throw parser_error("invalid tactic location, cannot mix positive and negative occurrences", p.pos()); throw parser_error("invalid tactic location, cannot mix positive and negative occurrences", p.pos());
has_neg = true; has_neg = true;
p.next(); 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 { } else {
auto pos = p.pos(); auto pos = p.pos();
occs.push_back(p.parse_small_nat()); 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) if (has_neg)
throw parser_error("invalid tactic location, cannot mix positive and negative occurrences", pos); throw parser_error("invalid tactic location, cannot mix positive and negative occurrences", pos);
has_pos = true; has_pos = true;