2021-03-01 05:39 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002323Frama-CDocumentationpublic2017-09-01 10:08
Reportermehdi 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C 15-Phosphorus 
Target VersionFixed in VersionFrama-C GIT, precise the release id 
Summary0002323: Spelling errors
DescriptionHi,

I've found some spelling errors in Frama-C's source code. Please find attached a patch to fixe them.
TagsNo tags attached.
Attached Files
  • patch file icon 0008-More-fixes-of-spelling-errors.patch (4,293 bytes) 2017-08-11 18:35 -
    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)
     
     
    
    patch file icon 0008-More-fixes-of-spelling-errors.patch (4,293 bytes) 2017-08-11 18:35 +
  • patch file icon 0001-Fix-spelling-error-in-binary.patch (2,708 bytes) 2017-08-11 18:49 -
    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 *)
    
    patch file icon 0001-Fix-spelling-error-in-binary.patch (2,708 bytes) 2017-08-11 18:49 +

-Relationships
+Relationships

-Notes

~0006436

mehdi (reporter)

I had another patch with other spelling errors. I am attaching it here.

~0006454

virgile (developer)

Thanks for the patches. They have been incorporated in our development repository and on our github snapshot in commit https://github.com/Frama-C/Frama-C-snapshot/commit/30b819710d7630dfaa9f1b434585c62265520d11
+Notes

-Issue History
Date Modified Username Field Change
2017-08-11 18:35 mehdi New Issue
2017-08-11 18:35 mehdi File Added: 0008-More-fixes-of-spelling-errors.patch
2017-08-11 18:49 mehdi Note Added: 0006436
2017-08-11 18:49 mehdi File Added: 0001-Fix-spelling-error-in-binary.patch
2017-09-01 09:46 virgile Note Added: 0006454
2017-09-01 09:46 virgile Status new => resolved
2017-09-01 09:46 virgile Fixed in Version => Frama-C GIT, precise the release id
2017-09-01 09:46 virgile Resolution open => fixed
2017-09-01 09:46 virgile Assigned To => virgile
2017-09-01 10:08 yakobowski Status resolved => closed
+Issue History