From 241eabfc41f2b25206a0d6404684230d57dae014 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 20 Sep 2020 17:04:39 -0700 Subject: [PATCH] fix: non termination on ill-formed string literals --- src/Init/LeanInit.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean index 769e70a60f..58a06f5e62 100644 --- a/src/Init/LeanInit.lean +++ b/src/Init/LeanInit.lean @@ -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)