From d825b30a5a0da18a647779040b31d6103b1423a7 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Mon, 23 Jan 2017 10:10:46 +0100
Subject: [PATCH] [doc] several typos fixed by misspell
---
Changelog | 42 +++++++++----------
Makefile | 2 +-
Makefile.generating | 2 +-
configure.in | 2 +-
doc/aorai/main.tex | 2 +-
doc/developer/changes.tex | 4 +-
doc/developer/check_api/run.oracle | 4 +-
doc/developer/refman.tex | 2 +-
doc/developer/tutorial.tex | 2 +-
doc/jessie/floats/shortprelim.tex | 2 +-
doc/jessie/flottants.tex | 2 +-
doc/pdg/CDG.tex | 12 +++---
doc/release/branch.tex | 2 +-
doc/release/intro.tex | 2 +-
doc/release/website.tex | 4 +-
doc/value/main.tex | 2 +-
ptests/ptests.ml | 2 +-
share/Makefile.common | 2 +-
share/configure.ac | 2 +-
share/libc/netinet/in.h | 2 +-
src/kernel_internals/parsing/clexer.mll | 2 +-
src/kernel_internals/runtime/special_hooks.ml | 2 +-
src/kernel_internals/typing/asm_contracts.ml | 2 +-
src/kernel_internals/typing/cabs2cil.ml | 14 +++----
src/kernel_internals/typing/cfg.mli | 2 +-
src/kernel_internals/typing/mergecil.ml | 2 +-
src/kernel_services/abstract_interp/fval.ml | 4 +-
src/kernel_services/abstract_interp/fval.mli | 2 +-
src/kernel_services/abstract_interp/ival.ml | 4 +-
.../abstract_interp/lmap_sig.mli | 2 +-
.../abstract_interp/locations.mli | 8 ++--
.../abstract_interp/offsetmap.ml | 4 +-
.../abstract_interp/origin.mli | 2 +-
src/kernel_services/analysis/dataflow.mli | 4 +-
src/kernel_services/analysis/dataflow2.ml | 2 +-
src/kernel_services/analysis/dataflows.mli | 4 +-
src/kernel_services/analysis/exn_flow.ml | 2 +-
src/kernel_services/analysis/logic_interp.ml | 24 +++++------
src/kernel_services/analysis/ordered_stmt.ml | 2 +-
.../analysis/wto_statement.mli | 2 +-
src/kernel_services/ast_data/cil_types.mli | 10 ++---
src/kernel_services/ast_data/globals.ml | 4 +-
src/kernel_services/ast_data/globals.mli | 2 +-
.../ast_data/property_status.mli | 8 ++--
.../ast_printing/cil_printer.ml | 2 +-
.../ast_printing/printer_api.mli | 6 +--
src/kernel_services/ast_queries/ast_info.mli | 8 ++--
src/kernel_services/ast_queries/cil.ml | 14 +++----
src/kernel_services/ast_queries/file.ml | 2 +-
.../ast_queries/logic_const.mli | 2 +-
src/kernel_services/ast_queries/logic_env.ml | 4 +-
.../ast_queries/logic_typing.ml | 4 +-
.../ast_queries/logic_typing.mli | 2 +-
.../ast_queries/logic_utils.ml | 4 +-
.../cmdline_parameters/parameter_builder.ml | 2 +-
.../plugin_entry_points/db.mli | 26 ++++++------
.../plugin_entry_points/journal.mli | 2 +-
.../plugin_entry_points/kernel.ml | 2 +-
.../plugin_entry_points/log.ml | 2 +-
.../plugin_entry_points/log.mli | 2 +-
.../plugin_entry_points/plugin.ml | 2 +-
src/libraries/stdlib/integer.mli | 8 ++--
src/libraries/utils/bitvector.ml | 2 +-
src/libraries/utils/pretty_utils.mli | 4 +-
src/libraries/utils/rangemap.mli | 2 +-
src/libraries/utils/rgmap.mli | 2 +-
src/libraries/utils/vector.mli | 4 +-
src/plugins/aorai/aorai_utils.ml | 2 +-
src/plugins/aorai/data_for_aorai.ml | 2 +-
src/plugins/aorai/utils_parser.ml | 2 +-
src/plugins/from/from_compute.ml | 4 +-
src/plugins/gui/design.ml | 4 +-
src/plugins/gui/design.mli | 4 +-
src/plugins/gui/file_manager.ml | 2 +-
src/plugins/gui/gtk_helper.mli | 2 +-
src/plugins/gui/pretty_source.ml | 2 +-
src/plugins/gui/wpane.mli | 2 +-
src/plugins/impact/register_gui.ml | 2 +-
src/plugins/inout/Inout.mli | 2 +-
src/plugins/inout/cumulative_analysis.mli | 2 +-
src/plugins/metrics/metrics_cabs.ml | 2 +-
src/plugins/metrics/metrics_cilast.ml | 2 +-
src/plugins/occurrence/Occurrence.mli | 2 +-
src/plugins/occurrence/register.ml | 2 +-
src/plugins/pdg/annot.mli | 2 +-
src/plugins/pdg/pdg_state.ml | 2 +-
src/plugins/pdg_types/pdgTypes.ml | 2 +-
src/plugins/print_api/print_interface.ml | 4 +-
src/plugins/rte/visit.ml | 4 +-
src/plugins/security_slicing/components.ml | 2 +-
src/plugins/slicing/fct_slice.ml | 2 +-
src/plugins/slicing/register.ml | 2 +-
src/plugins/slicing/slicingCmds.ml | 12 +++---
src/plugins/slicing/slicingTransform.ml | 2 +-
src/plugins/slicing_types/slicingInternals.ml | 2 +-
src/plugins/sparecode/globs.ml | 2 +-
src/plugins/sparecode/spare_marks.ml | 2 +-
src/plugins/value/alarmset.ml | 2 +-
src/plugins/value/domains/abstract_domain.mli | 2 +-
.../value/domains/apron/apron_domain.ok.ml | 2 +-
.../value/domains/cvalue/builtins_malloc.ml | 4 +-
.../value/domains/cvalue/builtins_string.mli | 2 +-
.../value/domains/cvalue/cvalue_init.ml | 2 +-
.../value/domains/gauges/gauges_domain.ml | 8 ++--
src/plugins/value/domains/symbolic_locs.ml | 2 +-
src/plugins/value/engine/abstractions.mli | 2 +-
src/plugins/value/engine/evaluation.ml | 2 +-
src/plugins/value/engine/initialization.ml | 2 +-
src/plugins/value/engine/initialization.mli | 2 +-
.../value/engine/non_linear_evaluation.ml | 2 +-
src/plugins/value/eval.ml | 2 +-
src/plugins/value/eval.mli | 2 +-
src/plugins/value/gui_files/register_gui.ml | 2 +-
src/plugins/value/legacy/eval_annots.ml | 2 +-
src/plugins/value/legacy/eval_exprs.ml | 2 +-
src/plugins/value/legacy/eval_op.ml | 2 +-
src/plugins/value/legacy/initial_state.ml | 2 +-
src/plugins/value/legacy/valarms.ml | 2 +-
src/plugins/value/value_parameters.ml | 2 +-
src/plugins/value/values/cvalue_forward.ml | 4 +-
src/plugins/value_types/cvalue.ml | 4 +-
src/plugins/value_types/function_Froms.ml | 2 +-
src/plugins/wp/Changelog | 4 +-
src/plugins/wp/Cint.ml | 2 +-
src/plugins/wp/GuiGoal.ml | 2 +-
src/plugins/wp/Letify.mli | 2 +-
src/plugins/wp/MemTyped.ml | 2 +-
src/plugins/wp/TacInstance.ml | 2 +-
src/plugins/wp/TacNormalForm.ml | 2 +-
src/plugins/wp/VC.mli | 2 +-
src/plugins/wp/calculus.ml | 2 +-
src/plugins/wp/cil2cfg.mli | 2 +-
src/plugins/wp/doc/manual/wp_caveat.tex | 2 +-
src/plugins/wp/doc/manual/wp_intro.tex | 2 +-
src/plugins/wp/doc/manual/wp_plugin.tex | 4 +-
src/plugins/wp/doc/tutorial/count/count.tex | 2 +-
src/plugins/wp/doc/tutorial/tut_intro.tex | 4 +-
src/plugins/wp/doc/wp-api.odoc | 2 +-
src/plugins/wp/qed/old/proof.mli | 2 +-
src/plugins/wp/qed/src/engine.mli | 4 +-
src/plugins/wp/qed/src/logic.mli | 4 +-
src/plugins/wp/qed/src/term.ml | 4 +-
src/plugins/wp/share/Makefile.headers | 2 +-
src/plugins/wp/share/src/qed.why | 2 +-
src/plugins/wp/share/src/vlist.why | 2 +-
src/plugins/wp/share/why3/Bits.v | 10 ++---
src/plugins/wp/wpAnnot.ml | 2 +-
src/plugins/wp/wpPropId.mli | 2 +-
src/plugins/wp/wpStrategy.mli | 4 +-
src/plugins/wp/wp_parameters.mli | 2 +-
tests/slicing/README | 2 +-
tests/slicing/merge.ml | 2 +-
152 files changed, 271 insertions(+), 271 deletions(-)
diff --git a/Changelog b/Changelog
index 6f96ab95d3f..ccd26c12d2e 100644
--- a/Changelog
+++ b/Changelog
@@ -75,7 +75,7 @@ Open Source Release Silicon-20161101
-! Libc [2016/10/07] Functions in share/libc.c have been inlined into
the proper .c files under share/libc
- Eva [2016/10/07] More systematic backward-propagation between
- actual paramaters and formals
+ actual parameters and formals
- Nonterm [2016/10/05] overall increase in precision, especially on
compound statements (if, switch, loops...). Verbosity has been
decreased
@@ -205,7 +205,7 @@ o! Value [2016/03/30] API change in functor Lmap.Make.
bounds and -slevel-function parameters. Invoked using option
-loop.
-* ACSL [2016/03/30] Fixes precedence uncompliance within ACSL Manual of
- some bitwise operators and more agressive checks of consistent
+ some bitwise operators and more aggressive checks of consistent
relation chains.
-* Metrics [2016/03/24] Fix list of undefined functions; functions that
are never called were not reported.
@@ -258,7 +258,7 @@ o! Value [2016/03/30] API change in functor Lmap.Make.
-* Libc [2016/02/02] Fix specifications of memchr and strncpy.
-* ACSL [2016/01/27] Fixes example of logic label use. Fixes bug #2203.
-* Logic [2016/01/17] Meaningless assigns clauses are now rejected more
- agressively. Fixes bug #1790.
+ aggressively. Fixes bug #1790.
o Kernel [2016/01/08] Several incompatible changes in module Property.
- Kernel [2016/01/08] Automatic generation of assigns from GCC's extended
asm.
@@ -273,7 +273,7 @@ o Kernel [2016/01/08] Several incompatible changes in module Property.
compatibility between the type of the pointer and the function
being pointed.
-* Eva [2016/01/01] Fixed some bugs related to 0. vs. -0. in conditions.
-- Eva [2016/01/01] More agressive reductions in complex conditions
+- Eva [2016/01/01] More aggressive reductions in complex conditions
such as if(a+3 < 10).
-*! Value [2016/01/01] Reimplementation of all the upper layers of the
plugin. Compatibility with the legacy version is almost complete,
@@ -310,7 +310,7 @@ o! Gui [2015/12/01] Refactor GUI Helpers.
precise) when the loops are not fully unrolled by slevel.
-! Makefile [2015/11/26] Target 'make rebuild' has been renamed into
'make clean-rebuild'.
--* Value [2015/11/24] The preconditions of functions overriden by builtins
+-* Value [2015/11/24] The preconditions of functions overridden by builtins
no longer receive an 'Unreachable status for calls within dead
code: the specification is ignored everywhere. Fixes bug #!1956.
-! Cil [2015/11/23] Incorrect return statements (return void on non-void
@@ -457,7 +457,7 @@ o! Value [2015/06/25] Remove duplicate values Ival.singleton_zero and
-* Parsing [2015/06/22] Black-list gcc's builtin macros for logic
pre-processing to avoid warnings for duplication. Fixes bug #2161.
-* Logic [2015/06/15] Fix typing bug when converting into a term an
- expression containing a pointer substraction.
+ expression containing a pointer subtraction.
-* Value [2015/06/09] Pointer comparisons using relational operators (<,
>=, etc) between a pointer and NULL is now flagged as undefined.
o! Kernel [2015/06/09] Remove support of plug-ins without .mli.
@@ -984,14 +984,14 @@ o Kernel [2013/11/08] parameters can be preserved across project creation
o* Value [2013/10/27] Type Base.string_id is now concrete. No more need
for function Base.cstring_of_string_id
-* RTE [2013/10/28] Better normalization when using -rte-precond.
-- Kernel [2013/10/27] Generate more agressive assigns clauses for
+- Kernel [2013/10/27] Generate more aggressive assigns clauses for
unspecified library functions that arguments with type pointer
to void or char
-* Kernel [2013/10/26] Do not generate invalid assigns clauses when some
formals are pointers to arrays
- Kernel [2013/10/22] Support for static evaluation of the
__builtin_compatible_p GCC specific function.
-- Kernel [2013/10/22] Add -agressive-merging option to merge two
+- Kernel [2013/10/22] Add -aggressive-merging option to merge two
inline functions if they are equal modulo alpha conversion.
-* Kernel [2013/10/17] Correctly distinguish typenames and declared
identifiers in declarations. Fixes #1500
@@ -1055,7 +1055,7 @@ o* Kernel [2013/09/11] Fixed buggy function Property.location.
- Value [2013/09/07] Degeneration points are now shown in the GUI
- Value [2013/09/07] Value analysis can now be aborted while keeping
intermediate results, by sending SIGUSR1 to Frama-C
-- Value [2013/09/06] More agressive evaluation of \initialized(p)
+- Value [2013/09/06] More aggressive evaluation of \initialized(p)
when p points to a memory zone containing both bottom and
non-bottom values
o! Value [2013/09/06] Function Cvalue.Model.find_unspecified now requires
@@ -1311,7 +1311,7 @@ o! Cil [2013/02/02] Remove unused 'alignof_char_array' machdep field.
-* Kernel [2013/02/01] Ghost status is appropriately propagated in
statements (instead of only instructions) and pretty-printed
accordingly. Fixes issue #1328.
-- Value [2013/02/01] Value more agressive evaluation of construct
+- Value [2013/02/01] Value more aggressive evaluation of construct
'//@ for b: assert p' when b is guaranteed to be active.
Harmonize behaviors-related messages.
- Kernel [2013/01/29] The level of verbose is at least the level of debug.
@@ -1385,7 +1385,7 @@ o! Kernel [2012/11/24] Various types whose names started by t_ in
o Rte [2012/11/23] Export function "exp_annotations" to get RTEs of a C
expression as annotations.
o*!Kernel [2012/11/23] Added TLogic_coerce constructor to mark
- explicitely a conversion from a C type to a logical one
+ explicitly a conversion from a C type to a logical one
(in particular floating point -> real and integral -> integer).
Fixes issue #1309.
o! Kernel [2012/11/22] Remove unintuitive ?prj argument from Cil visitors,
@@ -1424,7 +1424,7 @@ o! Kernel [2012/10/18] New API for module Alarms.
annotations corresponding to an alarm.
o* Kernel [2012/10/18] Fixes incorrect visitor behavior with JustCopy
(issue #1282).
-- Value [2012/10/16] Reduce more agressively on accesses *p where p is
+- Value [2012/10/16] Reduce more aggressively on accesses *p where p is
imprecise but contains only one valid value.
-* Value [2012/10/16] Correct potentially incorrect reduction on l-values
of the form *(p+off) or *(p-off).
@@ -1960,7 +1960,7 @@ o! Value [2011/08/09] Module Cvalue_type renamed to Cvalue.
o Kernel [2011/08/04] Add Kernel.Unicode.without_unicode, which applies
a function without upsetting the Unicode option in the gui.
-* Impact [2011/08/04] Correct a journalisation bug in gui mode.
-- Value [2011/08/01] More precise when an alarm is emited in a loop.
+- Value [2011/08/01] More precise when an alarm is emitted in a loop.
o! Kernel [2011/08/01] Signature of Plugin renamed for consistency.
Use carbon2nitrogen for automatic translation.
o! Kernel [2011/08/01] Annotations.replace and
@@ -2035,7 +2035,7 @@ o! Value [2011/06/03] Functions valid_* now take an argument ~for_writing
Pass true when the lvalue being considered is used for
writing in the program. Pass false when unsure.
- Value [2011/06/03] Literal strings are now read-only.
-- Value [2011/06/03] More agressive state reduction when emiting
+- Value [2011/06/03] More aggressive state reduction when emitting
pointer_comparable assertions. Use option
-undefined-pointer-comparison-propagate-all if you liked
the old behavior better.
@@ -2141,8 +2141,8 @@ o* Kernel [2011/04/13] Fix bug #790: AST integrity checker issue.
-* Pdg [2011/04/13] Fix bug #787 but leads to less precise dependencies.
-* Slicing [2011/04/02] Fix bug #786: missing label in sliced program.
-* Value [2011/04/12] Correctly emit \pointer_comparable(...) alarms.
--* From [2011/04/11] Fix #781: handling of function calls with an implict
- cast for the assignment of the result.
+-* From [2011/04/11] Fix #781: handling of function calls with an
+ implicit cast for the assignment of the result.
o Makefile [2011/04/08] Add target to launch the tests of a specific
dynamic internal plugin from Frama-C's main Makefile.
-* Aorai [2011/04/08] Existing assigns are augmented with the locations
@@ -2523,7 +2523,7 @@ o! Value [2010/07/21] There was one too many function called "find_ival".
sandbox.
- Configure [2010/07/05] Better detection of native dynlink support.
-* GUI [2010/06/30] Fixed parsing of floats in frama-c-gui.config
-- Cil [2010/06/30] Be less agressive during inline function merge.
+- Cil [2010/06/30] Be less aggressive during inline function merge.
Alpha equivalent function are now kept separate.
- GUI [2010/06/29] One tooltip by parameter in the launcher
o! Cil [2010/06/23] Removed function varinfo_from_vid. You can use
@@ -2565,7 +2565,7 @@ o! Kernel [2010/05/20] Added field b_extended in behaviors to
-* Logic [2010/05/19] Checking for loop variant position
- Kernel [2010/05/19] Feature #484 about requires into named behaviors
-* Inout [2010/05/12] Fixed bug in -inout where operational inputs of
- called library function were improperly infered from assigns
+ called library function were improperly inferred from assigns
-* Value [2010/05/12] Fixed bug with extern variables of incomplete type
-* Logic [2010/05/11] Fixed wrong precedence of <==>
- Value [2010/05/11] Improved Frama_C_memcpy built-in.
@@ -2748,7 +2748,7 @@ o! Kernel [2009/11/24] Use of global logic constants is now a
settable via the launcher dialog box (bts #!317).
-* Logic [2009/11/04] Fixed bug #272 (complete behaviors wo name)
- Logic [2009/11/03] Better error message when using = in annotations
--* Makefile [2009/11/02] Fixed bug #310: improve robustness againts new
+-* Makefile [2009/11/02] Fixed bug #310: improve robustness against new
ocaml warnings.
- Kernel [2009/11/02] New option -no-dynlink in order to prevent
loading of dynamic plug-ins.
@@ -2836,7 +2836,7 @@ o* Makefile [2009/09/18] Fixed bugs with the use of PLUGIN_EXTRA_BYTE
part of Why.
- Makefile [2009/09/08] Why is no longer a compilation dependency.
It is required only at runtime for the experimental WP plugin.
--* Makefile [2009/09/07] Fixed compilation error occuring on a platform
+-* Makefile [2009/09/07] Fixed compilation error occurring on a platform
which does not support native dynlink and with ocaml >= 3.11
(bts #224).
@@ -2924,7 +2924,7 @@ o GUI [2009/06/05] The plug-in GUI is now packed with the core plug-in
-* Jessie [2009/06/05] Fix bug #!8, compilation of jessie with Apron
-* Configure [2009/06/05] Fixed issues in configure and makefile if
lablgtk2 is not enabled.
-o! Kernel [2009/06/03] Moved lightweigth annotation support from
+o! Kernel [2009/06/03] Moved lightweight annotation support from
Jessie to Kernel. They are now available for all plugins.
Support for lightweight global invariants on globals has
been dropped.
diff --git a/Makefile b/Makefile
index 25bf88efb8b..cf1e854254b 100644
--- a/Makefile
+++ b/Makefile
@@ -707,7 +707,7 @@ SINGLE_GUI_CMO:= $(patsubst %,src/plugins/gui/%.cmo,$(SINGLE_GUI_CMO))
# Plug-in sections # #
#################### #
# #
-# For 'internal' developpers: #
+# For 'internal' developers: #
# you can add your own plug-in here, #
# but it is better to have your own separated Makefile #
###############################################################################
diff --git a/Makefile.generating b/Makefile.generating
index 063b2a11c93..bf8b8ad3bfe 100644
--- a/Makefile.generating
+++ b/Makefile.generating
@@ -121,7 +121,7 @@ $(MACHDEP_PATH)/local_machdep.ml: \
# Now generate the type definition
$(ECHO) "open Cil_types" >> $@
if $(CC) -D_GNUCC $< -o bin/machdep.exe ;then \
- $(ECHO) "machdep.exe created succesfully."; \
+ $(ECHO) "machdep.exe created successfully."; \
else \
$(RM) $@; exit 1; \
fi
diff --git a/configure.in b/configure.in
index ace93be018f..c3705a3a592 100644
--- a/configure.in
+++ b/configure.in
@@ -646,7 +646,7 @@ PLUGINS_FORCE_LIST=
# Plug-in sections # #
#################### #
# #
-# For 'internal' developpers: #
+# For 'internal' developers: #
# Add your own plug-in here #
# #
###############################################################################
diff --git a/doc/aorai/main.tex b/doc/aorai/main.tex
index c85bb87e291..85c46c98adf 100644
--- a/doc/aorai/main.tex
+++ b/doc/aorai/main.tex
@@ -362,7 +362,7 @@ followed by a comma separated list containing the states' name
\begin{new}
\item By default, \aorai considers that all functions calls and returns trigger
a transition of the automaton. In order to have transitions only for the
-functions that explicitely appear in the description of the automaton, the
+functions that explicitly appear in the description of the automaton, the
following directive must be used:
\begin{lstlisting}[language=ya]
%explicit transitions;
diff --git a/doc/developer/changes.tex b/doc/developer/changes.tex
index facba81bd7e..b2acdb7043a 100644
--- a/doc/developer/changes.tex
+++ b/doc/developer/changes.tex
@@ -199,7 +199,7 @@ We list changes of previous releases below.
\item \textbf{Architecture}: update according to the recent implementation
changes
\item \textbf{Tutorial}: update according to API changes and the new way of
- writting plug-ins
+ writing plug-ins
\item \textbf{configure.in}: update according to changes in the way of adding a
simple plug-in
\item \textbf{Plug-in Registration and Access}: update according to the new API
@@ -214,7 +214,7 @@ We list changes of previous releases below.
Option Values}
\item \textbf{Configure.in}: compliant with new implementations of
\texttt{configure\_library} and \texttt{configure\_tool}
-\item \textbf{Exporting Datatypes}: now embeded in new section \emph{Plug-in
+\item \textbf{Exporting Datatypes}: now embedded in new section \emph{Plug-in
Registration and Access}
\item \textbf{GUI}: update, in particular the full example has been removed
\item \textbf{Introduction}: improved
diff --git a/doc/developer/check_api/run.oracle b/doc/developer/check_api/run.oracle
index 387f497b0f9..7196c28e347 100644
--- a/doc/developer/check_api/run.oracle
+++ b/doc/developer/check_api/run.oracle
@@ -118,7 +118,7 @@ Cil.cilVisitor.vglob/Cil_types.global -> Cil_types.global list Cil.visitAction/G
Parameter_sig.Builder.String/string end ) -> Parameter_sig.String/What is the possible range of values for this parameter./
State/t -> unitend /A state is a project-compliant mutable value./
Type.name/'a Type.t -> string/Apply this functor to access to the abstract type of the given name./
-Log.Messages.debug/?level:int -> ?dkey:Log.category -> 'a Log.pretty_printer/Debugging information dedicated to Plugin developpers. Default level is 1. The debugging key is used in message headers. See also set_debug_keys and set_debug_keyset./
+Log.Messages.debug/?level:int -> ?dkey:Log.category -> 'a Log.pretty_printer/Debugging information dedicated to Plugin developers. Default level is 1. The debugging key is used in message headers. See also set_debug_keys and set_debug_keyset./
Cil_state_builder/functor (Data : Datatype.S ) -> functor (Info : State_builder.Info_with_size ) -> State_builder.Hashtbl with type key = Cil_types.varinfo and type data = Data.tend /Functors for building computations which use kernel datatypes./
Cil_printer.register_behavior_extension/string -> (Printer_api.extensible_printer_type -> Format.formatter -> int * Cil_types.identified_predicate list -> unit) -> unit/Register a pretty-printer used for behavior extension./
Structural_descr.p_int/Structural_descr.pack/Equivalent to pack Abstract/
@@ -228,4 +228,4 @@ Project_skeleton.t/{pid: int; mutable name: string; mutable unique_name: string}
Cil.get_kernel_function/Cil.visitor_behavior -> Cil_types.kernel_function -> Cil_types.kernel_function//
State_builder/?prj:Project.t -> string -> 'a Type.t -> 'a * boolend end /State builders. Provide ways to implement signature State_builder.S. Depending on the builder, also provide some additional useful information./
Cil.cilVisitor.current_kinstr/Cil_types.kinstr/Kstmt stmt when visiting statement stmt, Kglobal when called outside of a statement./
-Parameter_sig.Int/Parameter_sig.Int/Signature for an integer parameter./
\ No newline at end of file
+Parameter_sig.Int/Parameter_sig.Int/Signature for an integer parameter./
diff --git a/doc/developer/refman.tex b/doc/developer/refman.tex
index a7597b90da2..9af475f8b62 100644
--- a/doc/developer/refman.tex
+++ b/doc/developer/refman.tex
@@ -1031,7 +1031,7 @@ can be used to override the default value of 4.
\emph{Example value:} \texttt{-j 6}
\item \texttt{OCAML\_ANNOT\_OPTION}: this variable of the Makefile
-can be overriden in \texttt{.Makefile.user}.
+can be overridden in \texttt{.Makefile.user}.
By default, it is set to \texttt{-annot -bin-annot}. Users of
\textsf{Merlin}\index{Merlin} do not need \texttt{-annot}.
diff --git a/doc/developer/tutorial.tex b/doc/developer/tutorial.tex
index 30909ef11d8..17889df9339 100644
--- a/doc/developer/tutorial.tex
+++ b/doc/developer/tutorial.tex
@@ -726,7 +726,7 @@ following architecture:
\item \texttt{cfg\_options.ml} implements plug-in registration and
configuration options;
\item \texttt{cfg\_core.ml} implements the main functions for
- computating the CFG;
+ computing the CFG;
\item \texttt{cfg\_register.ml} implements ``global'' computation of
the CFG using the \texttt{-cfg} option, and hooking into the \framac
main loop;
diff --git a/doc/jessie/floats/shortprelim.tex b/doc/jessie/floats/shortprelim.tex
index 445267fd791..5ee3c57da3d 100644
--- a/doc/jessie/floats/shortprelim.tex
+++ b/doc/jessie/floats/shortprelim.tex
@@ -333,7 +333,7 @@ including higher-order functions, polymorphism, references, arrays and
exceptions.
The Why language is inspired from the {\it Ocaml}~\cite{ObjectiveCamlManual3.01}
-language for functionnal programs.
+language for functional programs.
So there is no distinction between instructions and expressions.
Special keywords are reserved in Why, for example, \verb|result|
denotes the value returned by a function and is used only in the postcondition.
diff --git a/doc/jessie/flottants.tex b/doc/jessie/flottants.tex
index 15fd03b202c..a785a2d3f45 100644
--- a/doc/jessie/flottants.tex
+++ b/doc/jessie/flottants.tex
@@ -246,7 +246,7 @@ They are written immediately before the C loops {\it for, while}, etc ...
The platform Why aims at being a verification conditions generator (VCG) back-end for other verification tools. It provides a powerful input language including higher-order functions, polymorphism, references, arrays and exceptions.
\newline
-The {\it Why} language is inspired from the {\it Ocaml}~\cite{ObjectiveCamlManual3.01} language for functionnal programs. So there is no distinction between instructions and expressions. Special keywords are reserved in {\it Why}, for example, \verb|result| denotes the value returned by a function and is used only in the postcondition. Programs in {\it Why} language can be annotated by preconditions, assertions, postconditions, loop invariant and loop variant to ensure the termination.
+The {\it Why} language is inspired from the {\it Ocaml}~\cite{ObjectiveCamlManual3.01} language for functional programs. So there is no distinction between instructions and expressions. Special keywords are reserved in {\it Why}, for example, \verb|result| denotes the value returned by a function and is used only in the postcondition. Programs in {\it Why} language can be annotated by preconditions, assertions, postconditions, loop invariant and loop variant to ensure the termination.
The language contains basic built-in types: \verb|bool|, \verb|unit|, \verb|int| and \verb|real|. The expressions in {\it Why} are formed by:
\begin{itemize}
\item The integer, boolean constants.
diff --git a/doc/pdg/CDG.tex b/doc/pdg/CDG.tex
index ddfc4bf0a76..eb1b63454f9 100644
--- a/doc/pdg/CDG.tex
+++ b/doc/pdg/CDG.tex
@@ -50,18 +50,18 @@ Let's prove it~:
\begin{itemize}
\item either X is postdominated by S, but not by G (ie. X in $PDB(G,S)$).
-It means that when the program pass throught G,
-it might be the case that it will not go throught X in the original program,
-but it always go throught it if the jump is removed, because the program will then go throught S which is postdominated by X.
+It means that when the program pass through G,
+it might be the case that it will not go through X in the original program,
+but it always go through it if the jump is removed, because the program will then go through S which is postdominated by X.
So, in this case, if X is in the slice, G has to be in it too.
\item or X is postdominated by L, but not by S, and is different from S
(ie. X in $PDB(S,L)-{S}$).
-It means that when the program pass throught G, if will go throught X
-in the original program, but if the jump is removed, it will go throught S,
-and then it might be the case that it will not go throught X because S
+It means that when the program pass through G, if will go through X
+in the original program, but if the jump is removed, it will go through S,
+and then it might be the case that it will not go through X because S
is not postdominated by X, except if X=S.
So, in this case, if X is in the slice, G has also to be in it.\\
diff --git a/doc/release/branch.tex b/doc/release/branch.tex
index 4bc235b499f..0d5391c728d 100644
--- a/doc/release/branch.tex
+++ b/doc/release/branch.tex
@@ -8,7 +8,7 @@ That is the procedure for forking the release from \texttt{master}.
Create the branch \texttt{stable/release} where \texttt{release} is the
element name.
-What can be commited in this branch must follow the release schedule,
+What can be committed in this branch must follow the release schedule,
and go through Merge-requests. Everything else should go in \texttt{master}.
diff --git a/doc/release/intro.tex b/doc/release/intro.tex
index 55985a6028a..9ff6dbf54e4 100644
--- a/doc/release/intro.tex
+++ b/doc/release/intro.tex
@@ -36,7 +36,7 @@ A \FramaC release consists of the following main steps:
branche is dedicated to the ongoing release.
\item \textbf{The build stage.} The source files are setup by the
- developpers, and the bug tracking system is updated to reflect the
+ developers, and the bug tracking system is updated to reflect the
distribution state. A source distribution is created and registered,
with its updated documentation.
diff --git a/doc/release/website.tex b/doc/release/website.tex
index 34004e72a12..aa630b85543 100644
--- a/doc/release/website.tex
+++ b/doc/release/website.tex
@@ -2,7 +2,7 @@
Where all our efforts goes on the web. There are two very different
tasks for \FramaC to go online. Authoring the web site pages is the
-responsibility of the developpers and the release manager. Publishing
+responsibility of the developers and the release manager. Publishing
the web site can only be performed by authorized peoples, who may not
be the release manager.
@@ -12,7 +12,7 @@ You need \texttt{pandoc} and \texttt{tidy} to perform those steps.
They can be installed from your Linux distribution.
\section{Authoring the Pages}
-To edit the web pages of the site, developpers only need the
+To edit the web pages of the site, developers only need the
\texttt{trunk} branch of the repository. The web site sources are in
\texttt{src} or the checkout of the \texttt{website} tree.
diff --git a/doc/value/main.tex b/doc/value/main.tex
index eee5c41225a..5a99248d6d7 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -3512,7 +3512,7 @@ functions than \verb+f+. Moreover, EVA does not attempt
to check that \verb+f+ conforms to its specification. In particular,
postconditions are marked as {\em unknown} with \verb+-val-use-spec+,
while they are {\em considered valid} for functions without body.
-It is the responsability
+It is the responsibility
of the user to verify those facts, for example by studying \verb+f+
on its own in a generic context.
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index d73a165cbd2..4949cb7a2b9 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -229,7 +229,7 @@ let example_msg =
@@PTEST_CONFIG@@ \
# test configuration suffix@ \
@@PTEST_FILE@@ \
- # substitued by the test filename@ \
+ # substituted by the test filename@ \
@@PTEST_DIR@@ \
# dirname of the test file@ \
@@PTEST_NAME@@ \
diff --git a/share/Makefile.common b/share/Makefile.common
index 4c88e5cf8c4..1db84ce3a7b 100644
--- a/share/Makefile.common
+++ b/share/Makefile.common
@@ -74,7 +74,7 @@ endif
# Flags to be used by ocamlc and ocamlopt when compiling Frama-C
# itself. For development versions, we add -warn-error for most
# warnings -warn-error has effect only for warnings that are
-# explicitely set using '-w'.
+# explicitly set using '-w'.
ifeq ($(DEVELOPMENT),yes)
# Most warnings are activated by default. The few that are deactivated are
# impossible to silence with the current Frama-C. Those settings are inherited
diff --git a/share/configure.ac b/share/configure.ac
index 79c84a799e6..078cf571783 100644
--- a/share/configure.ac
+++ b/share/configure.ac
@@ -409,7 +409,7 @@ lt_mark () {
# $2: mark to propagate to requires
# $3: mark to propagate to users
check_and_propagate () {
- # for each requiers
+ # for each requires
r=REQUIRE_$1
eval require="\$$r"
for p in $require; do
diff --git a/share/libc/netinet/in.h b/share/libc/netinet/in.h
index 0c4e8200262..edbb6a3777a 100644
--- a/share/libc/netinet/in.h
+++ b/share/libc/netinet/in.h
@@ -145,7 +145,7 @@ enum
-/*** originaly from bits/in.h ***/
+/*** originally from bits/in.h ***/
/* Options for use with `getsockopt' and `setsockopt' at the IP level.
The first word in the comment at the right is the data type used;
diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll
index c874fb0c5b1..3b463ccf493 100644
--- a/src/kernel_internals/parsing/clexer.mll
+++ b/src/kernel_internals/parsing/clexer.mll
@@ -357,7 +357,7 @@ let wbtowc wstr =
dest
*)
-(* This function converst the "Hi" in L"Hi" to { L'H', L'i', L'\0' }
+(* This function converts the "Hi" in L"Hi" to { L'H', L'i', L'\0' }
matth: this seems unused.
let wstr_to_warray wstr =
let len = String.length wstr in
diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml
index d2c8cce9cd5..32a1d5b7dd7 100644
--- a/src/kernel_internals/runtime/special_hooks.ml
+++ b/src/kernel_internals/runtime/special_hooks.ml
@@ -126,7 +126,7 @@ let () =
(* implement behavior described in BTS #1388:
- on normal exit: save
- on Sys.break, system error, user error or feature request: do not save
- - on fatal error or unexpected error: save, but slighly change the
+ - on fatal error or unexpected error: save, but slightly change the
generated filename. *)
Cmdline.at_normal_exit (fun () -> save_binary true);
Cmdline.at_error_exit
diff --git a/src/kernel_internals/typing/asm_contracts.ml b/src/kernel_internals/typing/asm_contracts.ml
index 3496d74ca26..c30fa220e01 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_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 053e9b1cd6f..ac8b91de240 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -717,7 +717,7 @@ let alreadyDefined: (string, location) H.t = H.create 117
let staticLocals: (string, varinfo) H.t = H.create 13
-(* Typedefs. We chose their names to be distinct from any global encounterd
+(* Typedefs. We chose their names to be distinct from any global encountered
* at the time. But we might see a global with conflicting name later in the
* file *)
let typedefs: (string, typeinfo) H.t = H.create 13
@@ -1198,7 +1198,7 @@ let findCompType (kind: string) (n: string) (a: attributes) =
with Not_found -> makeForward ()
-(* A simple visitor that searchs a statement for labels *)
+(* A simple visitor that searches a statement for labels *)
class canDropStmtClass pRes = object
inherit nopCilVisitor
@@ -5120,7 +5120,7 @@ and isIntegerConstant ghost (aexp) : int option =
* extract the effects as separate statements.
* doExp returns the following 4-uple:
* - a list of read accesses performed for the evaluation of the expression
- * - a chunk representing side-effects occuring during evaluation
+ * - a chunk representing side-effects occurring during evaluation
* - the CIL expression
* - its type.
*)
@@ -5394,7 +5394,7 @@ and doExp local_env
finishExp [] (unspecified_chunk empty) res (typeOf res)
| A.CONST_STRING s ->
- (* Maybe we burried __FUNCTION__ in there *)
+ (* Maybe we buried __FUNCTION__ in there *)
let s' =
try
let start = String.index s (Char.chr 0) in
@@ -6985,7 +6985,7 @@ and doBinOp loc (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) =
in
let doArithmeticComp () =
let tres = arithmeticConversion t1 t2 in
- (* Keep the operator since it is arithemtic *)
+ (* Keep the operator since it is arithmetic *)
intType,
optConstFoldBinOp loc false bop
(makeCastT e1 t1 tres) (makeCastT e2 t2 tres) intType
@@ -8070,7 +8070,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
Cil.update_var_type vi et;
if isNotEmpty se then
Kernel.error ~once:true ~current:true "global static initializer";
- (* Check that no locals are refered by the initializer *)
+ (* Check that no locals are referred by the initializer *)
check_no_locals_in_initializer ie';
(* Maybe the initializer refers to the function itself.
Push a prototype for the function, just in case. *)
@@ -8934,7 +8934,7 @@ and assignInit ~ghost (lv: lval)
completely. We'll do that ourselves, with
- a bzero to 0
- a contract for plugins that do not want to rely on bzero.
- All that is done at the toplevel occurence of implicit
+ All that is done at the toplevel occurrence of implicit
initialization.
*)
let (curr_host,curr_off) = lv in
diff --git a/src/kernel_internals/typing/cfg.mli b/src/kernel_internals/typing/cfg.mli
index a888a10244d..db42387f27e 100644
--- a/src/kernel_internals/typing/cfg.mli
+++ b/src/kernel_internals/typing/cfg.mli
@@ -60,7 +60,7 @@ val clearFileCFG: ?clear_id:bool -> file -> unit
filled in *)
val cfgFun : fundec -> unit
-(** clear the sid, succs, and preds fields of each statment in a function *)
+(** clear the sid, succs, and preds fields of each statement in a function *)
val clearCFGinfo: ?clear_id:bool -> fundec -> unit
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 247b49758c4..6dc74339d42 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -2462,7 +2462,7 @@ let oneFilePass2 (f: file) =
false (* do not emit *)
)
else if prevInitOpt = None then (
- (* The previous occurence was only a tentative defn. Now,
+ (* The previous occurrence was only a tentative defn. Now,
we have a real one. Set the correct value in the table,
and tell that we need to change the previous into a GVarDecl
*)
diff --git a/src/kernel_services/abstract_interp/fval.ml b/src/kernel_services/abstract_interp/fval.ml
index 844ec5dca50..165cb80d8be 100644
--- a/src/kernel_services/abstract_interp/fval.ml
+++ b/src/kernel_services/abstract_interp/fval.ml
@@ -1196,10 +1196,10 @@ let fmod (FRange.I(b1, e1) as x) (FRange.I(b2, e2) as y) =
F.compare (F.max (abs_float b1) (abs_float e1))
(F.min (abs_float b2) (abs_float e2)) < 0 then (alarms, `Value x)
else
- (* 3. x and y are within the same continuos region.
+ (* 3. x and y are within the same continuous region.
(i.e. do not contain zero, do not cross any modulo boundaries, etc.)
Example: x=[6,7] and y=[4,5].
- Restriciton: [|x/y| < 2^53], otherwise truncation to an integer
+ Restriction: [|x/y| < 2^53], otherwise truncation to an integer
(to test the above property) may return an incorrect result.
Note: to avoid issues with rounding, we conservatively set the
limit to 2^51 instead of 2^53. *)
diff --git a/src/kernel_services/abstract_interp/fval.mli b/src/kernel_services/abstract_interp/fval.mli
index 99344356dc3..9c54ba11aa3 100644
--- a/src/kernel_services/abstract_interp/fval.mli
+++ b/src/kernel_services/abstract_interp/fval.mli
@@ -232,7 +232,7 @@ val diff : t -> t -> t Bottom.or_bottom
val backward_comp_left :
Comp.t -> bool -> float_kind -> t -> t -> t Bottom.or_bottom
-(** [backward_comp op allroundingmodes fkind f1 f2] attemps to reduce
+(** [backward_comp op allroundingmodes fkind f1 f2] attempts to reduce
[f1] into [f1'] so that the relation [f1' op f2] holds. [fkind] is
the type of [f1] and [f1'] (not necessarily of [f2]). If
[allroundingmodes] is set, all possible rounding modes are taken into
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index 784639c6336..68df66f7dff 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -100,7 +100,7 @@ type t =
| Float of Fval.t
| Top of Int.t option * Int.t option * Int.t * Int.t
(* Binary abstract operations do not model precisely float/integer operations.
- It is the responsability of the callers to have two operands of the same
+ It is the responsibility of the callers to have two operands of the same
implicit type. The only exception is for [singleton_zero], which is the
correct representation of [0.] *)
@@ -1612,7 +1612,7 @@ let largest_below max x = (* TODO: improve for Set *)
then Extlib.the mx
else Int.round_down_to_r ~max ~r ~modu
-(* Rounds up (x+1) to the next power of two, then substracts one; optimized. *)
+(* Rounds up (x+1) to the next power of two, then subtracts one; optimized. *)
let next_pred_power_of_two x =
(* Unroll the first iterations, and skip the tests. *)
let x = Int.logor x (Int.shift_right x Int.one) in
diff --git a/src/kernel_services/abstract_interp/lmap_sig.mli b/src/kernel_services/abstract_interp/lmap_sig.mli
index 5e5aff366b1..ce2d2440cc3 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/abstract_interp/locations.mli b/src/kernel_services/abstract_interp/locations.mli
index dc04b3f45d3..9b7858beeb8 100644
--- a/src/kernel_services/abstract_interp/locations.mli
+++ b/src/kernel_services/abstract_interp/locations.mli
@@ -44,7 +44,7 @@ module Location_Bytes : sig
type t =
| Top of Base.SetLattice.t * Origin.t
(** Garbled mix of the addresses in the set *)
- | Map of M.t (** Precice set of addresses+offsets *)
+ | Map of M.t (** Precise set of addresses+offsets *)
(** This type should be considered private *)
(* TODO: make it private when OCaml 4.01 is mandatory *)
@@ -96,7 +96,7 @@ module Location_Bytes : sig
val sub_pointwise: ?factor:Int_Base.t -> t -> t -> Ival.t
(** Subtracts the offsets of two locations [loc1] and [loc2].
- Returns the pointwise substraction of their offsets
+ Returns the pointwise subtraction of their offsets
[off1 - factor * off2]. [factor] defaults to [1]. *)
(** Topifying of values, in case of imprecise accesses *)
@@ -177,7 +177,7 @@ module Location_Bytes : sig
val contains_addresses_of_locals : (M.key -> bool) -> t -> bool
(** [contains_addresses_of_locals is_local loc] returns [true]
- if [loc] contains the adress of a variable for which
+ if [loc] contains the address of a variable for which
[is_local] returns [true] *)
val remove_escaping_locals : (M.key -> bool) -> t -> Base.SetLattice.t * t
@@ -187,7 +187,7 @@ module Location_Bytes : sig
val contains_addresses_of_any_locals : t -> bool
(** [contains_addresses_of_any_locals loc] returns [true] iff [loc] contains
- the adress of a local variable or of a formal variable. *)
+ the address of a local variable or of a formal variable. *)
(** {2 Misc} *)
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index de0c911c896..46cf3d735a9 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -108,7 +108,7 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
case it is sometimes necessary to return Empty. In the current
implementation, sizes 0 are handled by the outer (exported) functions,
while the inner functions assume that the arguments [size] are
- stricty positive. *)
+ strictly positive. *)
let equal (t1:V.t offsetmap) (t2:V.t offsetmap) = t1 == t2
@@ -1158,7 +1158,7 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
(** More efficient version of {!f_aux_merge_generic}, specialized for
join-like functions. When one of the values is isotropic, we do not
concretize the other one with {!extract_stitch_and_bits}. Instead,
- we implicitely "extend" the isotropic value to the full range,
+ we implicitly "extend" the isotropic value to the full range,
and merge on the whole range. This does not work with narrow, because
[narrow {0} {1,2}] on the first bit is {0}, but the intersection
of the two sets is bottom. *)
diff --git a/src/kernel_services/abstract_interp/origin.mli b/src/kernel_services/abstract_interp/origin.mli
index 8def04b816d..1549309d238 100644
--- a/src/kernel_services/abstract_interp/origin.mli
+++ b/src/kernel_services/abstract_interp/origin.mli
@@ -45,7 +45,7 @@ type origin =
| Merge of LocationSetLattice.t (** Join between two control-flows *)
| Arith of LocationSetLattice.t (** Arithmetic operation that cannot be
represented, eg. ['&x * 2'] *)
- | Well (** Imprecise variables of the intial state *)
+ | Well (** Imprecise variables of the initial state *)
| Unknown
include Datatype.S with type t = origin
diff --git a/src/kernel_services/analysis/dataflow.mli b/src/kernel_services/analysis/dataflow.mli
index 94250b4c744..802f0605e28 100644
--- a/src/kernel_services/analysis/dataflow.mli
+++ b/src/kernel_services/analysis/dataflow.mli
@@ -145,7 +145,7 @@ module type ForwardsTransfer = sig
would normally be put in the worklist. *)
val stmt_can_reach : Cil_types.stmt -> Cil_types.stmt -> bool
- (** Must return [true] if ther is a path in the control-flow graph of the
+ (** Must return [true] if there is a path in the control-flow graph of the
function from the first statement to the second. Used to choose a "good"
node in the worklist. Suggested use is [let stmt_can_reach =
Stmts_graph.stmt_can_reach kf], where [kf] is the kernel_function
@@ -225,7 +225,7 @@ module type BackwardsTransfer = sig
changed) *)
val stmt_can_reach : Cil_types.stmt -> Cil_types.stmt -> bool
- (** Must return [true] if ther is a path in the control-flow graph of the
+ (** Must return [true] if there is a path in the control-flow graph of the
function from the first statement to the second. Used to choose a "good"
node in the worklist.
diff --git a/src/kernel_services/analysis/dataflow2.ml b/src/kernel_services/analysis/dataflow2.ml
index 0d6eb24c5a9..4286d8ec203 100644
--- a/src/kernel_services/analysis/dataflow2.ml
+++ b/src/kernel_services/analysis/dataflow2.ml
@@ -70,7 +70,7 @@ module StartData(X: sig type t val size: int end) = struct
let length () = length stmtStartData
end
-(** Find which function we are analysing from the set of inital statements *)
+(** Find which function we are analysing from the set of initial statements *)
let current_kf = function
| [] -> assert false
| s :: q ->
diff --git a/src/kernel_services/analysis/dataflows.mli b/src/kernel_services/analysis/dataflows.mli
index efb675f9ca2..a9c785b5f64 100644
--- a/src/kernel_services/analysis/dataflows.mli
+++ b/src/kernel_services/analysis/dataflows.mli
@@ -44,7 +44,7 @@
(** Implementation of data flow analyses over user-supplied domains. *)
(* Instead of defining a single dataflow interface that tries to
- accomodate with all the options (as was done in {!Dataflow2}),
+ accommodate with all the options (as was done in {!Dataflow2}),
having a set of dataflows allow to keep things simple in the
general case; specific demands are handled by using more general
dataflows. Simpler-to-instanciate dataflows are instances of the
@@ -160,7 +160,7 @@ module type FORWARD_MONOTONE_PARAMETER = sig
Note that it is allowed that not all succs are present in the
list returned by [transfer_stmt] (in which case, the successor is
assumed to be unreachable in the current state), or that succs are
- present several times (this is useful to handle switchs).
+ present several times (this is useful to handle switches).
Helper functions are provided for [If] and [Switch] statements. See
{!transfer_if_from_guard} and {!transfer_switch_from_guard} below. *)
diff --git a/src/kernel_services/analysis/exn_flow.ml b/src/kernel_services/analysis/exn_flow.ml
index 7f10d0a9b27..a32c483244d 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 ec565ce287f..dfba0166100 100644
--- a/src/kernel_services/analysis/logic_interp.ml
+++ b/src/kernel_services/analysis/logic_interp.ml
@@ -551,12 +551,12 @@ struct
Varinfo.Set.empty
(** Term utility:
- Extract C local variables occuring into a [term]. *)
+ Extract C local variables occurring into a [term]. *)
let extract_locals_from_term term =
extract_locals (extract_free_logicvars_from_term term)
(** Predicate utility:
- Extract C local variables occuring into a [term]. *)
+ Extract C local variables occurring into a [term]. *)
let extract_locals_from_pred pred =
extract_locals (extract_free_logicvars_from_predicate pred)
@@ -635,16 +635,16 @@ struct
match ki_opt,before_opt with
(* function contract *)
| None,Some true ->
- failwith "The use of the label Old is forbiden inside clauses \
- related the pre-state of function contracts."
+ failwith "The use of the label Old is forbidden inside clauses \
+ related to the pre-state of function contracts."
| None,None
| None,Some false ->
(* refers to the pre-state of the contract. *)
self#change_label AbsLabel_pre x
(* statement contract *)
| Some (_ki,false),Some true ->
- failwith "The use of the label Old is forbiden inside clauses \
-related the pre-state of statement contracts."
+ failwith "The use of the label Old is forbidden inside clauses \
+related to the pre-state of statement contracts."
| Some (ki,false),None
| Some (ki,false),Some false ->
(* refers to the pre-state of the contract. *)
@@ -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,8 +696,8 @@ contracts."
match ki_opt with
(* function contract *)
| None ->
- failwith "the use of C labels is forbiden inside clauses related \
-function contracts."
+ failwith "the use of C labels is forbidden inside clauses related \
+to function contracts."
(* statement contract *)
(* code annotation *)
| Some _ ->
diff --git a/src/kernel_services/analysis/ordered_stmt.ml b/src/kernel_services/analysis/ordered_stmt.ml
index 7e59cd58de1..5911aef40cf 100644
--- a/src/kernel_services/analysis/ordered_stmt.ml
+++ b/src/kernel_services/analysis/ordered_stmt.ml
@@ -115,7 +115,7 @@ let to_ordered = Order.get
is global, there is no guarantee on the orders between statements
inside of a cycle.
- Furthermore, to make the dataflow propogation strategy more
+ Furthermore, to make the dataflow propagation strategy more
understandable, the topological sort should be stable with regards
to program order (i.e. the order between a and b may change only
when there is a path from a to b, and no path from b to a). For
diff --git a/src/kernel_services/analysis/wto_statement.mli b/src/kernel_services/analysis/wto_statement.mli
index 5bb4a58fe99..18abbb73b04 100644
--- a/src/kernel_services/analysis/wto_statement.mli
+++ b/src/kernel_services/analysis/wto_statement.mli
@@ -28,7 +28,7 @@ open Cil_types
(** A weak topological ordering where nodes are Cil statements *)
type wto = stmt Wto.partition
-(** The datatype for statment WTOs *)
+(** The datatype for statement WTOs *)
module WTO : Datatype.S with type t = wto
(** @return the computed wto for the given function *)
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index cdc4a7be0ce..6e1c769e6e2 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -96,7 +96,7 @@ type file = {
and global =
| GType of typeinfo * location
(** A typedef. All uses of type names (through the [TNamed] constructor)
- must be preceeded in the file by a definition of the name. The string
+ must be preceded in the file by a definition of the name. The string
is the defined name and always not-empty. *)
| GCompTag of compinfo * location
@@ -217,7 +217,7 @@ and typ =
| TNamed of typeinfo * attributes
(** The use of a named type. All uses of the same type name must share the
- typeinfo. Each such type name must be preceeded in the file by a [GType]
+ typeinfo. Each such type name must be preceded in the file by a [GType]
global. This is printed as just the type name. The actual referred type
is not printed here and is carried only to simplify processing. To see
through a sequence of named type references, use {!Cil.unrollType}. The
@@ -227,7 +227,7 @@ and typ =
| TComp of compinfo * bitsSizeofTypCache * attributes
(** A reference to a struct or a union type. All references to the
same struct or union must share the same compinfo among them and
- with a [GCompTag] global that preceeds all uses (except maybe
+ with a [GCompTag] global that precedes all uses (except maybe
those that are pointers to the composite type). The attributes
given are those pertaining to this use of the type and are in
addition to the attributes that were given at the definition of
@@ -236,7 +236,7 @@ and typ =
| TEnum of enuminfo * attributes
(** A reference to an enumeration type. All such references must
share the enuminfo among them and with a [GEnumTag] global that
- preceeds all uses. The attributes refer to this use of the
+ precedes all uses. The attributes refer to this use of the
enumeration and are in addition to the attributes of the
enumeration itself, which are stored inside the enuminfo *)
@@ -477,7 +477,7 @@ and typeinfo = {
mutable tname: string;
(** The name. Can be empty only in a [GType] when introducing a composite or
- enumeration tag. If empty cannot be refered to from the file *)
+ enumeration tag. If empty cannot be referred to from the file *)
mutable ttype: typ;
(** The actual type. This includes the attributes that were present in the
diff --git a/src/kernel_services/ast_data/globals.ml b/src/kernel_services/ast_data/globals.ml
index 174cd2b92dc..a96082ded5f 100644
--- a/src/kernel_services/ast_data/globals.ml
+++ b/src/kernel_services/ast_data/globals.ml
@@ -485,7 +485,7 @@ module FileIndex = struct
let get_symbols ~filename = snd (get_symbols ~filename)
(** get all global variables as (varinfo, initinfo) list with only one
- occurence of a varinfo *)
+ occurrence of a varinfo *)
let get_globals ~filename =
compute ();
let varinfo_set =
@@ -568,7 +568,7 @@ module Types = struct
module PairsExpTyp = Datatype.Pair(Cil_datatype.Exp)(Cil_datatype.Typ)
- (* Map from enum constant names to an expression containg the constant,
+ (* Map from enum constant names to an expression containing the constant,
and its type. *)
module Enums = State_builder.Hashtbl(Datatype.String.Hashtbl)(PairsExpTyp)
(struct
diff --git a/src/kernel_services/ast_data/globals.mli b/src/kernel_services/ast_data/globals.mli
index 93c42601757..9fbb52626ea 100644
--- a/src/kernel_services/ast_data/globals.mli
+++ b/src/kernel_services/ast_data/globals.mli
@@ -252,7 +252,7 @@ val get_comments_stmt: stmt -> string list
A comment is associated to a statement if it occurs after
the preceding statement and before the current statement ends (except for
- the last statement in a block, to which statements occuring before the end
+ the last statement in a block, to which statements occurring before the end
of the block are associated). Note that this function is experimental and
may fail to associate comments properly. Use directly
{! Cabshelper.Comments.get} to retrieve comments in a given region.
diff --git a/src/kernel_services/ast_data/property_status.mli b/src/kernel_services/ast_data/property_status.mli
index 9be494942f1..36d6ede6ec6 100644
--- a/src/kernel_services/ast_data/property_status.mli
+++ b/src/kernel_services/ast_data/property_status.mli
@@ -37,7 +37,7 @@
(* ************************************************************************ *)
(** Type of status emitted by analyzers. Each Property is attached to a program
- point [s] and implicitely depends on an execution path from the program
+ point [s] and implicitly depends on an execution path from the program
entry point to [s]. It also depends on an explicit set of hypotheses [H]
indicating when emitting the property (see function {!emit}). *)
type emitted_status =
@@ -69,8 +69,8 @@ val emit:
may be required is when emitting a status for a pre-condition of a function
[f] since the status associated to a pre-condition [p] merges all statuses
of [p] at each callsite of the function [f]. @return the kept status.
- @raise Inconsistent_emitted_status when emiting False after emiting True or
- conversely *)
+ @raise Inconsistent_emitted_status when emitting False after emitting True
+ or conversely *)
val emit_and_get:
Emitter.t -> hyps:Property.t list -> Property.t -> ?distinct:bool ->
@@ -100,7 +100,7 @@ type emitter_with_properties = private
{ emitter: Emitter.Usable_emitter.t;
mutable properties: Property.t list;
logical_consequence: bool (** Is the emitted status automatically
- infered? *) }
+ inferred? *) }
type inconsistent = private
{ valid: emitter_with_properties list;
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 94105af849d..22596985ebd 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1934,7 +1934,7 @@ class cil_printer () = object (self)
begin
(* __blockattribute__ is not standard, and is used only when
we are outputting something destined to Cil. Otherwise we
- ouput everything between comments. *)
+ output everything between comments. *)
let for_cil s = if state.print_cil_input then "" else s in
if block
then fprintf fmt " %s __blockattribute__(" (for_cil "/*")
diff --git a/src/kernel_services/ast_printing/printer_api.mli b/src/kernel_services/ast_printing/printer_api.mli
index 99a37c5a140..3eba911e6dd 100644
--- a/src/kernel_services/ast_printing/printer_api.mli
+++ b/src/kernel_services/ast_printing/printer_api.mli
@@ -115,12 +115,12 @@ class type extensible_printer_type = object
(** Invoked on each variable use. *)
method lval: Format.formatter -> lval -> unit
- (** Invoked on each lvalue occurence *)
+ (** Invoked on each lvalue occurrence *)
method field: Format.formatter -> fieldinfo -> unit
method offset: Format.formatter -> offset -> unit
- (** Invoked on each offset occurence. The second argument is the base. *)
+ (** Invoked on each offset occurrence. The second argument is the base. *)
method global: Format.formatter -> global -> unit
(** Global (vars, types, etc.). This can be slow. *)
@@ -142,7 +142,7 @@ class type extensible_printer_type = object
second argument must also have a value. *)
method attrparam: Format.formatter -> attrparam -> unit
- (** Attribute paramter *)
+ (** Attribute parameter *)
method attribute: Format.formatter -> attribute -> bool
(** Attribute. Also return an indication whether this attribute must be
diff --git a/src/kernel_services/ast_queries/ast_info.mli b/src/kernel_services/ast_queries/ast_info.mli
index 2b5280d9c81..a1500650ff6 100644
--- a/src/kernel_services/ast_queries/ast_info.mli
+++ b/src/kernel_services/ast_queries/ast_info.mli
@@ -70,7 +70,7 @@ val precondition : funspec -> predicate
@since Carbon-20101201 *)
val behavior_assumes : funbehavior -> predicate
- (** Builds the conjonction of the [b_assumes].
+ (** Builds the conjunction of the [b_assumes].
@since Nitrogen-20111001 *)
val behavior_precondition : funbehavior -> predicate
@@ -97,21 +97,21 @@ val merge_assigns_from_complete_bhvs:
contract.
- the list of sets of behavior names can come from the contract of the
related function.
- Optional [warn] argument can be used to force emmiting or cancelation of
+ Optional [warn] argument can be used to force emitting or cancelation of
warnings.
@since Oxygen-20120901 *)
val merge_assigns_from_spec: ?warn:bool -> funspec -> identified_term assigns
(** It is a shortcut for [merge_assigns_from_complete_bhvs
spec.spec_complete_behaviors spec.spec_behavior]. Optional [warn] argument
- can be used to force emmiting or cancelation of warnings
+ can be used to force emitting or cancelation of warnings
@return the assigns of an unguarded behavior or a set of complete behaviors.
@since Oxygen-20120901 *)
val merge_assigns: ?warn:bool -> funbehavior list -> identified_term assigns
(** Returns the assigns of an unguarded behavior.
@modify Oxygen-20120901 Optional [warn] argument added which can be used to
- force emmiting or cancelation of warnings. *)
+ force emitting or cancelation of warnings. *)
val variable_term: location -> logic_var -> term
val constant_term: location -> Integer.t -> term
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index bf664737eb5..6f12bce75e5 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -503,7 +503,7 @@ type attributeClass =
[ "section"; "constructor"; "destructor"; "unused"; "used"; "weak";
"no_instrument_function"; "alias"; "no_check_memory_usage";
"exception"; "model"; (* "restrict"; *)
- "aconst"; "__asm__" (* Gcc uses this to specifiy the name to be used in
+ "aconst"; "__asm__" (* Gcc uses this to specify the name to be used in
* assembly for a global *)];
(* Now come the MSVC declspec attributes *)
List.iter (fun a -> Hashtbl.add table a (AttrName true))
@@ -1679,12 +1679,12 @@ class type cilVisitor = object
* variable use *)
method vexpr: exp -> exp visitAction
- (** Invoked on each expression occurence. The subtrees are the
+ (** Invoked on each expression occurrence. The subtrees are the
* subexpressions, the types (for a [Cast] or [SizeOf] expression) or the
* variable use. *)
method vlval: lval -> lval visitAction
- (** Invoked on each lvalue occurence *)
+ (** Invoked on each lvalue occurrence *)
method voffs: offset -> offset visitAction
(** Invoked on each offset occurrence that is *not* as part
@@ -4344,12 +4344,12 @@ let isCharPtrType t =
and typeTermOffset basetyp =
let blendAttributes baseAttrs t =
- let (_, _, contageous) =
+ let (_, _, contagious) =
partitionAttributes ~default:(AttrName false) baseAttrs in
let putAttributes =
function
| Ctype typ ->
- Ctype (typeAddAttributes contageous typ)
+ Ctype (typeAddAttributes contagious typ)
| Linteger | Lreal ->
Kernel.fatal ~current:true
"typeTermOffset: Attribute on a logic type"
@@ -7134,7 +7134,7 @@ let initCIL ~initLogicBuiltins machdep =
let pullTypesForward = true
- (* Scan a type and collect the variables that are refered *)
+ (* Scan a type and collect the variables that are referred *)
class getVarsInGlobalClass (pacc: varinfo list ref) = object
inherit nopCilVisitor
method! vvrbl (vi: varinfo) =
@@ -7160,7 +7160,7 @@ let pushGlobal (g: global)
variables := g :: !variables
else
begin
- (* Collect a list of variables that are refered from the type. Return
+ (* Collect a list of variables that are referred from the type. Return
* Some if the global should go with the types and None if it should go
* to the variables. *)
let varsintype : (varinfo list * location) option =
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index f31e95df220..252fa060749 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -770,7 +770,7 @@ let keep_entry_point ?(specs=Kernel.Keep_unused_specified_functions.get ()) g =
let files_to_cabs_cil files =
Kernel.feedback ~level:2 "parsing";
(* Parsing and merging must occur in the very same order.
- Otherwise the order of files on the command line will not be consistantly
+ Otherwise the order of files on the command line will not be consistently
handled. *)
let cil_cabs = List.fold_left (fun acc f -> to_cil_cabs f :: acc) [] files in
let cil_files, cabs_files = List.split cil_cabs in
diff --git a/src/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli
index 72d8f3e877a..64604fd7f66 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 6475cf4d9de..8750429f5b8 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 e6b083a5362..29bb1b0327e 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -2095,7 +2095,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 =
@@ -3805,7 +3805,7 @@ let add_label info lab =
let p, env = formals loc env p in
check_polymorphism loc ?return_type:t p;
let info = Cil_const.make_logic_info f in
- (* Should we add implicitely a default label for the declaration? *)
+ (* Should we add implicitly a default label for the declaration? *)
let labels = match !Lenv.default_label with
None -> labels
| Some lab -> [lab]
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index 0c4ae9a37d5..9a5678bcf36 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -31,7 +31,7 @@ open Cil_types
*)
val type_rel: Logic_ptree.relation -> Cil_types.relation
-(** Arithmetic binop conversion. Addition and Substraction are always
+(** Arithmetic binop conversion. Addition and Subtraction are always
considered as being used on integers. It is the responsibility of the
user to introduce PlusPI/IndexPI, MinusPI and MinusPP where needed.
@since Nitrogen-20111001
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index ddea72a1814..ab07426893c 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -478,7 +478,7 @@ and loffset_contains_result o =
| TField(_,o) | TModel(_,o) -> loffset_contains_result o
| TIndex(t,o) -> contains_result t || loffset_contains_result o
-(** @return [true] if the underlying lval contains an occurence of
+(** @return [true] if the underlying lval contains an occurrence of
\result; [false] otherwise or if the term is not an lval. *)
and contains_result t =
match t.term_node with
@@ -2073,7 +2073,7 @@ let pointer_comparable ?loc t1 t2 =
this *)
mk_cast ~loc Cil.voidPtrType t, obj_ptr
| TVoid _ | TFun _ | TNamed _ | TComp _ | TBuiltin_va_list _
- | TArray _ (* in logic array do not decay implicitely
+ | TArray _ (* in logic array do not decay implicitly
into pointers. *)
->
Kernel.fatal
diff --git a/src/kernel_services/cmdline_parameters/parameter_builder.ml b/src/kernel_services/cmdline_parameters/parameter_builder.ml
index a6ad4722a8b..042adcfedfd 100644
--- a/src/kernel_services/cmdline_parameters/parameter_builder.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_builder.ml
@@ -1201,7 +1201,7 @@ now bound to '%a'.@]"
Treats :: as part of a word to be able to handle C++ function names
in a non too awkward manner.
*)
- let split_delim d = (* handle different possible lenght of the delimiter *)
+ let split_delim d = (* handle different possible length of the delimiter *)
let rbis = Str.regexp ":" in
match Str.bounded_full_split rbis d 2 with
| [ Str.Delim _] -> (empty_string, empty_string)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index ba8de9d6ceb..2ba894afcea 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -796,7 +796,7 @@ module Properties : sig
end
- (** Does the interpretation of the predicate rely on the intepretation
+ (** Does the interpretation of the predicate rely on the interpretation
of the term result?
@since Carbon-20110201 *)
val to_result_from_pred:
@@ -1022,9 +1022,9 @@ module Pdg : sig
val find_simple_stmt_nodes : (t -> Cil_types.stmt -> PdgTypes.Node.t list) ref
(** Get the nodes corresponding to the statement.
- It is usualy composed of only one node (see {!find_stmt_node}),
+ It is usually composed of only one node (see {!find_stmt_node}),
except for call statement.
- Be careful that for block statements, it only retuns a node
+ Be careful that for block statements, it only returns a node
corresponding to the elementary stmt
(see {!find_stmt_and_blocks_nodes} for more)
@raise Not_found if the given statement is unreachable.
@@ -1470,7 +1470,7 @@ module Slicing : sig
val compare : (t -> t -> int) ref
(** A total ordering function similar to the generic structural
comparison function [compare].
- Can be used to build a map from [t] marks to, for exemple, colors for
+ Can be used to build a map from [t] marks to, for example, colors for
the GUI. *)
val is_bottom : (t -> bool) ref
@@ -1660,7 +1660,7 @@ module Slicing : sig
propagate data_mark on data dependencies of the statement
- mark the node with a spare_mark and propagate so that
the dependencies that were not selected yet will be marked spare.
- When the statement is a call, its functionnal inputs/outputs are
+ When the statement is a call, its functional inputs/outputs are
also selected (The call is still selected even it has no output).
When the statement is a composed one (block, if, etc...),
all the sub-statements are selected.
@@ -1839,12 +1839,12 @@ module Slicing : sig
val add_slice_selection_internal:
(Project.t -> Slice.t -> Select.t -> unit) ref
- (** Internaly used to add a selection request for a function slice
+ (** Internally used to add a selection request for a function slice
to the project requests. *)
val add_selection_internal:
(Project.t -> Select.t -> unit) ref
- (** Internaly used to add a selection request to the project requests.
+ (** Internally used to add a selection request to the project requests.
This selection will be applied to every slicies of the function
(already existing or created later). *)
@@ -1867,16 +1867,16 @@ module Slicing : sig
(** {3 Internal use only} *)
val apply_all_internal: (Project.t -> unit) ref
- (** Internaly used to apply all slicing requests. *)
+ (** Internally used to apply all slicing requests. *)
val apply_next_internal: (Project.t -> unit) ref
- (** Internaly used to apply the first slicing request of the project list
+ (** Internally used to apply the first slicing request of the project list
and remove it from the list.
- That may modify the contents of the remaing list.
- For exemple, new requests may be added to the list. *)
+ That may modify the contents of the remaining list.
+ For example, new requests may be added to the list. *)
val is_request_empty_internal: (Project.t -> bool) ref
- (** Internaly used to know if internal requests are pending. *)
+ (** Internally used to know if internal requests are pending. *)
val merge_slices:
(Project.t -> Slice.t -> Slice.t -> replace:bool -> Slice.t) ref
@@ -1891,7 +1891,7 @@ module Slicing : sig
val copy_slice:
(Project.t -> Slice.t -> Slice.t) ref
(** Copy the input slice. The new slice is not called,
- * so it is the user responsability to change the calls if he wants to. *)
+ * so it is the user responsibility to change the calls if he wants to. *)
val split_slice:
(Project.t -> Slice.t -> Slice.t list) ref
diff --git a/src/kernel_services/plugin_entry_points/journal.mli b/src/kernel_services/plugin_entry_points/journal.mli
index 2e8ece882d4..6d4836bb32c 100644
--- a/src/kernel_services/plugin_entry_points/journal.mli
+++ b/src/kernel_services/plugin_entry_points/journal.mli
@@ -95,7 +95,7 @@ val write: unit -> unit
without clearing the journal. *)
val save: unit -> unit
- (** Save the current state of the journal for future restauration.
+ (** Save the current state of the journal for future restoration.
@since Beryllium-20090901 *)
val restore: unit -> unit
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index e49f11d6370..77900249ee9 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -1119,7 +1119,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/kernel_services/plugin_entry_points/log.ml b/src/kernel_services/plugin_entry_points/log.ml
index 9aab7e0bbab..08bf94274c2 100644
--- a/src/kernel_services/plugin_entry_points/log.ml
+++ b/src/kernel_services/plugin_entry_points/log.ml
@@ -776,7 +776,7 @@ struct
Do you think we can emulate all other features of Log but without
using c.buffer at all?
Everything but ensure_unique_newline seems feasible.
- See Design.make_slash to see a usefull example.
+ See Design.make_slash to see a useful example.
let start_of_line= Printf.sprintf "\n[%s] " P.label in
let length= pred (String.length start_of_line) in
diff --git a/src/kernel_services/plugin_entry_points/log.mli b/src/kernel_services/plugin_entry_points/log.mli
index 534c2cbd226..da896ca36a2 100644
--- a/src/kernel_services/plugin_entry_points/log.mli
+++ b/src/kernel_services/plugin_entry_points/log.mli
@@ -148,7 +148,7 @@ module type Messages = sig
@plugin development guide *)
val debug : ?level:int -> ?dkey:category -> 'a pretty_printer
- (** Debugging information dedicated to Plugin developpers.
+ (** Debugging information dedicated to Plugin developers.
Default level is 1. The debugging key is used in message headers.
See also [set_debug_keys] and [set_debug_keyset].
@since Beryllium-20090601-beta1
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index 8ab152a51ca..7ed1b8bd73b 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -448,7 +448,7 @@ struct
(* default kinds when none are specified *)
let default_kinds_str = "erw"
- (* all valid characters for specifing kinds *)
+ (* all valid characters for specifying kinds *)
let valid_kinds_str = "adefiruw"
(* [parse_kinds str] parses [str] to return a list of [kind]s. *)
diff --git a/src/libraries/stdlib/integer.mli b/src/libraries/stdlib/integer.mli
index 1f689e34fdd..9ee3e7cba12 100644
--- a/src/libraries/stdlib/integer.mli
+++ b/src/libraries/stdlib/integer.mli
@@ -38,9 +38,9 @@ val add : t -> t -> t
val sub : t -> t -> t
val mul : t -> t -> t
val native_div : t -> t -> t
-val rem : t -> t -> t (** Remainder of the Euclidian division (always positive) *)
+val rem : t -> t -> t (** Remainder of the Euclidean division (always positive) *)
val pos_div : t -> t -> t
-(** Euclidian division. Equivalent to C division if both operands are positive.
+(** Euclidean division. Equivalent to C division if both operands are positive.
Equivalent to a floored division if b > 0 (rounds downwards),
otherwise rounds upwards.
Note: it is possible that pos_div (-a) b <> pos_div a (-b). *)
@@ -88,7 +88,7 @@ val succ : t -> t
val pred : t -> t
val round_up_to_r : min:t -> r:t -> modu:t -> t
val round_down_to_r : max:t -> r:t -> modu:t -> t
-val pos_rem : t -> t -> t (** Remainder of the Euclidian division (always positive) *)
+val pos_rem : t -> t -> t (** Remainder of the Euclidean division (always positive) *)
val shift_left : t -> t -> t
val shift_right : t -> t -> t
val logand : t -> t -> t
@@ -105,7 +105,7 @@ val zero : t
val eight : t
val sixteen : t
val thirtytwo : t
-val div : t -> t -> t (** Euclidian division (that returns a positive rem) *)
+val div : t -> t -> t (** Euclidean division (that returns a positive rem) *)
val billion_one : t
val hash : t -> int
diff --git a/src/libraries/utils/bitvector.ml b/src/libraries/utils/bitvector.ml
index b2d786b0ded..3ebf43df12b 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/libraries/utils/pretty_utils.mli b/src/libraries/utils/pretty_utils.mli
index c24d61b4a52..24332ed0f24 100644
--- a/src/libraries/utils/pretty_utils.mli
+++ b/src/libraries/utils/pretty_utils.mli
@@ -87,7 +87,7 @@ val pp_iter:
'a formatter -> 'b formatter
(** pretty prints any structure using an iterator on it. The argument
[pre] (resp. [suf]) is output before (resp. after) the iterator
- is started (resp. has ended). The optional argument [sep] is output bewteen
+ is started (resp. has ended). The optional argument [sep] is output between
two calls to the ['a formatter]. Default: open a box for [pre], close
a box for [suf], nothing for [sep]. *)
@@ -97,7 +97,7 @@ val pp_iter2:
'key formatter -> 'v formatter -> 'a formatter
(** pretty prints any map-like structure using an iterator on it. The argument
[pre] (resp. [suf]) is output before (resp. after) the iterator
- is started (resp. has ended). The optional argument [sep] is output bewteen
+ is started (resp. has ended). The optional argument [sep] is output between
two calls to the ['a formatter]. The optional argument [between] is
output between the key and the value. Default: open a box for [pre], close
a box for [suf], nothing for [sep], break-space for [between]. *)
diff --git a/src/libraries/utils/rangemap.mli b/src/libraries/utils/rangemap.mli
index 359abc03b3d..5e43842d981 100644
--- a/src/libraries/utils/rangemap.mli
+++ b/src/libraries/utils/rangemap.mli
@@ -44,7 +44,7 @@
The implementation uses balanced binary trees, and therefore searching
and insertion take time logarithmic in the size of the map.
- Compared to Ocaml's standard libary, this implementation caches at
+ Compared to Ocaml's standard library, this implementation caches at
each node the hash of the tree (which is computed in an associative
manner), and contains some functions not yet present in the caml
implementation. *)
diff --git a/src/libraries/utils/rgmap.mli b/src/libraries/utils/rgmap.mli
index ec9bc821a4d..e7a2c251a33 100644
--- a/src/libraries/utils/rgmap.mli
+++ b/src/libraries/utils/rgmap.mli
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-(** Associative maps for _ranges_ to _values_ with overlaping.
+(** Associative maps for _ranges_ to _values_ with overlapping.
The maps register a collection of entries, and looks for all
entries containing some specified range. For instance, this data
diff --git a/src/libraries/utils/vector.mli b/src/libraries/utils/vector.mli
index 8aa15fa7929..371be219c43 100644
--- a/src/libraries/utils/vector.mli
+++ b/src/libraries/utils/vector.mli
@@ -38,8 +38,8 @@ val addi : 'a t -> 'a -> int (** Return index of added (last) element. *)
val clear : 'a t -> unit (** Do not modify actual capacity. *)
val iter : ('a -> unit) -> 'a t -> unit
val iteri : (int -> 'a -> unit) -> 'a t -> unit
-val map : ('a -> 'b) -> 'a t -> 'b t (** Result is shrinked. *)
-val mapi : (int -> 'a -> 'b) -> 'a t -> 'b t (** Result is shrinked. *)
+val map : ('a -> 'b) -> 'a t -> 'b t (** Result is shrunk. *)
+val mapi : (int -> 'a -> 'b) -> 'a t -> 'b t (** Result is shrunk. *)
val find : 'a t -> ?default:'a -> ?exn:exn -> int -> 'a
(** Default exception is [Not_found].
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index ef302dca7b2..359d12f4f69 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/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index 8b5a00e285a..0332a621393 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -1785,7 +1785,7 @@ type end_state = End_state.t
(** The data associated to each statement: We have a mapping from each
possible state at the entrance to the function (before actual transition)
- to the current state possibles, associated to any action that has occured
+ to the current state possibles, associated to any action that has occurred
on that path.
*)
module Case_state = Aorai_state.Map.Make(End_state)
diff --git a/src/plugins/aorai/utils_parser.ml b/src/plugins/aorai/utils_parser.ml
index 4f2475a33c2..70438cc8ab2 100644
--- a/src/plugins/aorai/utils_parser.ml
+++ b/src/plugins/aorai/utils_parser.ml
@@ -66,7 +66,7 @@ let get_new_offset my_host my_offset name=
let get_field_from_offset my_offset = begin
match my_offset with
| Cil_types.Field(fieldinfo,_) -> fieldinfo
- | _ -> Aorai_option.fatal "support only struct no array wtih struct"
+ | _ -> Aorai_option.fatal "support only struct no array with struct"
end in
let field_info = get_field_from_offset my_offset in
let last_field_offset = get_last_field field_info my_offset in
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index 6a70e2dea52..2f5430b62e3 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -225,8 +225,8 @@ struct
that refer to [v] (when [v] is not guaranteed to be always assigned, or
for padding in local structs), and that would need to be removed when v
goes out of scope. Moreover, semantically, [v] *is* assigned (albeit to
- "uninitalized", which represents an indefinite part of the stack). We
- do not attemps to track this "uninitalized" information in From, as this
+ "uninitialized", which represents an indefinite part of the stack). We
+ do not attempts to track this "uninitialized" information in From, as this
is redundant with the work done by Value -- hence the use of [\nothing].*)
let bind_locals m b =
let aux_local acc vi =
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index d23d7938289..5772ea04141 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -152,7 +152,7 @@ let filetree_selector
(* original_source callback unnecessary here *) ()) ();
main_ui#display_globals l
| Filetree.Global (GVarDecl (vi, _)) ->
- (* try to find a defintion instead of a declaration, which is more
+ (* try to find a definition instead of a declaration, which is more
informative. *)
main_ui#display_globals [Ast.def_or_last_decl vi]
| Filetree.Global g ->
@@ -602,7 +602,7 @@ class protected_menu_factory (host:Gtk_helper.host) (menu:GMenu.menu) = object
end
(* This function reacts to the section of a localizable. The [origin]
- arguments identifies the widget where the selection occured *)
+ arguments identifies the widget where the selection occurred *)
let selector_localizable (main_ui:main_window_extension_points) origin ~button localizable =
let popup_factory =
new protected_menu_factory (main_ui:>Gtk_helper.host) (GMenu.menu())
diff --git a/src/plugins/gui/design.mli b/src/plugins/gui/design.mli
index d971acb2566..42036e30c6a 100644
--- a/src/plugins/gui/design.mli
+++ b/src/plugins/gui/design.mli
@@ -202,7 +202,7 @@ class type main_window_extension_points = object
method protect :
cancelable:bool -> ?parent:GWindow.window_skel -> (unit -> unit) -> unit
- (** Lock the GUI ; run the funtion ; catch all exceptions ; Unlock GUI
+ (** Lock the GUI ; run the function ; catch all exceptions ; Unlock GUI
The parent window must be set if this method is not called directly
by the main window: it will ensure that error dialogs are transient
for the right window.
@@ -213,7 +213,7 @@ class type main_window_extension_points = object
method full_protect :
'a . cancelable:bool -> ?parent:GWindow.window_skel -> (unit -> 'a) ->
'a option
- (** Lock the GUI ; run the funtion ; catch all exceptions ; Unlock GUI ;
+ (** Lock the GUI ; run the function ; catch all exceptions ; Unlock GUI ;
returns [f ()].
The parent window must be set if this method is not called directly
by the main window: it will ensure that error dialogs are transient
diff --git a/src/plugins/gui/file_manager.ml b/src/plugins/gui/file_manager.ml
index e7b91d1b62c..95082fa5a74 100644
--- a/src/plugins/gui/file_manager.ml
+++ b/src/plugins/gui/file_manager.ml
@@ -55,7 +55,7 @@ let reparse (host_window: Design.main_window_extension_points) =
begin match old_helt, succeeded with
| None, _ -> (** no history available before reparsing *)
host_window#reset ()
- | _, None -> (** the user stopped or an error occured *)
+ | _, None -> (** the user stopped or an error occurred *)
host_window#reset ()
| Some old_helt, Some () ->
let new_helt = History.translate_history_elt old_helt in
diff --git a/src/plugins/gui/gtk_helper.mli b/src/plugins/gui/gtk_helper.mli
index 230adf06e26..13242edf0db 100644
--- a/src/plugins/gui/gtk_helper.mli
+++ b/src/plugins/gui/gtk_helper.mli
@@ -144,7 +144,7 @@ module Configuration: sig
val config_string : key:string -> default:string -> string #selector -> unit
val config_values : key:string -> default:'a ->
values:('a * string) list -> 'a #selector -> unit
- (** The [values] field is used as a dictionnary of available values.
+ (** The [values] field is used as a dictionary of available values.
They are compared with [Pervasives.(=)]. *)
end
diff --git a/src/plugins/gui/pretty_source.ml b/src/plugins/gui/pretty_source.ml
index 1943cf45768..c23397c31c5 100644
--- a/src/plugins/gui/pretty_source.ml
+++ b/src/plugins/gui/pretty_source.ml
@@ -248,7 +248,7 @@ struct
| ((pb,pe),Some v) -> ((pb,pe),v)
(* find the next loc in array starting at index i
- which satifies the predicate;
+ which satisfies the predicate;
raises Not_found if none exists *)
let find_next arr i predicate =
let rec fnext i =
diff --git a/src/plugins/gui/wpane.mli b/src/plugins/gui/wpane.mli
index 00fdaec1d84..c50c9466467 100644
--- a/src/plugins/gui/wpane.mli
+++ b/src/plugins/gui/wpane.mli
@@ -40,7 +40,7 @@ type field =
Fields take place in right column.
It is also possible to add widget that spans over the two columns.
- The form can be horizontaly devided into sections.
+ The form can be horizontally divided into sections.
Elements must be added in left-to-right, top-down order.
*)
diff --git a/src/plugins/impact/register_gui.ml b/src/plugins/impact/register_gui.ml
index e8c09eb3400..d02763693c0 100644
--- a/src/plugins/impact/register_gui.ml
+++ b/src/plugins/impact/register_gui.ml
@@ -384,7 +384,7 @@ let file_tree_decorate (file_tree:Filetree.t) =
| _ -> false
in
let id =
- (* lazyness of && is used for efficiency *)
+ (* laziness of && is used for efficiency *)
if Enabled.get () && SelectedStmt.get_option () <> None &&
List.exists is_hilighted globs then "gtk-apply"
else ""
diff --git a/src/plugins/inout/Inout.mli b/src/plugins/inout/Inout.mli
index 7fb6c1316dd..d5ced51e58c 100644
--- a/src/plugins/inout/Inout.mli
+++ b/src/plugins/inout/Inout.mli
@@ -25,7 +25,7 @@
(** Inputs-outputs computations. *)
(** No function is directly exported: they are registered in:
- - {!Db.Inputs} for computations of non functionnal inputs;
+ - {!Db.Inputs} for computations of non functional inputs;
- {!Db.Outputs} for computations of outputs;
- {!Db.Operational_inputs} for computation of inout context; and
- {!Db.Derefs}. *)
diff --git a/src/plugins/inout/cumulative_analysis.mli b/src/plugins/inout/cumulative_analysis.mli
index c7e42460bd8..0d905d5dbd1 100644
--- a/src/plugins/inout/cumulative_analysis.mli
+++ b/src/plugins/inout/cumulative_analysis.mli
@@ -124,7 +124,7 @@ sig
(** Effects of a statement, using memoization if it contains a function call*)
val statement: stmt -> X.t
- (** Effects of the given expression (wich is supposed to be at the given
+ (** Effects of the given expression (which is supposed to be at the given
statement *)
val expr: stmt -> exp -> X.t
end
diff --git a/src/plugins/metrics/metrics_cabs.ml b/src/plugins/metrics/metrics_cabs.ml
index 7184a81cbb2..98bbe0861b3 100644
--- a/src/plugins/metrics/metrics_cabs.ml
+++ b/src/plugins/metrics/metrics_cabs.ml
@@ -37,7 +37,7 @@ class metricsCabsVisitor = object(self)
val was_case = ref false
(* Local metrics are kept stored after computation in this map of maps.
- Its storing hierachy is as follows: filename -> function_name -> metrics *)
+ Its storing hierarchy is as follows: filename -> function_name -> metrics *)
val mutable metrics_map:
(BasicMetrics.t Datatype.String.Map.t) Datatype.String.Map.t =
Datatype.String.Map.empty
diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml
index 4b91d0bbe4a..754c4e59219 100644
--- a/src/plugins/metrics/metrics_cilast.ml
+++ b/src/plugins/metrics/metrics_cilast.ml
@@ -78,7 +78,7 @@ class slocVisitor ~libc : sloc_visitor = object(self)
val local_metrics = ref BasicMetrics.empty_metrics
(* Local metrics are kept stored after computation in this map of maps.
- Its storing hierachy is as follows: filename -> function_name -> metrics
+ Its storing hierarchy is as follows: filename -> function_name -> metrics
*)
val mutable metrics_map:
(BasicMetrics.t Datatype.String.Map.t) Datatype.String.Map.t =
diff --git a/src/plugins/occurrence/Occurrence.mli b/src/plugins/occurrence/Occurrence.mli
index 2873122dd08..a1668782a02 100644
--- a/src/plugins/occurrence/Occurrence.mli
+++ b/src/plugins/occurrence/Occurrence.mli
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-(** Occurence plug-in. *)
+(** Occurrence plug-in. *)
(** No function is directly exported: they are registered in
{!Db.Occurrence}. *)
diff --git a/src/plugins/occurrence/register.ml b/src/plugins/occurrence/register.ml
index 9318acb0338..51ca7dfe618 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/pdg/annot.mli b/src/plugins/pdg/annot.mli
index 7556c0ceb5d..0c5d9fbddb9 100644
--- a/src/plugins/pdg/annot.mli
+++ b/src/plugins/pdg/annot.mli
@@ -34,7 +34,7 @@ type data_info =
((PdgTypes.Node.t * Locations.Zone.t option) list
* Locations.Zone.t option) option
-(** [ctrl_info] correspond to control dependancies nodes *)
+(** [ctrl_info] correspond to control dependencies nodes *)
type ctrl_info = PdgTypes.Node.t list
(** [decl_info] correspond to the declarations nodes of the variables needed to
diff --git a/src/plugins/pdg/pdg_state.ml b/src/plugins/pdg/pdg_state.ml
index d2425ff8ead..2d7bd3c0b44 100644
--- a/src/plugins/pdg/pdg_state.ml
+++ b/src/plugins/pdg/pdg_state.ml
@@ -21,7 +21,7 @@
(**************************************************************************)
(** DataState is associated with a program point
- and provide the dependancies for the data,
+ and provide the dependencies for the data,
ie. it stores for each location the nodes of the pdg where its value
was last defined.
*)
diff --git a/src/plugins/pdg_types/pdgTypes.ml b/src/plugins/pdg_types/pdgTypes.ml
index 302d5216088..d4298f06f06 100644
--- a/src/plugins/pdg_types/pdgTypes.ml
+++ b/src/plugins/pdg_types/pdgTypes.ml
@@ -401,7 +401,7 @@ module G = struct
end
(** DataState is associated with a program point
- and provide the dependancies for the data,
+ and provide the dependencies for the data,
ie. it stores for each location the nodes of the pdg where its value
was last defined.
Managed in src/pdg/state.ml
diff --git a/src/plugins/print_api/print_interface.ml b/src/plugins/print_api/print_interface.ml
index 1c011684e16..71bf44c56c7 100644
--- a/src/plugins/print_api/print_interface.ml
+++ b/src/plugins/print_api/print_interface.ml
@@ -68,7 +68,7 @@ let clash_with_compilation_unit =
module Module_deps = Graph.Imperative.Digraph.Concrete(Datatype.String)
let module_deps = Module_deps.create ()
-(** Comments are registered appart in the module Dynamic *)
+(** Comments are registered apart in the module Dynamic *)
module Comment: sig
val add: string -> string -> unit
val find: string -> string
@@ -233,7 +233,7 @@ let fill_tbl key typ _ =
(** It replaces the sub-strings "Plugin.type" of all the string [type_string]
used in the module named "Plugin" by "type".
- It also removes the option stucture (e.g. "~gid:string" is replaced by
+ It also removes the option structure (e.g. "~gid:string" is replaced by
"string"). *)
let repair_type module_name type_string =
let rec remove_param_name s =
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index c803fbda055..682c55293e6 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -494,7 +494,7 @@ class annot_visitor kf to_annot on_alarm = object (self)
None
| assigns ->
(* Case 1.2: that assigns will be used as default assigns later.
- note: a message has been emmited. *)
+ note: a message has been emitted. *)
Some assigns)
| _ -> (* Case 2: no special thing to do *)
None)
@@ -505,7 +505,7 @@ class annot_visitor kf to_annot on_alarm = object (self)
let new_bhvs =
List.fold_left
(fun acc bhv ->
- (* step 1: looking for managment of allocation and assigns
+ (* step 1: looking for management of allocation and assigns
clause. *)
let allocation =
fun_transform_allocations bhv.b_allocation
diff --git a/src/plugins/security_slicing/components.ml b/src/plugins/security_slicing/components.ml
index c88c434d3a1..88e7c23c8ec 100644
--- a/src/plugins/security_slicing/components.ml
+++ b/src/plugins/security_slicing/components.ml
@@ -595,7 +595,7 @@ Ignoring this function in the analysis (potentially incorrect results)."
pdg from_stmt stmt called_pdg
with
| Db.Pdg.Top ->
- (* warning already emited in the previous fold *)
+ (* warning already emitted in the previous fold *)
[]
| Db.Pdg.Bottom | Not_found -> assert false
in
diff --git a/src/plugins/slicing/fct_slice.ml b/src/plugins/slicing/fct_slice.ml
index 741676045eb..0e7cc8863a0 100644
--- a/src/plugins/slicing/fct_slice.ml
+++ b/src/plugins/slicing/fct_slice.ml
@@ -34,7 +34,7 @@
* so they can return a list of actions to be applied in order to deal with
* the propagation in the calls and callers.
*
- * Moreover, some function (named [get_xxx_mark]) are provided to retreive
+ * Moreover, some function (named [get_xxx_mark]) are provided to retrieve
* the mark of the slice elements.
* *)
diff --git a/src/plugins/slicing/register.ml b/src/plugins/slicing/register.ml
index 2da6ca3c467..fb051e65de0 100644
--- a/src/plugins/slicing/register.ml
+++ b/src/plugins/slicing/register.ml
@@ -502,7 +502,7 @@ let print_extracted_project ?fmt ~extracted_prj =
if SlicingParameters.Print.get () then
FC_file.pretty_ast ?fmt ~prj:extracted_prj ()
-(** Global data managment *)
+(** Global data management *)
module P =
State_builder.Ref
diff --git a/src/plugins/slicing/slicingCmds.ml b/src/plugins/slicing/slicingCmds.ml
index 7e89c6f1207..b74fe55619d 100644
--- a/src/plugins/slicing/slicingCmds.ml
+++ b/src/plugins/slicing/slicingCmds.ml
@@ -74,13 +74,13 @@ struct
in
ignore (visitCilFunction (visitor:>cilVisitor) definition)
- (** Get directly read/writen [Zone.t] by the statement.
+ (** Get directly read/written [Zone.t] by the statement.
* i.e. directly means when [ki] is a call,
it doesn't don't look at the assigns clause of the called function. *)
- let get_rw_zone stmt = (* returns [Zone.t read],[Zone.t writen] *)
+ let get_rw_zone stmt = (* returns [Zone.t read],[Zone.t written] *)
assert (Db.Value.is_computed ());
let lval_process read_zone stmt lv =
- (* returns [read_zone] joined to [Zone.t read] by [lv], [Zone.t writen] by [lv] *)
+ (* returns [read_zone] joined to [Zone.t read] by [lv], [Zone.t written] by [lv] *)
(* The modified locationss are [looking_for], those address are
function of [deps]. *)
let state = Db.Value.get_stmt_state stmt in
@@ -95,11 +95,11 @@ struct
(* returns [Zone.t read] by condition [exp], [Zone.bottom] *)
!Db.From.find_deps_no_transitivity stmt exp, Locations.Zone.bottom
| Instr (Set (lv,exp,_)) ->
- (* returns [Zone.t read] by [exp, lv], [Zone.t writen] by [lv] *)
+ (* returns [Zone.t read] by [exp, lv], [Zone.t written] by [lv] *)
let read_zone = !Db.From.find_deps_no_transitivity stmt exp in
lval_process read_zone stmt lv
| Instr (Call (lvaloption,funcexp,argl,_)) ->
- (* returns [Zone.t read] by [lvaloption, funcexp, argl], [Zone.t writen] by [lvaloption] *)
+ (* returns [Zone.t read] by [lvaloption, funcexp, argl], [Zone.t written] by [lvaloption] *)
let read_zone = !Db.From.find_deps_no_transitivity stmt funcexp in
let add_args arg inputs =
Locations.Zone.join inputs (!Db.From.find_deps_no_transitivity stmt arg) in
@@ -112,7 +112,7 @@ struct
| _ -> Locations.Zone.bottom, Locations.Zone.bottom
(** Look at intersection of [rd_zone_opt]/[wr_zone_opt] with the
- directly read/writen [Zone.t] by the statement.
+ directly read/written [Zone.t] by the statement.
* i.e. directly means when [ki] is a call,
it doesn't don't look at the assigns clause of the called function. *)
let is_rw_zone (rd_zone_opt, wr_zone_opt) stmt =
diff --git a/src/plugins/slicing/slicingTransform.ml b/src/plugins/slicing/slicingTransform.ml
index 6a401cac603..ec2f9e3fba8 100644
--- a/src/plugins/slicing/slicingTransform.ml
+++ b/src/plugins/slicing/slicingTransform.ml
@@ -210,7 +210,7 @@ module Visibility (SliceName : sig
(* work-around to avoid outputting annotations with type errors:
in case we end up with NotImplemented somewhere, we keep the annotation
- iff all C variables occuring in there are visible.
+ iff all C variables occurring in there are visible.
*)
let all_logic_var_visible, all_logic_var_visible_identified_term, all_logic_var_visible_term,
all_logic_var_visible_assigns, all_logic_var_visible_deps =
diff --git a/src/plugins/slicing_types/slicingInternals.ml b/src/plugins/slicing_types/slicingInternals.ml
index f72a78b9261..986a4ccca31 100644
--- a/src/plugins/slicing_types/slicingInternals.ml
+++ b/src/plugins/slicing_types/slicingInternals.ml
@@ -78,7 +78,7 @@ type fct_info = {
fi_def : Cil_types.fundec option;
fi_project : project;
mutable fi_top : pdg_mark option;
- (** indicates if the function is maked top (=> src visible) *)
+ (** indicates if the function is marked top (=> src visible) *)
mutable fi_level_option : level_option;
(** level of specialisation for this function *)
mutable fi_init_marks : ff_marks option;
diff --git a/src/plugins/sparecode/globs.ml b/src/plugins/sparecode/globs.ml
index 906499e38ce..51046be16b7 100644
--- a/src/plugins/sparecode/globs.ml
+++ b/src/plugins/sparecode/globs.ml
@@ -47,7 +47,7 @@ class collect_visitor = object (self)
method! vtype t = match t with
| TNamed(ti,_) ->
- (* we use the type name because directe typeinfo comparision
+ (* we use the type name because directe typeinfo comparison
* doesn't wok. Anyway, CIL renames types if several type have the same
* name... *)
if Hashtbl.mem used_typeinfo ti.tname then SkipChildren
diff --git a/src/plugins/sparecode/spare_marks.ml b/src/plugins/sparecode/spare_marks.ml
index 9ba8cdf53a7..3f21edc91cd 100644
--- a/src/plugins/sparecode/spare_marks.ml
+++ b/src/plugins/sparecode/spare_marks.ml
@@ -26,7 +26,7 @@ let fatal fmt = Sparecode_params.fatal fmt
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
(** The project is composed of [FctIndex] marked with [BoolMark]
* to be used by [Pdg.Register.F_Proj], and another table to store if a function
-* is visible (usefull for Top PDG). *)
+* is visible (useful for Top PDG). *)
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
module BoolMark = struct
diff --git a/src/plugins/value/alarmset.ml b/src/plugins/value/alarmset.ml
index 14a6350c632..7cf97e63760 100644
--- a/src/plugins/value/alarmset.ml
+++ b/src/plugins/value/alarmset.ml
@@ -243,7 +243,7 @@ let current_stmt () =
with Stack.Empty -> assert false
let sc_kinstr_loc ki = match ki with
- | Cil_types.Kglobal -> (* can occur in case of obscure bugs (already happended)
+ | Cil_types.Kglobal -> (* can occur in case of obscure bugs (already happened)
with wacky initializers. Module Initial_state of
value analysis correctly positions the loc *)
assert (Cil_datatype.Kinstr.equal Cil_types.Kglobal (current_stmt ()));
diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index 2fdec90925b..8dbc26fef07 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -68,7 +68,7 @@
{!S_with_Structure} is the interface to implement in order to introduce
a now domain in EVA.
- The module type {!Internal} contains some other functionnalities needed by
+ The module type {!Internal} contains some other functionalities needed by
the analyzer, but that can be automatically generated from the previous
one. The functor {!Domain_builder.Complete} produces an {!Internal} module
from a {!S_with_Structure} one.
diff --git a/src/plugins/value/domains/apron/apron_domain.ok.ml b/src/plugins/value/domains/apron/apron_domain.ok.ml
index e7e38558e41..ccf717c1a86 100644
--- a/src/plugins/value/domains/apron/apron_domain.ok.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ok.ml
@@ -141,7 +141,7 @@ let expr_fits_in_range (expr: Apron.Texpr1.expr) range =
false (* TODO? Unclear whether those cases would add expressivity. *)
(* Auxiliary function for {!coerce} below. It normalizes [expr] in an expression
- that is guaranteed to fit withing the integer type [range], or returns
+ that is guaranteed to fit within the integer type [range], or returns
an interval covering the entire range.
Algorithm from Verasco.
See section 6.5 of the paper 'A Formally-Verified C Static Analyzer'. *)
diff --git a/src/plugins/value/domains/cvalue/builtins_malloc.ml b/src/plugins/value/domains/cvalue/builtins_malloc.ml
index 1acb4a1f755..935bdbda827 100644
--- a/src/plugins/value/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/value/domains/cvalue/builtins_malloc.ml
@@ -243,7 +243,7 @@ let add_uninitialized state base max_valid_bits =
try
let cur = match Model.find_base_or_default base state with
| `Top -> assert false (* Value nevers passes Top as state *)
- | `Bottom -> assert false (* implicitely checked by offsm_with_uninit *)
+ | `Bottom -> assert false (* implicitly checked by offsm_with_uninit *)
| `Value m -> m
in
V_Offsetmap.join offsm cur
@@ -543,7 +543,7 @@ let realloc_alloc_copy loc weak bases_to_realloc null_in_arg sizev state =
let offsm =
if null_in_arg then offsm (* In this case, realloc may copy nothing *)
else
- (* Compute the maximal size that is guaranteed to be copied accross all
+ (* Compute the maximal size that is guaranteed to be copied across all
bases *)
let aux_valid size b = Integer.min size (size_sure_valid b) in
let size_new_loc = Integer.mul size_max (Bit_utils.sizeofchar ()) in
diff --git a/src/plugins/value/domains/cvalue/builtins_string.mli b/src/plugins/value/domains/cvalue/builtins_string.mli
index 167b4935e59..81820624a5c 100644
--- a/src/plugins/value/domains/cvalue/builtins_string.mli
+++ b/src/plugins/value/domains/cvalue/builtins_string.mli
@@ -22,7 +22,7 @@
(** Value builtins related to functions in string.h. *)
-(** The actual builtins are registed through {!Builtins.register_builtin}.
+(** The actual builtins are registered through {!Builtins.register_builtin}.
The functions below are also used for the evaluation of logical predicates
[valid_string] and [valid_read_string]. *)
diff --git a/src/plugins/value/domains/cvalue/cvalue_init.ml b/src/plugins/value/domains/cvalue/cvalue_init.ml
index 6ddddd7f901..cc23fb671f1 100644
--- a/src/plugins/value/domains/cvalue/cvalue_init.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_init.ml
@@ -300,7 +300,7 @@ let initialize_var_using_type varinfo state =
Value_parameters.result ~once:true ~current:true
"no size specified for array, assuming 0";
(* This is either a flexible array member (for which Cil
- implicitely returns a size of 0, so we are doing the proper
+ implicitly returns a size of 0, so we are doing the proper
thing), or an incomplete array (which is forbidden) *)
state
| Cil.SizeOfError (s, t) ->
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index c3002047c85..e44efc0af9c 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -152,7 +152,7 @@ module G = struct
let zero = Some Integer.zero, Some Integer.zero
(* Widening between two bounds. Unstable bounds are widened to infty
- agressively. This widening does not assumes that [is_included i1 i2]
+ aggressively. This widening does not assumes that [is_included i1 i2]
holds, unlike the widening of Ival. *)
let widen ?threshold (min1, max1: t) (min2, max2: t) : t =
let widen_unstable_min b1 b2 =
@@ -351,7 +351,7 @@ module G = struct
(* This function takes two mv, and 'subtracts' them for the [inc]
operation of gauges. More precisely, for each base present in both maps,
- we substract pointwise the min and max or their possible values.
+ we subtract pointwise the min and max or their possible values.
This is used to compute the 'difference' during one loop iteration. *)
let sub_mv =
let cache = cache_name "sub_mv" in
@@ -563,7 +563,7 @@ module G = struct
let join_same_lambda =
let cache = cache_name "join_same_lambda" in
let decide _ v1 v2 =
- (* Forbid muliple pointers in the result *)
+ (* Forbid multiple pointers in the result *)
try
let b1, _i1 = Cvalue.V.find_lonely_key v1 in
let b2, _i2 = Cvalue.V.find_lonely_key v2 in
@@ -1078,7 +1078,7 @@ module D_Impl : Abstract_domain.S_with_Structure
List.fold_left remove_variable state vars
let leave_scope _kf vars state =
- (* reverts implicity to Top *)
+ (* reverts implicitly to Top *)
remove_variables vars state
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index 080604ebf04..cbdb3aa5167 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -387,7 +387,7 @@ module Internal : Domain_builder.InputDomain
let enter_scope _kf _vars state = state
let leave_scope _kf vars state =
- (* removed variables revert implicity to Top *)
+ (* removed variables revert implicitly to Top *)
Memory.remove_variables vars state
let top_return = { v = `Value V.top; initialized = false; escaping = true }
diff --git a/src/plugins/value/engine/abstractions.mli b/src/plugins/value/engine/abstractions.mli
index bfa21ba5415..2c883ecf25a 100644
--- a/src/plugins/value/engine/abstractions.mli
+++ b/src/plugins/value/engine/abstractions.mli
@@ -43,7 +43,7 @@ val default_config : config
May be the default config as well. *)
val legacy_config : config
-(** Build a configuration according to the analysis paramaters. *)
+(** Build a configuration according to the analysis parameters. *)
val configure : unit -> config
diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml
index 1d3742fce2f..a9d4e5f059d 100644
--- a/src/plugins/value/engine/evaluation.ml
+++ b/src/plugins/value/engine/evaluation.ml
@@ -177,7 +177,7 @@ let return t = `Value t, Alarmset.none
(* Intersects [alarms] with the only possible alarms from the dereference of
the left-value [lval] of type [typ].
- Usefull if the abstract domain returns a non-closed AllBut alarmset for
+ Useful if the abstract domain returns a non-closed AllBut alarmset for
some lvalues. *)
let close_dereference_alarms lval typ alarms =
let init_alarm = Alarms.Uninitialized lval
diff --git a/src/plugins/value/engine/initialization.ml b/src/plugins/value/engine/initialization.ml
index 69e969c8029..ce819f841bb 100644
--- a/src/plugins/value/engine/initialization.ml
+++ b/src/plugins/value/engine/initialization.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-(* Creation of the inital state of abstract domain. *)
+(* Creation of the initial state of abstract domain. *)
open Cil_types
open Eval
diff --git a/src/plugins/value/engine/initialization.mli b/src/plugins/value/engine/initialization.mli
index 9caee205a6e..c0f0c187e51 100644
--- a/src/plugins/value/engine/initialization.mli
+++ b/src/plugins/value/engine/initialization.mli
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-(** Creation of the inital state of abstract domain. *)
+(** Creation of the initial state of abstract domain. *)
open Cil_types
open Bottom.Type
diff --git a/src/plugins/value/engine/non_linear_evaluation.ml b/src/plugins/value/engine/non_linear_evaluation.ml
index f86cbb04baa..372898fac1b 100644
--- a/src/plugins/value/engine/non_linear_evaluation.ml
+++ b/src/plugins/value/engine/non_linear_evaluation.ml
@@ -334,7 +334,7 @@ module Make
(* Subdivision of the evaluation of the expression [expr], according to the
lvalue [lval], in the state [state].
- [subexpr] is the smallest subexpression of [expr] containing all occurences
+ [subexpr] is the smallest subexpression of [expr] containing all occurrences
of the lvalue [lval]. It is thus its value that needs to be reduced.
However, we perform the complete evaluation of [expr] to be able to remove
the values of [lval] that lead to Bottom.
diff --git a/src/plugins/value/eval.ml b/src/plugins/value/eval.ml
index 3358510d4e9..0d9780fde03 100644
--- a/src/plugins/value/eval.ml
+++ b/src/plugins/value/eval.ml
@@ -232,7 +232,7 @@ type ('state, 'return, 'value) return_state = {
type ('state, 'return, 'value) call_result =
('state, 'return, 'value) return_state list or_bottom
-(* Initialization of a dataflow analysis, by definig the initial value of
+(* Initialization of a dataflow analysis, by defining the initial value of
each statement. *)
type 't init =
| Default
diff --git a/src/plugins/value/eval.mli b/src/plugins/value/eval.mli
index f2d5e132ad2..3e2d03c72e1 100644
--- a/src/plugins/value/eval.mli
+++ b/src/plugins/value/eval.mli
@@ -221,7 +221,7 @@ type ('state, 'return, 'value) return_state = {
type ('state, 'return, 'value) call_result =
('state, 'return, 'value) return_state list or_bottom
-(** Initialization of a dataflow analysis, by definig the initial value of
+(** Initialization of a dataflow analysis, by defining the initial value of
each statement. *)
type 't init =
| Default
diff --git a/src/plugins/value/gui_files/register_gui.ml b/src/plugins/value/gui_files/register_gui.ml
index 7d1e2c92604..f45ff944dd7 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/legacy/eval_annots.ml b/src/plugins/value/legacy/eval_annots.ml
index 3760fd834d4..dc58de3cafc 100644
--- a/src/plugins/value/legacy/eval_annots.ml
+++ b/src/plugins/value/legacy/eval_annots.ml
@@ -682,7 +682,7 @@ let mark_unreachable () =
(match Kernel_function.get_called e with
| Some kf ->
(* Do not put "unreachable" statuses on preconditions of
- functions overriden by builtins. We do not evaluate those
+ functions overridden by builtins. We do not evaluate those
preconditions on reachable calls, and the consolidation
gives very bad results when reachable and unrechable calls
coexist (untried+dead -> unknown). *)
diff --git a/src/plugins/value/legacy/eval_exprs.ml b/src/plugins/value/legacy/eval_exprs.ml
index e3c743d9729..81f91d69fb8 100644
--- a/src/plugins/value/legacy/eval_exprs.ml
+++ b/src/plugins/value/legacy/eval_exprs.ml
@@ -1072,7 +1072,7 @@ let reduce_by_cond state cond =
in
let result = aux cond state in
(* If the condition does not evaluate exactly to true (or false if [cond] is
- negative), we reduce more agressively by splitting on some variables *)
+ negative), we reduce more aggressively by splitting on some variables *)
let evaled = eval_expr ~with_alarms:CilE.warn_none_mode result cond.exp in
let reduce_more =
if cond.positive
diff --git a/src/plugins/value/legacy/eval_op.ml b/src/plugins/value/legacy/eval_op.ml
index e57109da56c..b713a7c19be 100644
--- a/src/plugins/value/legacy/eval_op.ml
+++ b/src/plugins/value/legacy/eval_op.ml
@@ -282,7 +282,7 @@ let eval_binop_int ~with_alarms ~te1 ev1 op ev2 =
| Shiftrt -> V.shift_right ev1 ev2
| Shiftlt -> V.shift_left ev1 ev2
(* Strict evaluation. The caller of this function is supposed to take
- into account the lazyness of those operators itself *)
+ into account the laziness of those operators itself *)
| LOr -> V.interp_boolean
~contains_zero:(V.contains_zero ev1 && V.contains_zero ev2)
~contains_non_zero:(V.contains_non_zero ev1 || V.contains_non_zero ev2)
diff --git a/src/plugins/value/legacy/initial_state.ml b/src/plugins/value/legacy/initial_state.ml
index 1b3c75505f3..f8de88297a3 100644
--- a/src/plugins/value/legacy/initial_state.ml
+++ b/src/plugins/value/legacy/initial_state.ml
@@ -301,7 +301,7 @@ let initialize_var_using_type varinfo state =
Value_parameters.result ~once:true ~current:true
"no size specified for array, assuming 0";
(* This is either a flexible array member (for which Cil
- implicitely returns a size of 0, so we are doing the proper
+ implicitly returns a size of 0, so we are doing the proper
thing), or an incomplete array (which is forbidden) *)
state
| Cil.SizeOfError (s, t) ->
diff --git a/src/plugins/value/legacy/valarms.ml b/src/plugins/value/legacy/valarms.ml
index 61c3ed903e5..c0364d7eb99 100644
--- a/src/plugins/value/legacy/valarms.ml
+++ b/src/plugins/value/legacy/valarms.ml
@@ -95,7 +95,7 @@ let get_syntactic_context () = current_stmt (),!syntactic_context
let sc_kinstr_loc ki =
match ki with
- | Kglobal -> (* can occur in case of obscure bugs (already happended)
+ | Kglobal -> (* can occur in case of obscure bugs (already happened)
with wacky initializers. Module Initial_state of
value analysis correctly positions the loc *)
assert (Cil_datatype.Kinstr.equal Kglobal
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 8be2acc73c8..149da154881 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -443,7 +443,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/values/cvalue_forward.ml b/src/plugins/value/values/cvalue_forward.ml
index e734154add3..7ee78ca1875 100644
--- a/src/plugins/value/values/cvalue_forward.ml
+++ b/src/plugins/value/values/cvalue_forward.ml
@@ -26,7 +26,7 @@ open Cil_types
let return v = v, Alarmset.none
(* --------------------------------------------------------------------------
- Comparision
+ Comparison
-------------------------------------------------------------------------- *)
(* Literal strings can only be compared if their contents are recognizably
@@ -344,7 +344,7 @@ let forward_binop_unbounded_integer ~context ~typ ev1 op ev2 =
let signed = Bit_utils.is_signed_int_enum_pointer typ in
return (V.bitwise_and ~size ~signed ev1 ev2)
(* Strict evaluation. The caller of this function is supposed to take
- into account the lazyness of those operators itself *)
+ into account the laziness of those operators itself *)
| LOr -> return (
V.interp_boolean
~contains_zero:(V.contains_zero ev1 && V.contains_zero ev2)
diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index 947a05be216..605ac862d26 100644
--- a/src/plugins/value_types/cvalue.ml
+++ b/src/plugins/value_types/cvalue.ml
@@ -301,7 +301,7 @@ module V = struct
else r
with Not_found -> l
- (* More agressive reduction by relational pointer operators. This version
+ (* More aggressive reduction by relational pointer operators. This version
assumes that \pointer_comparable alarms have been emitted, and that
we want to reduce by them. For example, &a < &b reduces to bottom,
which might be problematic if &a and &b have been cast to uintptr_t *)
@@ -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/value_types/function_Froms.ml b/src/plugins/value_types/function_Froms.ml
index 307d785f602..8631bac1a91 100644
--- a/src/plugins/value_types/function_Froms.ml
+++ b/src/plugins/value_types/function_Froms.ml
@@ -361,7 +361,7 @@ module Memory = struct
let both = find_precise_offsetmap in
let conv = convert_find_offsm in
(* We are querying a zone for which no dependency is stored. Hence, every
- base is implicitely bound to [Unassigned]. *)
+ base is implicitly bound to [Unassigned]. *)
let empty_map z = Deps.from_data_deps z in
let join = Deps.join in
let empty = Deps.bottom in
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index e8123cbd322..d063b30c6ee 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -92,7 +92,7 @@ Plugin WP 0.9 Magnesium_20151002
- WP [2015/02/28] Refactoring of compound objects modeling.
- Qed [2015/02/28] Fold constant expressions in goals.
- Qed [2015/02/28] More simplifications on strict inequalities.
-- Qed [2015/02/28] More agressive filtering and pruning (-wp-filter).
+- Qed [2015/02/28] More aggressive filtering and pruning (-wp-filter).
- Qed [2015/02/28] Aggressive ite-lifting.
- Qed [2015/02/28] Automatic introduction of existentials.
-! Coq [2015/02/28] Inductive if-then-else construct.
@@ -174,7 +174,7 @@ Plugin WP 0.7 Fluorine_20130401
- WP [2013/02/01] New interface to model selection (unique
-wp-model option).
- WP [2013/02/01] Experimental float and machine-integer models.
-- WP [2013/02/01] 'Store' and 'Runtime' models abandonned.
+- WP [2013/02/01] 'Store' and 'Runtime' models abandoned.
- WP [2013/01/09] 'Typed' becomes the default model.
- Why3 [2012/12/18] Why3 output (-wp-proof why3:xxx).
- Typed [2012/10/23] Extensions of Typed model (unsafe-casts).
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index b37785bb329..22dee44ab67 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -452,7 +452,7 @@ let smp1 zf = (* f(c1) ~> zf(c1) *)
let smp2 f zf = (* f(c1,c2) ~> zf(c1,c2), f(c1,c2,...) ~> f(zf(c1,c2),...) *)
function
| e1::e2::others -> begin match (F.repr e1), (F.repr e2) with
- (* integers should be at the begining of the list *)
+ (* integers should be at the beginning of the list *)
| Logic.Kint c1, Logic.Kint c2 ->
let z12 = ref (zf c1 c2) in
let rec smp2 = function (* look at the other integers *)
diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/GuiGoal.ml
index 3758c682cba..082e9df9117 100644
--- a/src/plugins/wp/GuiGoal.ml
+++ b/src/plugins/wp/GuiGoal.ml
@@ -267,7 +267,7 @@ class pane (proverpane : GuiConfig.provers) =
| Empty | Forking _ | Composer _ | Browser _ -> ()
(* ---------------------------------------------------------------------- *)
- (* --- Prover Controlers --- *)
+ (* --- Prover Controllers --- *)
(* ---------------------------------------------------------------------- *)
method private register_provers dps =
diff --git a/src/plugins/wp/Letify.mli b/src/plugins/wp/Letify.mli
index ec7c9749c99..e163458103f 100644
--- a/src/plugins/wp/Letify.mli
+++ b/src/plugins/wp/Letify.mli
@@ -69,7 +69,7 @@ val add_definitions : Sigma.t -> Defs.t -> Vars.t -> pred list -> pred list
definitions of variables [xs] from [sigma] that comes from [defs].
They are added to [ps]. *)
-(** Pruning strategy ; selects most occuring literals to split cases. *)
+(** Pruning strategy ; selects most occurring literals to split cases. *)
module Split :
sig
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 0c27341d0a4..22c2d889f6f 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -534,7 +534,7 @@ module ShiftGen = Model.StaticGenerator(Cobj)
let compile = Lang.local generate
end)
-(* The model-dependent derivation of model-independant ShiftDef *)
+(* The model-dependent derivation of model-independent ShiftDef *)
module Shift = Model.Generator(Cobj)
(struct
let name = "MemTyped.Shift"
diff --git a/src/plugins/wp/TacInstance.ml b/src/plugins/wp/TacInstance.ml
index 05e782cc961..68d09f8536e 100644
--- a/src/plugins/wp/TacInstance.ml
+++ b/src/plugins/wp/TacInstance.ml
@@ -33,7 +33,7 @@ let descr = function
| 1 -> "First Parameter"
| 2 -> "Second Parameter"
| 3 -> "Third Parameter"
- | n -> Printf.sprintf "%d-th Paramter" n
+ | n -> Printf.sprintf "%d-th Parameter" n
let mkparam k =
Tactical.composer
diff --git a/src/plugins/wp/TacNormalForm.ml b/src/plugins/wp/TacNormalForm.ml
index 7d56a68b3d4..41403ed21a7 100644
--- a/src/plugins/wp/TacNormalForm.ml
+++ b/src/plugins/wp/TacNormalForm.ml
@@ -24,7 +24,7 @@ open Lang
open Conditions
open Tactical
-(** Usefull **)
+(** Useful **)
let str_case = "Case"
let sub_cases phi = function
diff --git a/src/plugins/wp/VC.mli b/src/plugins/wp/VC.mli
index d230fa5846d..2c65f764a55 100644
--- a/src/plugins/wp/VC.mli
+++ b/src/plugins/wp/VC.mli
@@ -45,7 +45,7 @@ val is_proved : t -> bool
(** {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/calculus.ml b/src/plugins/wp/calculus.ml
index fecd02f0f5f..772bc8febfe 100644
--- a/src/plugins/wp/calculus.ml
+++ b/src/plugins/wp/calculus.ml
@@ -301,7 +301,7 @@ module Cfg (W : Mcfg.S) = struct
if we have some goal G about this edge, store G /\ p
if we have annotation B to be used as both H and G, store B /\ B=>P
We also have to add H and G from HI (invariants computed in Pass1 mode)
- So finaly, we build : [ H => [ BG /\ (BH => (G /\ P)) ] ]
+ So finally, we build : [ H => [ BG /\ (BH => (G /\ P)) ] ]
*)
let set strategy wenv res e obj =
try
diff --git a/src/plugins/wp/cil2cfg.mli b/src/plugins/wp/cil2cfg.mli
index 6905e379fa8..ad99002599a 100644
--- a/src/plugins/wp/cil2cfg.mli
+++ b/src/plugins/wp/cil2cfg.mli
@@ -141,7 +141,7 @@ val get_post_edges : t -> node -> edge list
val get_post_logic_label : t -> node -> logic_label option
(** Find the edges [e] that goes to the [Vexit] node inside the statement
- * begining at node [n] *)
+ * beginning at node [n] *)
val get_exit_edges : t -> node -> edge list
(** Find the edges [e] of the statement node [n] postcondition
diff --git a/src/plugins/wp/doc/manual/wp_caveat.tex b/src/plugins/wp/doc/manual/wp_caveat.tex
index 3905b649808..f4cf40c4e68 100644
--- a/src/plugins/wp/doc/manual/wp_caveat.tex
+++ b/src/plugins/wp/doc/manual/wp_caveat.tex
@@ -19,7 +19,7 @@ global ones).
%read into the memory. Only pure logic functions and pure predicates can be
%defined in axiomatics with this model.
-Additionaly, the \texttt{Caveat} memory model of \textsf{Frama-C}
+Additionally, the \texttt{Caveat} memory model of \textsf{Frama-C}
performs a local allocation of formal parameters with pointer
types that cannot be treated as \textit{reference parameters}.
diff --git a/src/plugins/wp/doc/manual/wp_intro.tex b/src/plugins/wp/doc/manual/wp_intro.tex
index 5c49943bd02..68165a3ee56 100644
--- a/src/plugins/wp/doc/manual/wp_intro.tex
+++ b/src/plugins/wp/doc/manual/wp_intro.tex
@@ -53,7 +53,7 @@ precondition engine implemented in the \textsf{WP} plug-in.
The \textsf{WP} plug-in is distributed with the \textsf{Frama-C}
platform. However, you should install at least one external prover in
order to fulfill proof obligations. An easy choice is to install the
-\textsf{Alt-Ergo} theorem prover developped at
+\textsf{Alt-Ergo} theorem prover developed at
\textsc{inria}\footnote{\textsf{Alt-Ergo}:
\url{http://alt-ergo.lri.fr}}. See section~\ref{wp-install-provers}
for installing other provers.
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index e14ad7a95ea..1d73181de41 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -383,7 +383,7 @@ $$\TACTIC{\Delta\models\,G}{%
\end{array}} $$
\paragraph{Rewrite} Replace Terms\\
-This tactic uses an equality in hypothesis to replace each occurence of term by another one.
+This tactic uses an equality in hypothesis to replace each occurrence of term by another one.
The tactic exists with two variants: the left-variant which rewrites $a$ into $b$ from equality $a=b$,
and the right-variant which rewrites $b$ into $a$ from equality $a=b$.
The original equality hypothesis is removed from the goal.
@@ -577,7 +577,7 @@ sequence of hypothesis, and a goal to prove. Each hypothesis is represented by a
When you walk through a sequence of hypothesis, you shall reuse the provided steps to build clauses and selections.
\paragraph{Exploring Formulae}.
-The constituant of hypothesis and goals are logical terms and predicates. You shall use
+The constituent of hypothesis and goals are logical terms and predicates. You shall use
module \lstinline$Repr.term$ and \lstinline$Repr.pred$ to access the internal representation
of formulae. There are many constructors for terms and predicates, simply browse the html documentation to have an overview. Many properties about terms and predicates are directly obtained from the \lstinline$Lang.F$ module. The API is quite rich, so use the html documentation to get details.
diff --git a/src/plugins/wp/doc/tutorial/count/count.tex b/src/plugins/wp/doc/tutorial/count/count.tex
index ac5d57cb4a3..c975eaf8c56 100644
--- a/src/plugins/wp/doc/tutorial/count/count.tex
+++ b/src/plugins/wp/doc/tutorial/count/count.tex
@@ -1,7 +1,7 @@
\section{The \textsf{count} Algorithm}
\label{count}
-The algorithm presented here counts the number of occurences for a
+The algorithm presented here counts the number of occurrences for a
given element in a sequence. The axiomatization of counting
occurrences proposed in ``ACSL By Example'' is:
diff --git a/src/plugins/wp/doc/tutorial/tut_intro.tex b/src/plugins/wp/doc/tutorial/tut_intro.tex
index 9077270c2db..b48e5486357 100644
--- a/src/plugins/wp/doc/tutorial/tut_intro.tex
+++ b/src/plugins/wp/doc/tutorial/tut_intro.tex
@@ -20,7 +20,7 @@ ones presented in the original ``ACSL By Example'' book. Sometimes, we
indicate some modifications of the specification that makes
\textsf{WP} better prove the programs.
-All examples uses the following \emph{libary} of \textsf{C} and
+All examples uses the following \emph{library} of \textsf{C} and
\textsf{ACSL} definitions:
\listingname{library.h}
@@ -42,7 +42,7 @@ Thus, a header file \texttt{A.h} should be enclosed by the following lines:
#endif
\end{ccode}
-Similarily, an implementation file \texttt{A.c} should start by including its header:
+Similarly, an implementation file \texttt{A.c} should start by including its header:
\begin{ccode}
#include "A.h"
[...]
diff --git a/src/plugins/wp/doc/wp-api.odoc b/src/plugins/wp/doc/wp-api.odoc
index ce27f486896..a847ef1f74c 100644
--- a/src/plugins/wp/doc/wp-api.odoc
+++ b/src/plugins/wp/doc/wp-api.odoc
@@ -1,5 +1,5 @@
This is the documentation index for Frama-C/WP plug-in API. The main entry
-point of the plug-in is module {!Wp.VC}, which provides third party developpers
+point of the plug-in is module {!Wp.VC}, which provides third party developers
with a programmatic access to WP command line features. The complete list of
available API is listed in module {!Wp}, although a more comprehensive
organization is described below.
diff --git a/src/plugins/wp/qed/old/proof.mli b/src/plugins/wp/qed/old/proof.mli
index 0747761a02a..b5fdb9c5f5e 100644
--- a/src/plugins/wp/qed/old/proof.mli
+++ b/src/plugins/wp/qed/old/proof.mli
@@ -52,7 +52,7 @@ sig
- when [Qi=forall x], check [Li=Lterm t],
- when [Qi=exists x], check [Li=Lvar y] and [y] is fresh,
- assume [P[xi:=Li]],
- - finaly prove goal with [Pgoal]. *)
+ - finally prove goal with [Pgoal]. *)
| Intro of link list * proof
(** [Intro(L1..Ln,Pgoal)]:
diff --git a/src/plugins/wp/qed/src/engine.mli b/src/plugins/wp/qed/src/engine.mli
index 56585fe64ac..21c096e6ed9 100644
--- a/src/plugins/wp/qed/src/engine.mli
+++ b/src/plugins/wp/qed/src/engine.mli
@@ -287,11 +287,11 @@ class type virtual ['z,'adt,'field,'logic,'tau,'var,'term,'env] engine =
Default uses [self#pp_shared] with mode [Mprop] inside an [<hv>] box. *)
method pp_expr : 'tau -> 'term printer
- (** Prints in {i term}, {i arithemtic} or {i prop} mode with
+ (** Prints in {i term}, {i arithmetic} or {i prop} mode with
respect to provided type. *)
method pp_sort : 'term printer
- (** Prints in {i term}, {i arithemtic} or {i prop} mode with
+ (** Prints in {i term}, {i arithmetic} or {i prop} mode with
respect to the sort of term. Boolean expression that also have a
property form are printed in [Mprop] mode. *)
diff --git a/src/plugins/wp/qed/src/logic.mli b/src/plugins/wp/qed/src/logic.mli
index 52b806660d3..f733b1d3d90 100644
--- a/src/plugins/wp/qed/src/logic.mli
+++ b/src/plugins/wp/qed/src/logic.mli
@@ -420,7 +420,7 @@ sig
The list of shared subterms is consistent with
order of definition: each trailing terms only depend on heading ones.
- The traversal is controled by two optional arguments:
+ The traversal is controlled by two optional arguments:
- [shared] those terms are not traversed (considered as atomic, default to none)
- [shareable] those terms ([is_simple] excepted) that can be shared (default to all)
- [subterms] those sub-terms a term to be considered during
@@ -449,7 +449,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/qed/src/term.ml b/src/plugins/wp/qed/src/term.ml
index 0a9b45857fc..372e97df973 100644
--- a/src/plugins/wp/qed/src/term.ml
+++ b/src/plugins/wp/qed/src/term.ml
@@ -2393,8 +2393,8 @@ struct
let marks ?(shared=none) ?(shareable=all) ?(subterms=lc_iter) () =
{
shareable ; subterms ;
- marked = shared ; (* allready shared are set to be marked *)
- shared = Tset.empty ; (* accumulator initialy empty *)
+ marked = shared ; (* already shared are set to be marked *)
+ shared = Tset.empty ; (* accumulator initially empty *)
mark = Tmap.empty ;
roots = [] ;
}
diff --git a/src/plugins/wp/share/Makefile.headers b/src/plugins/wp/share/Makefile.headers
index 1607279c77a..aca872c9b21 100644
--- a/src/plugins/wp/share/Makefile.headers
+++ b/src/plugins/wp/share/Makefile.headers
@@ -34,7 +34,7 @@ headers:
$(HEADACHE) -h $(LGPL_HEADERS)/MODIFIED_WHY3 $(ALL_MODIFIED_WHY3_RESOURCES)
$(HEADACHE) -h $(LGPL_HEADERS)/UNMODIFIED_WHY3 $(ALL_UNMODIFIED_WHY3_RESOURCES)
-# target used by developpers of wp/share directory
+# target used by developers of wp/share directory
.PHONY: headers.wp_share_src
headers.wp_share_src:
$(HEADACHE) -h $(LGPL_HEADERS)/CEA_WP $(WP_SHARE_SRC_CEA_RESOURCES)
diff --git a/src/plugins/wp/share/src/qed.why b/src/plugins/wp/share/src/qed.why
index c701920b230..93964ca523c 100644
--- a/src/plugins/wp/share/src/qed.why
+++ b/src/plugins/wp/share/src/qed.why
@@ -29,7 +29,7 @@ theory Qed
use import int.ComputerDivision as CD
(** to be used only for the ACSL ite generation.
- Something is wrong with "wp/share/ergo/bool.Bool.mlw" (comming from why3),
+ Something is wrong with "wp/share/ergo/bool.Bool.mlw" (coming from why3),
the function match_bool is undefined.
An hack is to give a definition here. *)
function match_bool (x : bool) (y z:'a ) : 'a
diff --git a/src/plugins/wp/share/src/vlist.why b/src/plugins/wp/share/src/vlist.why
index cbc995cc7d2..de7e3fb62c8 100644
--- a/src/plugins/wp/share/src/vlist.why
+++ b/src/plugins/wp/share/src/vlist.why
@@ -43,7 +43,7 @@ theory Vlist
function nth (list 'a) int : 'a
(* -------------------------------------------------------------------- *)
- (* --- lenght --- *)
+ (* --- length --- *)
(* -------------------------------------------------------------------- *)
axiom length_pos : forall w:list 'a. (Int.(<=) 0 (length w))
diff --git a/src/plugins/wp/share/why3/Bits.v b/src/plugins/wp/share/why3/Bits.v
index f91102a11b0..d33aa34a3cd 100644
--- a/src/plugins/wp/share/why3/Bits.v
+++ b/src/plugins/wp/share/why3/Bits.v
@@ -28,7 +28,7 @@
- for natural [n], the [k]-th bit of [2^n] if [(k=n)] ;
- for positive integer [x>=0], it is the union of the bits of its binary
decomposition (hence, natural powers of two) ;
- - finaly, the bits of a negative integer [x<0] are the reverted ones
+ - finally, the bits of a negative integer [x<0] are the reverted ones
of its two's complement [-(x+1)].
The realization of the theory proceeds into several stages,
@@ -88,7 +88,7 @@ Ltac Z_compare Inf EQ Sup i j :=
[ destruct TMP as [ Inf | Sup ] | try rewrite <- EQ ];
auto with zarith.
-(** For proving a symetrical relation [P],
+(** For proving a symmetrical relation [P],
it is sufficient to prove [P i j] for [i<j] and [P i i]. *)
Lemma symetrical_ind: forall (P : nat -> nat -> Prop),
(forall i j, P i j -> P j i) ->
@@ -160,7 +160,7 @@ Qed.
(** {@trailing:} *)
(** * Eventually constant functions *)
-(** The bits representation of [Z] integers are eventualy constant
+(** The bits representation of [Z] integers are eventually constant
[nat -> bool] functions. Positive integers finally ends with an infinite
sequence of 0-bits, while negative inetegers ends with 1-bits.
@@ -819,7 +819,7 @@ Proof.
Qed.
(** ** Involution of Decomposition and Recomposition *)
-(** These two fundemental lemmas allow reasoning conversely with bits or integers. *)
+(** These two fundamental lemmas allow reasoning conversely with bits or integers. *)
(** [Z_of_bits] is the inverse of [bits_of_Z] *)
Lemma Z_recomp_decomp: forall x: Z,
@@ -1117,7 +1117,7 @@ Proof.
+ generalize (two_power_nat_is_positive n). omega.
Qed.
-(** Position of the highest significant bit of the predecesor of [two_power_nat]. *)
+(** Position of the highest significant bit of the predecessor of [two_power_nat]. *)
Remark ZxHpos_of_two_power_nat_minus_one: forall n: nat,
(ZxHpos ((two_power_nat n) - 1) = n)%nat.
Proof.
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 328d426883d..af54a479207 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -1120,7 +1120,7 @@ let build_bhv_strategy config =
new_loops WpStrategy.SKannots annots
(* Visit the CFG to find all the internal statement specifications.
- * (see [HdefAnnotBhv] documentation for infomation about this table).
+ * (see [HdefAnnotBhv] documentation for information about this table).
*)
let internal_function_behaviors cfg =
let def_annot_bhv = HdefAnnotBhv.create 42 in
diff --git a/src/plugins/wp/wpPropId.mli b/src/plugins/wp/wpPropId.mli
index 7a78120f69e..6120492db89 100644
--- a/src/plugins/wp/wpPropId.mli
+++ b/src/plugins/wp/wpPropId.mli
@@ -242,7 +242,7 @@ val mk_part : prop_id -> (int * int) -> prop_id
(** get the 'kind' information. *)
val kind_of_id : prop_id -> prop_kind
-(** get the 'part' infomation. *)
+(** get the 'part' information. *)
val parts_of_id : prop_id -> (int * int) option
(** How many subproofs *)
diff --git a/src/plugins/wp/wpStrategy.mli b/src/plugins/wp/wpStrategy.mli
index 6cdee0fc6db..bfb137b9cec 100644
--- a/src/plugins/wp/wpStrategy.mli
+++ b/src/plugins/wp/wpStrategy.mli
@@ -165,7 +165,7 @@ val get_both_hyp_goals : t_annots ->
* considered as a both goal and hyp ([goal=true], or hyp only ([goal=false]) *)
val get_cut : t_annots -> (bool * WpPropId.pred_info) list
-(** To be used as hypotheses arround a call, (the pre are in
+(** To be used as hypotheses around a call, (the pre are in
* [get_call_pre_goal]) *)
val get_call_hyp : t_annots -> kernel_function -> WpPropId.pred_info list
@@ -251,7 +251,7 @@ val pp_info_of_strategy : Format.formatter -> strategy -> unit
val is_main_init : Cil_types.kernel_function -> bool
-(** True if both options [-const-readonly] and [-wp-init] are positionned,
+(** True if both options [-const-readonly] and [-wp-init] are positioned,
and the variable is global, not extern, with a ["const"] type
(see [hasConstAttribute]).
@since Sodium-20150201
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 20740a965ff..89ca7abd7a0 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -121,7 +121,7 @@ module Check: Parameter_sig.Bool
(** {2 Environment Variables} *)
val get_env : ?default:string -> string -> string
-val is_out : unit -> bool (* -wp-out <dir> positionned *)
+val is_out : unit -> bool (* -wp-out <dir> positioned *)
val get_session : unit -> string
val get_session_dir : string -> string
val get_output : unit -> string
diff --git a/tests/slicing/README b/tests/slicing/README
index 60d7316aec5..47ee0df1fc9 100644
--- a/tests/slicing/README
+++ b/tests/slicing/README
@@ -72,7 +72,7 @@ For the Program Dependence Graph tests, see ppc/tests/pdg.
the version of the function to call.
** tests/slicing/libAnim.ml
- Usefull functions to view graphically the building process of a slicing
+ Useful functions to view graphically the building process of a slicing
project.
** tests/slicing/anim.ml
diff --git a/tests/slicing/merge.ml b/tests/slicing/merge.ml
index d090c1f55c1..f14fca36514 100644
--- a/tests/slicing/merge.ml
+++ b/tests/slicing/merge.ml
@@ -57,7 +57,7 @@ let main _ =
(*
Format.printf "~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\n";;
- Format.printf "=== g_2 sould call init_2 and g_3, init_3 :\n";
+ Format.printf "=== g_2 should call init_2 and g_3, init_3 :\n";
!S.Project.export None project;;
Format.printf "~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\n";;
*)
--
GitLab