max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: non termination on ill-formed string literals

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-20 17:04:39 -07:00
parent 03a361edf4
commit 241eabfc41
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/LeanInit.lean
View file

@ -670,7 +670,7 @@ match stx.isNatLit? with
| some val => val
| none => 0
private def decodeQuotedChar (s : String) (i : String.Pos) : Option (Char × String.Pos) :=
def decodeQuotedChar (s : String) (i : String.Pos) : Option (Char × String.Pos) :=
let c := s.get i;
let i := s.next i;
if c == '\\' then pure ('\\', i)
@ -698,6 +698,8 @@ partial def decodeStrLitAux (s : String) : String.Pos → String → Option Stri
let i := s.next i;
if c == '\"' then
pure acc
else if s.atEnd i then
none
else if c == '\\' then do
(c, i) ← decodeQuotedChar s i;
decodeStrLitAux i (acc.push c)