Project

General

Profile

« Previous | Next » 

Revision 397d5ae3

Added by Pierre-Loïc Garoche about 5 years ago

Copied Printers.pp_expr functions to Horn backend to escape < and > in XML traces output

View differences:

src/backends/Horn/horn_backend_traces.ml
149 149
	(Utils.fprintf_list ~sep:" | " pp_var) init_local_vars
150 150
	(Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) init_local_vars
151 151
	(fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt "")
152
	(Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt "%a" Printers.pp_expr ee)) memories_next;
152
	(Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt "%a" pp_xml_expr ee)) memories_next;
153 153

  
154 154
      fprintf fmt "<localStep name=\"%a\" type=\"%a\">%t%a</localStep>@ "
155 155
	(Utils.fprintf_list ~sep:" | " pp_var) step_local_vars
156 156
	(Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) step_local_vars
157 157
	(fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt "")
158 158
	(Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt "(%a)"
159
          Printers.pp_expr ee)) (memories_old);
159
          pp_xml_expr ee)) (memories_old);
160 160

  
161 161
      let arrow_vars = arrow_vars machines m in
162 162
      let arrow_vars_curr = rename_current_list arrow_vars and

Also available in: Unified diff