From: Mehdi Dogguy Date: Thu, 21 Jan 2016 23:48:35 +0100 Subject: Fix spelling-error-in-binary --- man/frama-c.1 | 4 ++-- src/kernel_internals/typing/asm_contracts.ml | 2 +- src/kernel_services/abstract_interp/lmap_sig.mli | 2 +- src/kernel_services/analysis/exn_flow.ml | 2 +- src/kernel_services/analysis/logic_interp.ml | 14 +++++++------- src/kernel_services/ast_queries/file.ml | 2 +- src/kernel_services/ast_queries/logic_const.mli | 2 +- src/kernel_services/ast_queries/logic_env.ml | 4 ++-- src/kernel_services/ast_queries/logic_typing.ml | 2 +- src/kernel_services/plugin_entry_points/kernel.ml | 2 +- src/libraries/utils/bitvector.ml | 2 +- src/plugins/aorai/aorai_utils.ml | 2 +- src/plugins/occurrence/register.ml | 2 +- src/plugins/scope/dpds_gui.ml | 2 +- .../security_slicing/security_slicing_parameters.ml | 2 +- src/plugins/slicing/fct_slice.ml | 4 ++-- src/plugins/value/gui_files/register_gui.ml | 2 +- src/plugins/value/value_parameters.ml | 2 +- src/plugins/value_types/cvalue.ml | 2 +- src/plugins/wp/VC.mli | 2 +- src/plugins/wp/qed/src/logic.mli | 2 +- src/plugins/wp/wpAnnot.ml | 2 +- src/plugins/wp/wp_parameters.ml | 2 +- 23 files changed, 32 insertions(+), 32 deletions(-) diff --git a/man/frama-c.1 b/man/frama-c.1 index 67f47d2..9eccab8 100644 --- a/man/frama-c.1 +++ b/man/frama-c.1 @@ -389,14 +389,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_internals/typing/asm_contracts.ml b/src/kernel_internals/typing/asm_contracts.ml index 3496d74..c30fa22 100644 --- a/src/kernel_internals/typing/asm_contracts.ml +++ b/src/kernel_internals/typing/asm_contracts.ml @@ -91,7 +91,7 @@ object(self) (* the only interesting information for clobbers is the presence of the "memory" keyword, which indicates that memory may have been accessed (read or write) outside of - the locations explicitely referred to as output or + the locations explicitly referred to as output or input. We can't do much more than emitting a warning and considering that nothing is touched beyond normally specified outputs and inputs. *) diff --git a/src/kernel_services/abstract_interp/lmap_sig.mli b/src/kernel_services/abstract_interp/lmap_sig.mli index 5e5aff3..ce2d244 100644 --- a/src/kernel_services/abstract_interp/lmap_sig.mli +++ b/src/kernel_services/abstract_interp/lmap_sig.mli @@ -103,7 +103,7 @@ val find_base : Base.t -> t -> offsetmap Bottom.Top.or_top_bottom val find_base_or_default : Base.t -> t -> offsetmap Bottom.Top.or_top_bottom (** Same as [find_base], but return the default values for bases that are not currently present in the map. Prefer the use of this function - to [find_base], unless you explicitely want to see if the base is bound. *) + to [find_base], unless you explicitly want to see if the base is bound. *) (** {2 Binding variables} *) diff --git a/src/kernel_services/analysis/exn_flow.ml b/src/kernel_services/analysis/exn_flow.ml index 7f10d0a..a32c483 100644 --- a/src/kernel_services/analysis/exn_flow.ml +++ b/src/kernel_services/analysis/exn_flow.ml @@ -638,7 +638,7 @@ object(self) method private guard_post_cond (kind,pred as orig) = match kind with - (* If we exit explicitely with exit, + (* If we exit explicitly with exit, we haven't seen an uncaught exception anyway. *) | Exits | Breaks | Continues -> orig | Returns | Normal -> diff --git a/src/kernel_services/analysis/logic_interp.ml b/src/kernel_services/analysis/logic_interp.ml index ec565ce..fff7627 100644 --- a/src/kernel_services/analysis/logic_interp.ml +++ b/src/kernel_services/analysis/logic_interp.ml @@ -635,7 +635,7 @@ struct match ki_opt,before_opt with (* function contract *) | None,Some true -> - failwith "The use of the label Old is forbiden inside clauses \ + failwith "The use of the label Old is forbidden inside clauses \ related the pre-state of function contracts." | None,None | None,Some false -> @@ -643,7 +643,7 @@ struct self#change_label AbsLabel_pre x (* statement contract *) | Some (_ki,false),Some true -> - failwith "The use of the label Old is forbiden inside clauses \ + failwith "The use of the label Old is forbidden inside clauses \ related the pre-state of statement contracts." | Some (ki,false),None | Some (ki,false),Some false -> @@ -662,20 +662,20 @@ related the pre-state of statement contracts." (* function contract *) | None,Some _ -> failwith "Function contract where the use of the label Post is \ - forbiden." + forbidden." | None,None -> (* refers to the post-state of the contract. *) self#change_label AbsLabel_post x (* statement contract *) | Some (_ki,false),Some _ -> failwith "Statement contract where the use of the label Post is \ -forbiden." +forbidden." | Some (_ki,false),None -> (* refers to the pre-state of the contract. *) self#change_label AbsLabel_post x (* code annotation *) | Some (_ki,true), _ -> - failwith "The use of the label Post is forbiden inside code \ + failwith "The use of the label Post is forbidden inside code \ annotations." method private change_label_to_pre: 'a.'a -> 'a visitAction = @@ -683,7 +683,7 @@ annotations." match ki_opt with (* function contract *) | None -> - failwith "The use of the label Pre is forbiden inside function \ + failwith "The use of the label Pre is forbidden inside function \ contracts." (* statement contract *) (* code annotation *) @@ -696,7 +696,7 @@ contracts." match ki_opt with (* function contract *) | None -> - failwith "the use of C labels is forbiden inside clauses related \ + failwith "the use of C labels is forbidden inside clauses related \ function contracts." (* statement contract *) (* code annotation *) diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml index af53fad..e5a3a7c 100644 --- a/src/kernel_services/ast_queries/file.ml +++ b/src/kernel_services/ast_queries/file.ml @@ -413,7 +413,7 @@ let parse_cabs = function "your preprocessor is not known to handle option `%s'. \ If pre-processing fails because of it, please add \ -no-cpp-gnu-like option to Frama-C's command-line. \ - If you do not want to see this warning again, use explicitely \ + If you do not want to see this warning again, use explicitly \ -cpp-gnu-like option." opt; opt diff --git a/src/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli index 72d8f3e..64604fd 100644 --- a/src/kernel_services/ast_queries/logic_const.mli +++ b/src/kernel_services/ast_queries/logic_const.mli @@ -22,7 +22,7 @@ (* *) (**************************************************************************) -(** Smart contructors for logic annotations. +(** Smart constructors for logic annotations. @plugin development guide *) open Cil_types diff --git a/src/kernel_services/ast_queries/logic_env.ml b/src/kernel_services/ast_queries/logic_env.ml index 6475cf4..8750429 100644 --- a/src/kernel_services/ast_queries/logic_env.ml +++ b/src/kernel_services/ast_queries/logic_env.ml @@ -92,7 +92,7 @@ module Logic_ctor_builtin = (Datatype.String.Hashtbl) (Cil_datatype.Logic_ctor_info) (struct - let name = "built-in logic contructors table" + let name = "built-in logic constructors table" let dependencies = [] let size = 17 end) @@ -102,7 +102,7 @@ module Logic_ctor_info = (Datatype.String.Hashtbl) (Cil_datatype.Logic_ctor_info) (struct - let name = "logic contructors table" + let name = "logic constructors table" let dependencies = [ Logic_ctor_builtin.self ] let size = 17 end) diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml index 9694a9f..e20b73c 100644 --- a/src/kernel_services/ast_queries/logic_typing.ml +++ b/src/kernel_services/ast_queries/logic_typing.ml @@ -2090,7 +2090,7 @@ let add_label info lab = res | _ -> ind (* We do not have a context allowing to update the predicate. - Implies that any recursive call is already explicitely guarded + Implies that any recursive call is already explicitly guarded *) method! vlogic_info_decl info = diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml index 0112fac..83d7dd6 100644 --- a/src/kernel_services/plugin_entry_points/kernel.ml +++ b/src/kernel_services/plugin_entry_points/kernel.ml @@ -1068,7 +1068,7 @@ module UnspecifiedAccess = False(struct let module_name = "UnspecifiedAccess" let option_name = "-unspecified-access" - let help = "do not assume that read/write accesses occuring \ + let help = "do not assume that read/write accesses occurring \ between sequence points are separated" end) diff --git a/src/libraries/utils/bitvector.ml b/src/libraries/utils/bitvector.ml index b2d786b..3ebf43d 100644 --- a/src/libraries/utils/bitvector.ml +++ b/src/libraries/utils/bitvector.ml @@ -34,7 +34,7 @@ bitvector, which has to be provided in some informations (such as concat). We rely on the invariant that the extra bits are set to 0 (this is important e.g. for equality testing). An alternative - design could have been not to explicitely ignore these extra bits + design could have been not to explicitly ignore these extra bits in operations that are sensitive to them, but this seems more error-prone. *) diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml index b9df7f2..778f9cc 100644 --- a/src/plugins/aorai/aorai_utils.ml +++ b/src/plugins/aorai/aorai_utils.ml @@ -736,7 +736,7 @@ let is_out_of_state_pred state = (* In the deterministic case, we only assign the unique state variable to a specific enumerated constant. Non-determistic automata on the other - hand, need to have the corresponding state variable explicitely set to 0. *) + hand, need to have the corresponding state variable explicitly set to 0. *) let is_out_of_state_stmt (_,copy) loc = if Aorai_option.Deterministic.get () then diff --git a/src/plugins/occurrence/register.ml b/src/plugins/occurrence/register.ml index 9318acb..51ca7df 100644 --- a/src/plugins/occurrence/register.ml +++ b/src/plugins/occurrence/register.ml @@ -216,7 +216,7 @@ let print_one fmt v l = | (Some kf, _, _) :: _ -> Kernel_function.get_name kf | (None,Kstmt _,_)::_ -> assert false | (None,Kglobal,_)::_ -> - fatal "inconsistent context for occurence of variable %s" v.vname + fatal "inconsistent context for occurrence of variable %s" v.vname in if v.vformal then "parameter of " ^ kf_name else "local of " ^ kf_name); diff --git a/src/plugins/scope/dpds_gui.ml b/src/plugins/scope/dpds_gui.ml index b0052bb..019566d 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/security_slicing/security_slicing_parameters.ml b/src/plugins/security_slicing/security_slicing_parameters.ml index 6a7e58c..7b40173 100644 --- a/src/plugins/security_slicing/security_slicing_parameters.ml +++ b/src/plugins/security_slicing/security_slicing_parameters.ml @@ -31,7 +31,7 @@ module Slicing = False (struct let option_name = "-security-slicing" - let help = "perfom the security slicing analysis" + let help = "perform the security slicing analysis" end) (* diff --git a/src/plugins/slicing/fct_slice.ml b/src/plugins/slicing/fct_slice.ml index 7416760..8631141 100644 --- a/src/plugins/slicing/fct_slice.ml +++ b/src/plugins/slicing/fct_slice.ml @@ -1035,7 +1035,7 @@ let choose_precise_slice fi_to_call call_info = if more_outputs then (* not enough outputs in [ff] *) begin - SlicingParameters.debug ~level:2 "[Fct_Slice.choose_precise_slice] %s ? not enought outputs" + SlicingParameters.debug ~level:2 "[Fct_Slice.choose_precise_slice] %s ? not enough outputs" (SlicingMacros.ff_name ff); find slices end @@ -1258,7 +1258,7 @@ let apply_missing_outputs proj ff call output_marks more_outputs = (** check if [f_to_call] is ok for this call, and if so, * change the function call and propagate missing marks in the inputs * if needed. -* @raise ChangeCallErr if [f_to_call] doesn't compute enought outputs. +* @raise ChangeCallErr if [f_to_call] doesn't compute enough outputs. *) let apply_change_call proj ff call f_to_call = SlicingParameters.debug ~level:1 "[Fct_Slice.apply_change_call]"; diff --git a/src/plugins/value/gui_files/register_gui.ml b/src/plugins/value/gui_files/register_gui.ml index 7d1e2c9..f45ff94 100644 --- a/src/plugins/value/gui_files/register_gui.ml +++ b/src/plugins/value/gui_files/register_gui.ml @@ -794,7 +794,7 @@ module Callstacks_manager = struct statement" () in let chk_consolidated = new Widget.checkbox ~label:"Consolidated value" - ~tooltip:"Show values consolidated accross all callstacks" () + ~tooltip:"Show values consolidated across all callstacks" () in let chk_callstacks = new Widget.checkbox ~label:"Per callstack" ~tooltip:"Show values per callstack" () diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml index 3dc6b8f..beb79cd 100644 --- a/src/plugins/value/value_parameters.ml +++ b/src/plugins/value/value_parameters.ml @@ -441,7 +441,7 @@ module WarnCopyIndeterminate = let option_name = "-val-warn-copy-indeterminate" let arg_name = "f | @all" let help = "warn when a statement of the specified functions copies a \ -value that may be indeterminate (uninitalized or containing escaping address). \ +value that may be indeterminate (uninitialized or containing escaping address). \ Set by default; can be deactivated for function 'f' by '=-f', or for all \ functions by '=-@all'." end) diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml index 947a05b..b743720 100644 --- a/src/plugins/value_types/cvalue.ml +++ b/src/plugins/value_types/cvalue.ml @@ -1072,7 +1072,7 @@ module Default_offsetmap = struct let default_contents = Lmap.Bottom (* this works because, currently: - during the analysis, we merge maps with the same variables (all locals - are explicitely present) + are explicitly present) - after the analysis, for synthetic results, we merge maps with different sets of locals, but is is ok to have missing ones considered as being bound to Bottom. diff --git a/src/plugins/wp/VC.mli b/src/plugins/wp/VC.mli index 0f90d67..75de324 100644 --- a/src/plugins/wp/VC.mli +++ b/src/plugins/wp/VC.mli @@ -43,7 +43,7 @@ val get_formula: t -> Lang.F.pred (** {2 Database} Notice that a property or a function have no proof obligation until you - explicitely generate them {i via} the [generate_xxx] functions below. + explicitly generate them {i via} the [generate_xxx] functions below. *) val clear : unit -> unit diff --git a/src/plugins/wp/qed/src/logic.mli b/src/plugins/wp/qed/src/logic.mli index dc316d0..54c3437 100644 --- a/src/plugins/wp/qed/src/logic.mli +++ b/src/plugins/wp/qed/src/logic.mli @@ -423,7 +423,7 @@ sig (** Mark a term to be printed *) val mark : marks -> term -> unit - (** Mark a term to be explicitely shared *) + (** Mark a term to be explicitly shared *) val share : marks -> term -> unit (** Returns a list of terms to be shared among all {i shared} or {i diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml index d1d0952..cea0dd8 100644 --- a/src/plugins/wp/wpAnnot.ml +++ b/src/plugins/wp/wpAnnot.ml @@ -1274,7 +1274,7 @@ let build_configs assigns kf model behaviors ki property = | None -> () | Some Kglobal -> debug - "[get_strategies] select in function properies@." + "[get_strategies] select in function properties@." | Some (Kstmt s) -> debug "[get_strategies] select stmt %d properties@." s.sid diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml index 9ad708a..861dbda 100644 --- a/src/plugins/wp/wp_parameters.ml +++ b/src/plugins/wp/wp_parameters.ml @@ -372,7 +372,7 @@ let () = Parameter_customize.set_group wp_simplifier module BoundForallUnfolding = Int(struct let option_name = "-wp-bound-forall-unfolding" - let help = "Instanciate up to forall-integers hypotheses." + let help = "Instantiate up to forall-integers hypotheses." let arg_name="n" let default = 1000 end)