From 48a40c4d0a974e7f25565c09feb1536390a73c83 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 11 Oct 2021 06:13:46 -0700 Subject: [PATCH] fix: `quoteString` at `EmitC.lean` Fix issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Incorrect.20escaping.20of.20.5Cr.20.3F/near/257061704 --- src/Lean/Compiler/IR/EmitC.lean | 3 ++- tests/compiler/escape.lean | 3 +++ tests/compiler/escape.lean.expected.out | 2 ++ 3 files changed, 7 insertions(+), 1 deletion(-) create mode 100644 tests/compiler/escape.lean create mode 100644 tests/compiler/escape.lean.expected.out diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean index 796c29e61f..8d8f445256 100644 --- a/src/Lean/Compiler/IR/EmitC.lean +++ b/src/Lean/Compiler/IR/EmitC.lean @@ -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 diff --git a/tests/compiler/escape.lean b/tests/compiler/escape.lean new file mode 100644 index 0000000000..e6d71faa33 --- /dev/null +++ b/tests/compiler/escape.lean @@ -0,0 +1,3 @@ +def main : IO Unit := do + IO.eprintln $ "\rfailed at counter-example" + IO.eprintln $ "\tfailed at counter-example" diff --git a/tests/compiler/escape.lean.expected.out b/tests/compiler/escape.lean.expected.out new file mode 100644 index 0000000000..9c31d16cee --- /dev/null +++ b/tests/compiler/escape.lean.expected.out @@ -0,0 +1,2 @@ + failed at counter-example + failed at counter-example