From 05c68ff053485e9d5089969303e73045fb6cab6c Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Wed, 21 Nov 2018 12:31:07 +0000
Subject: Escape string literals in coq backend. Note that
 71020c2f460e6031776df17cf8f2f71df5bb9730 introduced assert error messages
 containing " revealing unescaped string literals in generated lem and
 prompting review of other backends.

---
 src/pretty_print_coq.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 2e62188d..163cd183 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -556,6 +556,10 @@ let doc_tannot ctxt env eff typ =
     else string " : " ^^ ta
   in of_typ typ
 
+(* Only double-quotes need escaped - by doubling them. *)
+let coq_escape_string s =
+  Str.global_replace (Str.regexp "\"") "\"\"" s
+   
 let doc_lit (L_aux(lit,l)) =
   match lit with
   | L_unit  -> utf8string "tt"
@@ -570,7 +574,7 @@ let doc_lit (L_aux(lit,l)) =
   | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*)
   | L_undef ->
      utf8string "(Fail \"undefined value of unsupported type\")"
-  | L_string s -> utf8string ("\"" ^ s ^ "\"")
+  | L_string s -> utf8string ("\"" ^ (coq_escape_string s) ^ "\"")
   | L_real s ->
     (* Lem does not support decimal syntax, so we translate a string
        of the form "x.y" into the ratio (x * 10^len(y) + y) / 10^len(y).
-- 
cgit v1.2.3