From: Mehdi Dogguy <mehdi@debian.org>
Date: Fri, 11 Aug 2017 12:29:34 -0400
Subject: More fixes of spelling errors

---
 src/plugins/scope/dpds_gui.ml   | 2 +-
 src/plugins/wp/GuiProver.ml     | 2 +-
 src/plugins/wp/Strategy.ml      | 2 +-
 src/plugins/wp/Tactical.ml      | 4 ++--
 src/plugins/wp/wp_parameters.ml | 4 ++--
 5 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/plugins/scope/dpds_gui.ml b/src/plugins/scope/dpds_gui.ml
index c7b2a01..82cb868 100644
--- a/src/plugins/scope/dpds_gui.ml
+++ b/src/plugins/scope/dpds_gui.ml
@@ -379,7 +379,7 @@ let help (main_ui:Design.main_window_extension_points) =
        ^"and the data is the one that is selected if any, "
        ^"or it can be given via a popup.\n"
        ^"\tIf the text given in the popup is empty, or 'Cancel' is chosen, "
-       ^"the selection of the command is reseted.");
+       ^"the selection of the command is reset.");
     add (ShowDef.help);
     add (Zones.help);
     add (DataScope.help);
diff --git a/src/plugins/wp/GuiProver.ml b/src/plugins/wp/GuiProver.ml
index 6706138..3804a1e 100644
--- a/src/plugins/wp/GuiProver.ml
+++ b/src/plugins/wp/GuiProver.ml
@@ -165,7 +165,7 @@ class prover ~(console:Wtext.text) ~prover =
           Pretty_utils.ksfprintf self#set_label "%a" VCS.pp_prover prover ;
       | VCS.Computing signal ->
           self#set_status `EXECUTE ;
-          self#set_action ~tooltip:"Interrrupt Prover" ~icon:`STOP ~callback:signal () ;
+          self#set_action ~tooltip:"Interrupt Prover" ~icon:`STOP ~callback:signal () ;
           Pretty_utils.ksfprintf self#set_label "%a (...)" VCS.pp_prover prover ;
       | VCS.Valid | VCS.Checked ->
           self#set_status ok_status ;
diff --git a/src/plugins/wp/Strategy.ml b/src/plugins/wp/Strategy.ml
index 008b61c..d4a0188 100644
--- a/src/plugins/wp/Strategy.ml
+++ b/src/plugins/wp/Strategy.ml
@@ -131,7 +131,7 @@ let registry = ref Tmap.empty
 let register s =
   let id = s#id in
   if Tmap.mem id !registry then
-    Wp_parameters.error "Strategy #%s already registered (skiped)" id
+    Wp_parameters.error "Strategy #%s already registered (skipped)" id
   else
     registry := Tmap.add id (s :> heuristic) !registry
 
diff --git a/src/plugins/wp/Tactical.ml b/src/plugins/wp/Tactical.ml
index 1afdf92..273f82c 100644
--- a/src/plugins/wp/Tactical.ml
+++ b/src/plugins/wp/Tactical.ml
@@ -53,7 +53,7 @@ let rec insert_group cc = function
 let add_composer (c : #composer) =
   let id = c#id in
   if Tmap.mem id !composers then
-    Wp_parameters.error "Composer #%s already registered (skiped)" id
+    Wp_parameters.error "Composer #%s already registered (skipped)" id
   else
     begin
       composers := Tmap.add id (c :> composer) !composers ;
@@ -404,7 +404,7 @@ let tacticals = ref Tmap.empty
 let register t =
   let id = t#id in
     if Tmap.mem id !tacticals then
-      Wp_parameters.error "Tactical #%s already registered (skiped)" id
+      Wp_parameters.error "Tactical #%s already registered (skipped)" id
     else
       tacticals := Tmap.add id (t :> t) !tacticals
 
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 1fb99f9..82a4998 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -276,7 +276,7 @@ module SplitDepth =
     let option_name = "-wp-split-depth"
     let default = 0
     let arg_name = "p"
-    let help = "Set depth of exploration for spliting conjunctions into sub-goals.\n\
+    let help = "Set depth of exploration for splitting conjunctions into sub-goals.\n\
 Value `-1` means an unlimited depth."
   end)
 
@@ -681,7 +681,7 @@ module TruncPropIdFileName =
     let option_name = "-wp-filename-truncation"
     let default = 60
     let arg_name = "n"
-    let help = "Truncate basename of proof obligation files after <n> characters. Since numbers can be added as suffixes to make theses names unique, filename lengths can be highter to <n>. No truncation is performed when the value equals to zero (defaut: 60)."
+    let help = "Truncate basename of proof obligation files after <n> characters. Since numbers can be added as suffixes to make theses names unique, filename lengths can be highter to <n>. No truncation is performed when the value equals to zero (default: 60)."
   end)
 
 

From: Mehdi Dogguy <mehdi@debian.org>
Date: Thu, 21 Jan 2016 23:48:35 +0100
Subject: Fix spelling-error-in-binary

---
 man/frama-c.1                              | 4 ++--
 src/kernel_services/ast_data/cil_types.mli | 2 +-
 src/plugins/e-acsl/typing.ml               | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/man/frama-c.1 b/man/frama-c.1
index fac74bc..5801d7b 100644
--- a/man/frama-c.1
+++ b/man/frama-c.1
@@ -404,14 +404,14 @@ alias of
 .TP
 .B -print-plugin-path
 outputs the directory where Frama-C searches its plugins
-(can be overidden by the
+(can be overridden by the
 .B FRAMAC_PLUGIN
 variable and the
 .B -add-path
 option)
 .TP
 .B -print-share-path
-outputs the directory where Frama-C stores its data (can be overidden by the
+outputs the directory where Frama-C stores its data (can be overridden by the
 .B FRAMAC_SHARE
 variable)
 .TP
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index c23460a..1c78913 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -543,7 +543,7 @@ and varinfo = {
   (**
      - For global variables, true iff the variable or function
        is defined in the file.
-     - For local variables, true iff the variable is explicitely initialized
+     - For local variables, true iff the variable is explicitly initialized
        at declaration time.
      - Unused for formals variables and logic variables.
   *)
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 9f9130f..7d7fb03 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -203,7 +203,7 @@ let coerce ~arith_operand ~ctx ~op ty =
   end else
     (* only add an explicit cast if the context is [Gmp] and [ty] is not;
        or if the term corresponding to [ty] is an operand of an arithmetic
-       operation which must be explicitely coerced in order to force the
+       operation which must be explicitly coerced in order to force the
        operation to be of the expected type. *)
     if (ctx = Gmp && ty <> Gmp) || arith_operand
     then { ty; op; cast = Some ctx }
@@ -329,7 +329,7 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
         with Interval.Not_an_integer ->
           dup Other (* real *)
       in
-      (* it is enough to explicitely coerce when required one operand to [ctx]
+      (* it is enough to explicitly coerce when required one operand to [ctx]
          (through [arith_operand]) in order to force the type of the operation.
          Heuristic: coerce the operand which is not a lval in order to lower
          the number of explicit casts *)