diff -ur frama-c-Phosphorus-20170501.old/src/plugins/gui/gtk_helper.ml frama-c-Phosphorus-20170501/src/plugins/gui/gtk_helper.ml
--- frama-c-Phosphorus-20170501.old/src/plugins/gui/gtk_helper.ml	2017-06-01 09:02:15.000000000 +0100
+++ frama-c-Phosphorus-20170501/src/plugins/gui/gtk_helper.ml	2017-11-18 11:08:13.554409903 +0000
@@ -317,11 +317,7 @@
             begin fun cond ->
               try if List.mem `IN cond then begin
                   (* On Windows, you must use Io.read *)
-                  (* buf' is added only to work around the suspicious type of
-                     Glib.Io.read *)
-                  let buf' = Bytes.to_string buf in
-                  let len = Glib.Io.read channel ~buf:buf' ~pos:0 ~len in
-                  let buf = Bytes.of_string buf' in
+                  let len = Glib.Io.read channel ~buf ~pos:0 ~len in
                   len >= 1 &&
                   (let full_string = !current_partial ^ Bytes.sub_string buf 0 len in
                    let to_emit, c = splitting_for_utf8 full_string in
diff -ur frama-c-Phosphorus-20170501.old/src/plugins/wp/qed/src/export_why3.ml frama-c-Phosphorus-20170501/src/plugins/wp/qed/src/export_why3.ml
--- frama-c-Phosphorus-20170501.old/src/plugins/wp/qed/src/export_why3.ml	2017-06-01 09:02:17.000000000 +0100
+++ frama-c-Phosphorus-20170501/src/plugins/wp/qed/src/export_why3.ml	2017-11-18 11:05:18.667545678 +0000
@@ -60,11 +60,11 @@
       method! basename s =
         (** TODO: better uncapitalization of the first letter? utf8? *)
         let lower0 = Char.lowercase s.[0] in
-        if String.length s > 0 &&  lower0 <> s.[0] then
-          let s = String.copy s in
-          s.[0] <- lower0;
-          s
-        else s
+        if String.length s > 0 &&  lower0 <> s.[0] then (
+          let s = Bytes.of_string s in
+          Bytes.set s 0 lower0;
+          Bytes.to_string s
+        ) else s
 
       (* -------------------------------------------------------------------------- *)
       (* --- Types                                                              --- *)
diff -ur frama-c-Phosphorus-20170501.old/src/plugins/wp/qed/src/numbers.mll frama-c-Phosphorus-20170501/src/plugins/wp/qed/src/numbers.mll
--- frama-c-Phosphorus-20170501.old/src/plugins/wp/qed/src/numbers.mll	2017-06-01 09:02:10.000000000 +0100
+++ frama-c-Phosphorus-20170501/src/plugins/wp/qed/src/numbers.mll	2017-11-18 11:04:26.777566914 +0000
@@ -128,8 +128,8 @@
       | 'a' .. 'f' -> int_of_char 'a' - 10
       | 'A' .. 'F' -> int_of_char 'A' - 10
       | _ ->
-	  let e = "?" in e.[0] <- c ;
-	  error "Incorrect hex-digit" e
+	  let e = Bytes.of_string "?" in Bytes.set e 0 c;
+	  error "Incorrect hex-digit" (Bytes.to_string e)
     in int_of_char c - d
 
   open Big_int
@@ -164,8 +164,9 @@
 
   let power_of_ten e =
     if e < 0 then raise (Invalid_argument "negative power") ;
-    let s = String.make (succ e) '0' in
-    s.[0] <- '1' ; s
+    let s = Bytes.make (succ e) '0' in
+    Bytes.set s 0 '1';
+    Bytes.to_string s
 
   let significant cst =
     let digits = cst.man ^ cst.com in