aboutsummaryrefslogtreecommitdiffstats
path: root/backend/AisAnnot.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2018-03-08 17:52:31 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2018-03-08 17:52:31 +0100
commit5063ae307001dcddbfcc60e7abda04cf98bffeb4 (patch)
treee1c22e88075976f6daf0723908534c8c9ceb1756 /backend/AisAnnot.ml
parentbf21c2c43629ca47a2a34c47a01c4525a69a2ca6 (diff)
downloadcompcert-kvx-5063ae307001dcddbfcc60e7abda04cf98bffeb4.tar.gz
compcert-kvx-5063ae307001dcddbfcc60e7abda04cf98bffeb4.zip
Perform quoting for json.
The strings for json need quoting of special characters such as \" and \\. Bug 22438
Diffstat (limited to 'backend/AisAnnot.ml')
-rw-r--r--backend/AisAnnot.ml9
1 files changed, 8 insertions, 1 deletions
diff --git a/backend/AisAnnot.ml b/backend/AisAnnot.ml
index 5983f417..27005561 100644
--- a/backend/AisAnnot.ml
+++ b/backend/AisAnnot.ml
@@ -163,7 +163,14 @@ let json_ais_annot preg_string sp_reg_name txt args =
let txt = ais_annot_txt false 0 preg_string sp_reg_name txt args in
let t_to_json = function
| Label _ -> String "%here"
- | s -> s in
+ | String s -> let buf = Buffer.create (String.length s) in
+ String.iter (fun c ->
+ begin match c with
+ | '\\' | '"' -> Buffer.add_char buf '\\'
+ | _ -> () end;
+ Buffer.add_char buf c) s;
+ String (Buffer.contents buf)
+ | Symbol s -> Symbol s in
(List.map t_to_json txt)
let validate_ais_annot env loc txt args =