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

fix: quoteString at EmitC.lean

Browse source 
Fix issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Incorrect.20escaping.20of.20.5Cr.20.3F/near/257061704
This commit is contained in:
Leonardo de Moura 2021-10-11 06:13:46 -07:00
parent 002fb7f446
commit 48a40c4d0a
3 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Compiler/IR/EmitC.lean
View file

@ -475,7 +475,8 @@ def quoteString (s : String) : String :=
let q := s.foldl
(fun q c => q ++
if c == '\n' then "\\n"
else if c == '\n' then "\\t"
else if c == '\r' then "\\r"
else if c == '\t' then "\\t"
else if c == '\\' then "\\\\"
else if c == '\"' then "\\\""
else if c.toNat <= 31 then

3
tests/compiler/escape.lean Normal file
View file

@ -0,0 +1,3 @@
def main : IO Unit := do
IO.eprintln $ "\rfailed at counter-example"
IO.eprintln $ "\tfailed at counter-example"

2
tests/compiler/escape.lean.expected.out Normal file
View file

@ -0,0 +1,2 @@
failed at counter-example
failed at counter-example