diff --git a/Changelog b/Changelog
index 6f96ab95d3f32779d2d07d3af81445224e11811f..ccd26c12d2e9241d1355ad25d156e1403c334459 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 25bf88efb8bea47d25868f9f31ab618ce62dd67f..cf1e854254b5085cf73b449c85c7dca671da7a04 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 063b2a11c935ee006b665873de86ae0995a70c8f..bf8b8ad3bfe7681da10b64b647352d4678a7b1bd 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 ace93be018f84fa2cc3aafaa7cad0ba56403fdc4..c3705a3a5921e68cc36493666cc8564620073712 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 c85bb87e291ac4dbb977bd0af70d18a03bcf9c80..85c46c98adfde48955bbbde37718555a928377b5 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 facba81bd7e8407c26b983a3ec202e81da3f9c95..b2acdb7043ad6ba8e1ac5c4ec989d058439d3b53 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 387f497b0f9edaf05a405a88ca666d6f2420621d..7196c28e347d7544fd56ce6ffabdc015c31ac596 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 a7597b90da29fb64433d68a5dee3a1727f46f70d..9af475f8b62895915b1fa589e9d99d264c297c0d 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 30909ef11d86cb8651503a006f3fd195924924ed..17889df93390ea6a988e42fb3b9f849713bba264 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 445267fd791b4b8f3cc9e007cd7f2d033a2b978c..5ee3c57da3d650a83d0c1d31204f4317497f1718 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 15fd03b202cb08ff479089a387d5624db89dbdca..a785a2d3f451058fa5d70cdeee5d29f6b9a77731 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 ddfc4bf0a7644b769f4e7f7e9aecdaf28385daca..eb1b63454f9c86fd5cd5210310d99ae48c52ccee 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 4bc235b499f49c44c00ebcdfc5a437a70d7f88f8..0d5391c728d9592084b91b3ab586f58ec3e3bddc 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 55985a6028aac3e6d58448bd9d580aa4ab7b6503..9ff6dbf54e4745d3645700f4b38a7d230a14eef4 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 34004e72a12c49baaa382babc3063d639a1f1f3b..aa630b8554353327da6d4506d35d939ba5c022f9 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 eee5c41225a8121b37f82d369fd0522f55258c70..5a99248d6d715039d1daf0dbbe290a0a849b947f 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 d73a165cbd291a832cce16552c696543b9317929..4949cb7a2b9623df84b762530f46c90c76d7b124 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 4c88e5cf8c41d765b295d394b1facaad5b9ef1ae..1db84ce3a7b2c230bb32d72745ff059cdc20d53e 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 79c84a799e6cbca60a08b7ae8ac1f700fb7f6c60..078cf571783e71969e76302f7d85175930062831 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 0c4e8200262878255eef3c281411746608c6e8dd..edbb6a3777aab970b231ea614a2e21280e9e2720 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 c874fb0c5b1f222c0c444f580095b63b671fe3cd..3b463ccf4934dda9e3db983fdcb23a96c7de2787 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 d2c8cce9cd5e658cd9bfa7e7881d31e9cf934ed5..32a1d5b7dd77c646ea7751d09f9099cf5bdd02b7 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 3496d74ca261f4de1afc9b51ad907e7e7072ee21..c30fa220e018a2c683423810a499ec5913d0ef71 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 053e9b1cd6f8d8aa8396bf8e4f36170d728afcdf..ac8b91de240e57cd6d6401b1606af25cf3371341 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 a888a10244d23064d1adb8b89f84239183795389..db42387f27ee3e863422f40f1043e8948b50df5e 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 247b49758c4025a5fb5032696c2f7c67ac0f9c45..6dc74339d427ef94120800ba9f3b5801fad7d1ce 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 844ec5dca50311685ff4c361c92ff21ecfd9cb3d..165cb80d8bea1c4a646394daf9e778df028be294 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 99344356dc3669b5ca71838f5dc0e4a68f809a66..9c54ba11aa3e0072edb06067d4439f9e5c8ffe07 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 784639c63362b52b59ee95fd40b951e8e9d3d666..68df66f7dff6d00876e6a5b0c4e475b7c50c74e3 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 5e5aff366b16c560d0007a0e6ad9569831471ff1..ce2d2440cc39544ae06f7ec847daa71750756a38 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 dc04b3f45d39d784cfe1ff93f1e62835e0d542c6..9b7858beeb8c1dfb18f928970cd518a8285fa1b6 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 de0c911c896a95e35ee670988e33b756505b235a..46cf3d735a93f02786b05d8ec94e77b7b2f7c606 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 8def04b816d1d3a059d5d6863bd8d095d9c68509..1549309d2381e8af4e5d6acdf6512eb16c7ca5bf 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 94250b4c744157e34932fa5e38f2bf01faf4a462..802f0605e28eed44f2e1451de1340ccafcd4ff7d 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 0d6eb24c5a99afe4c219b54317933714b13b0c51..4286d8ec203afa820e85f148fef8048d3e4a5146 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 efb675f9ca29cd11e4f7cc507aa0f81d39ffac6d..a9c785b5f642a1010ec39b88f8d3d99296d78e7a 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 7f10d0a9b27e71aaf5d48ba1a0d2cda6bc4147d2..a32c483244d1f058536ed49d615f6ddf5d673737 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 ec565ce287f4da4e393225a76cc33acfb74175be..dfba0166100d1aece627f3372ea6b628d94cbf14 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 7e59cd58de137e69d41be00cffcd2e284e608867..5911aef40cff189ed06d14ef4041fc734e1d406e 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 5bb4a58fe993a1e7bf0b6629dd78f62bc8a23a4d..18abbb73b04f6aa1c06211d77927a005f96f32b7 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 cdc4a7be0ce5ee825c665723d792680182afaf65..6e1c769e6e2445f28883994b6d9758b92e020a65 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 174cd2b92dcc1fa074cff480f99579f63984ee02..a96082ded5f8d477e1990b3a7b7ad04653328bfb 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 93c42601757552e2f4231d6911355a3b17f856d9..9fbb52626ea8abd7b0416172c6fa3bb9b89fae34 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 9be494942f146df2a2b0650a761285d88a0ec59d..36d6ede6ec6c68d4d88a9174bf68eac4bc18f854 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 94105af849da862f88bdfd7a5a3aefc3c8751d9b..22596985ebd9c6bb5ca59a03e4926745101b1c55 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 99a37c5a140b4e44b9f46f4e20407a4e35562310..3eba911e6ddd076409a2e5699100d1f0220e7cf1 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 2b5280d9c8167da1ba111c4b53aae598db21bd34..a1500650ff6438c31dcc720c48b3a573a0978e6e 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 bf664737eb56849f5371133f09e3412df5fc5589..6f12bce75e5e9d25d75386239410be07d7a6cb8a 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 f31e95df220716f65adb47132ee81681e93b09e7..252fa06074984a7ce9eb001f1bf7204506c4299f 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 72d8f3e877a1722e2e89b699cbb9d8eb1d6683cb..64604fd7f668ddfb947debb21019201db7fcd06d 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 6475cf4d9dedeebd317fe535bed9fe807bc637d1..8750429f5b86a188dbc889850b4fbb3de652327f 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 e6b083a53625877a112d3cbc540645c9e98f4ff6..29bb1b0327e12bd644be4f26abac3b1b75315dcb 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 0c4ae9a37d5c752b8f5b8616c4524b6a6a6ab0cc..9a5678bcf36f27750349a2a333cec95ee6e2ea77 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 ddea72a181473a7a4d56c49f499f039e0e5fa11a..ab07426893c51b4b288bde1be3a2e28113b7c8da 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 a6ad4722a8b2def04f9fda8f72f1bb1a588647d2..042adcfedfd569baf574feb1ba713776e27eeb3b 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 ba8de9d6ceb0fd5d8bfe627a1f169d0a277abc12..2ba894afceabe2faa810a51ae031a6a04f7e2287 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 2e8ece882d4492928d707acf7c6b830fadcd1390..6d4836bb32c289931e7a4ee27ad3782c6a267fab 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 e49f11d63709b370d5f2c3aa65eb9f8718721ebb..77900249ee9ce951327cb08273829370c962f985 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 9aab7e0bbabb5d86966578f11ba2790ef76996af..08bf94274c2bf23fa821f39fb820a4218d996767 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 534c2cbd226945c8377f6faeb57ed2963af7377b..da896ca36a2b10a29accc3cc15bdb35defd4a1b9 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 8ab152a51ca35e468b65a6e336bc6f718be44c18..7ed1b8bd73b504387a61a3b66364f8887b022258 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 1f689e34fddc5a64a20b511378999e08c1dee2bb..9ee3e7cba12a585c64cf659301a8985fcc062971 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 b2d786b0ded60d8f23d9de6bd6ec2bdbddc8a492..3ebf43df12b59650f7a61f4fad2203111d8bef37 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 c24d61b4a52057ca2a1f16f316b20b0e657ffcc4..24332ed0f24bb4ffa9c3b327398dbe0dbb383b64 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 359abc03b3d6d3cde74fbc05c857346d32e31121..5e43842d981966a3d3788d789a78c47c5f8ac1c8 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 ec9bc821a4da2d0d628851ab69e6b794b33e54db..e7a2c251a336e0f4f3b4f32b4abc385fddcf79fd 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 8aa15fa792904c76c7d2ab5790838089820da315..371be219c4352f727dac3b92f26a69a18839a79b 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 ef302dca7b2c1016ab05030fbcfb91579a2a2fcd..359d12f4f69d77e7e3ffe4a9d67a19e9b4f7de23 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 8b5a00e285a41e2a81c2fd69f24f1f16740bfc95..0332a621393f158cfbf5a8183380700e35c7930b 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 4f2475a33c28a0e56aaf708eaf6fd34175b2d923..70438cc8ab29dbd08f02ed1df0f610898ac6f71e 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 6a70e2dea52faf78f318628278fef109bb3840fc..2f5430b62e34520143d02453b419d88537518439 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 d23d7938289b658b75e13130bbe0e2f26abb84dc..5772ea04141acac8c11b16764cea746a849cc7b8 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 d971acb2566cf6bbf438a620ec3ead9f83b5d767..42036e30c6a276a0ca9fbf59e7cb85144a9d0edb 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 e7b91d1b62c97018045ddfe20d1e866d24815ba3..95082fa5a7436cc47b9f48755237684154442959 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 230adf06e264467c00fcee890d6419e565b11664..13242edf0dbf7c6ae3af67fe36b2203a834deead 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 1943cf45768c4b59362a64f93f33cdaf7c909158..c23397c31c5b8e069cb0cfaff2ca8d8044419931 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 00fdaec1d844c3033892d0d21aad005667063c39..c50c9466467a44f6fb4bfc9ce402b81181243f3b 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 e8c09eb34004620faa1211330115849ec1c774f3..d02763693c03d5a9a2fd2258a6c448e2d00846c5 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 7fb6c1316dd9dbb28f24e9aae903381ba6f4a6ba..d5ced51e58c658a1edd4e02453fc46d828e8b2a8 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 c7e42460bd8bcd9b386fcd239d216486ba55555b..0d905d5dbd126db37695bc7a1153e26d3ab0d1d1 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 7184a81cbb291d8481409cfcc12fa22b28caf701..98bbe0861b3fc8ace48a70cb64d6ccc35fb0dcaf 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 4b91d0bbe4a6ae21e9d9fde2addd80ff7a903220..754c4e5921929f49e8339994136b44e17b6c906d 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 2873122dd0849ec63a20aad59869cd5722e08a74..a1668782a02d584008bdb3795248e8a7bab74a5d 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 9318acb0338340539219ca209a8c0fdac29048e1..51ca7dfe618e7f75948ec2c80844d7b8a494280a 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 7556c0ceb5d2807b0c7b1cffb7ac08ed2df63135..0c5d9fbddb94dce9c289b13b5068d20b43a471ea 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 d2425ff8ead91d7a3f1cbbbef091d43a6553ee93..2d7bd3c0b441ea695c5bd8472a5aeb035baa54c2 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 302d52160882a642488fdb05a4f237b72f6f995c..d4298f06f06e41e55d5e38f9345b3eb62838ea6b 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 1c011684e167b0d95a1b2178e07c82e70a956cb1..71bf44c56c7b2f3d83a75da39204c075923a83b0 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 c803fbda0557ec198cdd77b425e3a2a57b3361c8..682c55293e63089d1c2492b3417b574e45373068 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 c88c434d3a1db98e534981edc3223b3d89ec6665..88e7c23c8ec776993b453c14d003c3a8340e12cd 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 741676045ebe1a12891290f93e69cfe29b2436bd..0e7cc8863a067569ef1f78c63f871e8391fdba22 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 2da6ca3c467c1ff3df676202f6b4b138eb66d8ef..fb051e65de0e1144a64ab56a2bfc54db9ee8951f 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 7e89c6f1207f81c46bc208af8e89d087e5477877..b74fe55619d0a127c1dc30d0fd28b9ab590d477a 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 6a401cac603d3f821beeca87bc938ad66defa056..ec2f9e3fba8d8d5f3a80a8eefca2f697ee2399f0 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 f72a78b92612df8bec0cdd045c1b7ec89fc3a8d7..986a4ccca31e1029591952ab029ced956ad094b0 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 906499e38ce93a62a83860eb1935b98928a0ca50..51046be16b70fa4cb956691fbee47134e375d4b8 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 9ba8cdf53a72c3ea12a2952b692da0e61c2a9468..3f21edc91cdf6b1c1f966f0eaafa97fab861d557 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 14a6350c63252885c02ea02dfcb45108adfc1838..7cf97e637601e24edd8d08ae6b1ac3a9892e3ea0 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 2fdec90925b7b5750aa9cff38222b453aacee852..8dbc26fef07e41a2b5bf1aa0d1c42d056d0bd840 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 e7e38558e41746912c7941ec2bfeec0e0bef1550..ccf717c1a8640f6d44cf9bb3c9b303c47339ebb4 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 1acb4a1f755b2e20670f30dd94837718baa94c0a..935bdbda827557f989c1788f97691810d5be9ed2 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 167b4935e593aa832e9eb303d9fce6137d671f7a..81820624a5cbed6430ce4fe94a80c91fe45169c2 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 6ddddd7f9014fb9ae9bb1653af483c105f3a72fc..cc23fb671f1a64177e9d3e5864edd19e223a2580 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 c3002047c858c27983e7598d76f5e5edddd663b4..e44efc0af9ce3ec27be8dce2d93d6d6efae4d7c8 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 080604ebf044cbd9e8d53e7d02546a227e7a46bb..cbdb3aa5167bcc9c8b940aaeedae5225ea7a3cab 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 bfa21ba5415d71380b9e36d3e1a15b94e080e08b..2c883ecf25a811c06dde69fd248b7dda579a23a5 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 1d3742fce2fb12ae0a1a9d63a9c0d0b2567059a6..a9d4e5f059d86a0101061296e34e142c1ad36833 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 69e969c80294ef752c49a199fd9fe52181f44310..ce819f841bb208a320b3813395e1764f53ca1f93 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 9caee205a6e2202b3d53abafb86333412af909d7..c0f0c187e51504fe36d70069f4d62431fe0f0258 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 f86cbb04baad5f6043a7bda8a0eeead06c6f790a..372898fac1babe1256224162a9d83a0f5a213e54 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 3358510d4e9e52c29d8d4ff9f401b13feb315ad4..0d9780fde03a7347aba14201d9483df855778c5f 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 f2d5e132ad2b75c825e5d139a674d353be460f6f..3e2d03c72e18d4389bb13d02e8beb2e6633fbaa3 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 7d1e2c92604bbd3d70398dd129d7d449cd4c715b..f45ff944dd7fb543eb37ab3f454aea778850b638 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 3760fd834d4d9a03f3f12218e17d6ec34cbebfe2..dc58de3cafc87d8046bfc6c716904e4d6219d79f 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 e3c743d97292919a5f4cc0f15f413b750f52b4fb..81f91d69fb8197b27185eefeb1da8ae207770f0b 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 e57109da56c98e8389d32a4e4e50b8a8ed54db4c..b713a7c19be96463151c47a2e162d73000a0406f 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 1b3c75505f38c1d29481bf37c3209d5676a5c4d7..f8de88297a3b7f229eb738b8cbf5855e04aea733 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 61c3ed903e5426db83250abf1024937f2f9bb70d..c0364d7eb997882b4682d21fbd95d07fb5abd010 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 8be2acc73c8976ccfc9c2a4763c02e9abb0373e7..149da154881ba01095ad446990d73db9e7b1e8d8 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 e734154add384f017568fca0503601a5875a7f96..7ee78ca18759996cab0272ea6f599220113647eb 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 947a05be216e528562a09b47d138714562f9f3f8..605ac862d2684af86e73dfac168e9e89b3c66d6e 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 307d785f602db78dc116ee659ffc27a980d3cddc..8631bac1a91e4da5f281ee1487f46153fcfbd9c6 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 e8123cbd322a466c230ba80048e544f18e896190..d063b30c6ee6e1069a0a1b29ad5e04239c8e414a 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 b37785bb32911e50236b8791bf55b46a50666c3e..22dee44ab674dab1751380e2410d2e36d7fd6285 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 3758c682cba0667ce861e7a1c5e07f2b426f89e0..082e9df9117404b4b0dd4d36152dfd7135cef6d2 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 ec7c9749c99e6941c5daf8a766f091443cde83b7..e163458103f545a763217cc1ff1a6cdeacc77bcb 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 0c27341d0a46f0e4ab2f7745814c45090f20a1a8..22c2d889f6fa8a33bf46214cf7b144d72cee0579 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 05e782cc96133a59c4bbe2061602fc2e1e8c54cb..68d09f8536e144969adeaac17131fa33a2ba94c7 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 7d56a68b3d4616908c94e12f256b2ebd70e15e50..41403ed21a745cf9c3ebc783ac775350c4302db6 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 d230fa5846d65331fc6748621d26dd667a38b637..2c65f764a552bbb6a3ece9da6e6642451700a764 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 fecd02f0f5f7d9a5fc8bcc0fa26ff059f6a369be..772bc8febfeef1b564b2938c4c97d6a338fb98de 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 6905e379fa8bdbc843afda5f21d4cfbcfb6b4ccd..ad99002599a8e5f7cef5536dba8de04f643de07e 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 3905b64980833655a9202599b110098dc458e1d8..f4cf40c4e6806dd82ed2c5cef8e14fdaa86c6e77 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 5c49943bd02eeb4327ed9a98bd75ca771d56b10a..68165a3ee5618bdf2245a66c0e63c575933f00e6 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 e14ad7a95ea193c4555956312f24a479fdb9f05e..1d73181de410c165973b76a941ce9327f66a8ead 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 ac5d57cb4a383e64fcf5578b5fe2d8290a8a66d6..c975eaf8c564f1a99cd9dc57c011a8fb5af16899 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 9077270c2db52a39a1e3af89939470032d6e172c..b48e5486357e1f517ffa3bb243882c987500db6c 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 ce27f48689625d9daa29ad3d013e9ce82f0225e9..a847ef1f74ca17a2206265032b08af0bf72de7dd 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 0747761a02aeaec8a2fc68615a66f6941428d582..b5fdb9c5f5efe38919f2757e26ebb430f151eb09 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 56585fe64acd7e244b4734f6e7c99e68cf2e0d63..21c096e6ed961fa5b2aaebf15968af644a8e180c 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 52b806660d3fad544467e020044ca25d4c8d0738..f733b1d3d90f7c64745b5cc3a174c044be789848 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 0a9b45857fccec84ac865683aacc138fc1fc1b46..372e97df973e3d6213aa1797fd61ae56bc3047d8 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 1607279c77a2bfc1d5be4df70354e17d1fe0d8ad..aca872c9b21ea6f2e0f43c13c1ff1acff11f0df7 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 c701920b230da9ebef5da50a5061d2c6ae136ac9..93964ca523c1e1ccf711179ab2c3bc6a6e22b22b 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 cbc995cc7d2a607d90664ba7248a3271227e814a..de7e3fb62c807ba030d40c737058f5a9a43deeae 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 f91102a11b005c37ad503aac2415ba6284c500eb..d33aa34a3cd9a833bd4b669c0b06e69523a492e3 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 328d426883d8e4b948cd8e089c8a355c08a17574..af54a4792079f19a894d6c1a3306d1674d0678e0 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 7a78120f69e246ca1ba86af6c75248c2dd97e3c2..6120492db89bf2d4d4395ec68b3fab2de913eb23 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 6cdee0fc6db20f3b29be6275bb00ed05e0ff439a..bfb137b9cecdf2ce6b806a7aa1d9ed0a5cd4bb54 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 20740a965ffd1534243dc5a46fd6275a99c9d07f..89ca7abd7a080009ddfbc6f645143ba4c4a52d51 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 60d7316aec5ab89713c4c29bd93e42254d19107e..47ee0df1fc9a8b784d4128621a8dbe315b1bd21d 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 d090c1f55c12f072515ffb858ad2cf59679158a6..f14fca3651496c2b47534c5ecdee63deb2a01cf3 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";;
*)