diff options
| author | Robert Norton | 2018-11-21 12:31:07 +0000 |
|---|---|---|
| committer | Robert Norton | 2018-11-21 12:31:07 +0000 |
| commit | 05c68ff053485e9d5089969303e73045fb6cab6c (patch) | |
| tree | efff1a12e3aec8f5660ce42b8377d853914db9ec /src | |
| parent | f4affce812cdc1762ac2617682f813f1f34ab6b4 (diff) | |
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.
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 6 |
1 files changed, 5 insertions, 1 deletions
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). |