From 0297bb18f7d524eca548e6cacb40a4f2433e91cc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 15 May 2019 15:03:33 +0200
Subject: [PATCH] [wp] fix expl string for why3 output
---
src/plugins/wp/ProverWhy3.ml | 11 +++++++++--
1 file changed, 9 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 38e73ded32b..61230201355 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -323,6 +323,13 @@ end
(* --- Assembling Goal --- *)
(* -------------------------------------------------------------------------- *)
+let sanitize_expl fmt title =
+ for i = 0 to String.length title - 1 do
+ match title.[i] with
+ | '\n' | '\t' -> Format.pp_print_char fmt ' '
+ | c -> Format.pp_print_char fmt c
+ done
+
let assemble_goal ~id ~title ~theory ?axioms prop fmt =
(** Also create the directory *)
let goal = cluster ~id ~title () in
@@ -348,9 +355,9 @@ let assemble_goal ~id ~title ~theory ?axioms prop fmt =
engine#set_goal true ;
engine#global
begin fun () ->
- v#printf "@[<hv 2>goal %s[@expl:%s]:@ %a@]@\n@\n"
+ v#printf "@[<hv 2>goal %s[@expl:%a]:@ %a@]@\n@\n"
why3_goal_name
- title
+ sanitize_expl title
engine#pp_prop (F.e_prop prop) ;
end ;
engine#set_goal false ;
--
GitLab