diff --git a/Changelog b/Changelog
index efb27e56573f89ee354c22ffee3a02ad9d031764..068aa475004be37dc68267703778ad673a59a4b0 100644
--- a/Changelog
+++ b/Changelog
@@ -2451,7 +2451,7 @@ o! Kernel [2010/12/07] Remove function Globals.has_entry_point. Use
Relevant messages changed a little.
-! Cil [2010/11/16] Cil normalization takes care of abrupt clauses
o Kernel [2010/11/15] New Task module: a monadic library for calling
- asynchroneous commands from the toplevel and the gui.
+ asynchronous commands from the toplevel and the gui.
o! Kernel [2010/11/05] File.check_file takes a new argument, allowing to
describe which AST fails integrity check in case of trouble.
-!* Kernel [2010/11/05] Fixed #620 (default assigns generation).
@@ -2900,7 +2900,7 @@ o Value [2009/06/23] New constructor Signed_overflow_alarm for type
-! Jessie [2009/06/18] GUI mode is now the default, options -jessie-gui and
-jessie-goals do not exists anymore
-* Jessie [2009/06/18] Full support for loop assigns, including those
- implictly generated from function's assigns, fixes bug #41
+ implicitly generated from function's assigns, fixes bug #41
- GUI [2009/06/18] Change the warning to panel to preserve decent
performance. This imposes lablgtk 2.12 at least.
- Semantic_callgraph [2009/06/15] small change in the computation of services:
@@ -3058,7 +3058,7 @@ o! Kernel [2009/01/05] Some changes in API of module Type
registration. No more in module Journal. Only in module Type.
-* GUI [2008/12/22] Reentrancy fix with left panels.
-* Impact [2008/12/22] In the GUI, fixed bug while the analysis raised
- an exception. It is now properly catched and displayed on stderr.
+ an exception. It is now properly caught and displayed on stderr.
- Impact [2008/12/22] In the GUI, highlight the selected statement in cyan.
-! Impact [2008/12/22] Do not select anymore the selected statements
except if they are effectively impacted themselves (bts #?411).
@@ -3269,7 +3269,7 @@ o* Makefile [2008/05/21] Fixed bug in "make clean-doc" (and "make distclean").
Open Source Release Hydrogen-20080501
#####################################
--! Value [2008/04/24] Display a warning whenever an unitialized value
+-! Value [2008/04/24] Display a warning whenever an uninitialized value
causes the death of a branch.
- GUI [2008/04/18] Project names are pairwise different in the GUI.
-* GUI [2008/04/17] Win32 default fonts fixed.
diff --git a/Makefile b/Makefile
index cf1e854254b5085cf73b449c85c7dca671da7a04..53ae95db952ed165e137e047110fc897bc5020ec 100644
--- a/Makefile
+++ b/Makefile
@@ -1876,12 +1876,12 @@ dist-clean distclean: clean clean-doc \
ifeq ($(OCAMLWIN32),yes)
-# Use Win32 typical ressources
+# Use Win32 typical resources
share/frama-c.rc: share/frama-c.WIN32.rc
$(PRINT_MAKING) $@
$(CP) $^ $@
else
-# Use Unix typical ressources
+# Use Unix typical resources
share/frama-c.rc: share/frama-c.Unix.rc
$(PRINT_MAKING) $@
$(CP) $^ $@
@@ -1990,7 +1990,7 @@ DISTRIB_FILES:=$(filter-out $(GENERATED) $(PLUGIN_GENERATED_LIST),\
$(DISTRIB_FILES))
# Variables governing the name of the generated .tar.gz.
-# Optionnaly define them as empty to silence warnings about undefined variables
+# Optionally define them as empty to silence warnings about undefined variables
GITVERSION ?=
CLIENT ?=
diff --git a/configure.in b/configure.in
index c3705a3a5921e68cc36493666cc8564620073712..2408602cc3d16ea1f56729586f6133fd8cd093c2 100644
--- a/configure.in
+++ b/configure.in
@@ -160,7 +160,7 @@ fi
# Select devel compilation (warnings, warn-error) #
###################################################
-# It is herited by the plugins
+# It is inherited by the plugins
if test -e ".for_devel"; then
DEFAULT_DEVEL_MODE=yes
@@ -498,7 +498,7 @@ fi # local machdep configuration
# Specific preprocessor support
AC_ARG_WITH(
cpp,
- [ --with-cpp customize defaut preprocessor for Frama-C],
+ [ --with-cpp customize default preprocessor for Frama-C],
[FRAMAC_DEFAULT_CPP=$withval],
[FRAMAC_DEFAULT_CPP=])
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 108e62d1de926664488884c5dd7305cbd08ed78e..1f6a0507deab57df67a6c9dc2c68b82df29c0ad7 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -279,7 +279,7 @@ is not installed (potentially offering reduced functionality).
Plug-in \texttt{gui}\index{Plug-in!GUI} requires
\lablgtk\index{Lablgtk} and \gnomecanvas\index{GnomeCanvas}. It
also optionally uses \dottool\index{Dot} for displaying graphs (graph cannot
- be displayed withoud this tool). So, just after its declaration, there are the
+ be displayed without this tool). So, just after its declaration, there are the
following lines in \texttt{configure.in}.
\begin{configurecode}
plugin_require_external(gui,lablgtk)
@@ -1154,7 +1154,7 @@ or
Module \texttt{Plugin}\codeidxdef{Plugin} provides an access to some general
services available for all plug-ins. The goal of this module is twofold. First,
-it helps developpers to use general \framac services. Second, it provides to the
+it helps developers to use general \framac services. Second, it provides to the
end-user a set of features common to all plug-ins. To access to these services,
you have to apply the functor
\texttt{Plugin.Register}\scodeidx{Plugin}{Register}.
@@ -1771,7 +1771,7 @@ module AB =
(* the unique name of the built datatype; usually the name of the
type *)
let name = "ab"
- (* representents of the type: a non-empty list of values of this type. It
+ (* representants of the type: a non-empty list of values of this type. It
is only used for safety check: the best the list represents the
different possible physical representation of the type, the best the
check is. *)
@@ -2426,7 +2426,7 @@ the low-level functor \texttt{State\_builder.Register} is postponed in
Section~\ref{proj:lowlevel} because it is more tricky and rarely useful.
In most non-\framac applications, a state is a global mutable value. One can use
-it to store results of analyses. For example, using this mecanism inside
+it to store results of analyses. For example, using this mechanism inside
\framac to create a \texttt{state} which would memoize\index{Memoization} some
information attached to statements would result in the following piece of code.
\scodeidx{Kernel\_function}{t} \scodeidx{Cil\_types}{varinfo}
@@ -2788,7 +2788,7 @@ This example shows that the value analysis has been computed only in project
\begin{important}
An important invariant of \framac is: if $p$ is the current project before
running an analysis, then $p$ will be the current project after running it. It
-is the responsability of any plug-in developer to enforce this invariant for
+is the responsibility of any plug-in developer to enforce this invariant for
his/her own analysis.
\end{important}
@@ -3196,7 +3196,7 @@ their execution order.
\item \textbf{The Exiting Stage:} this step is reserved for commands
that makes \framac exit before starting any analysis at all, such as
- printing help informations:
+ printing help information:
\begin{enumerate}[(a)]
\item the command line options registered for the
@@ -3951,7 +3951,7 @@ generator provides a custom tag \texttt{@modify version description} which
should be used to document any element which semantics have changed since its
introduction.
-Furthemore, the special tag \texttt{@plugin developer guide} must be attached
+Furthermore, the special tag \texttt{@plugin developer guide} must be attached
to each function used in this document.
\paragraph{Plug-in API}
diff --git a/doc/developer/architecture.tex b/doc/developer/architecture.tex
index 709a57c52a72c2a8c64788ae580860a5e3983567..2df3d83a5dc1f5be4b46891e2d7ed895dbcb189e 100644
--- a/doc/developer/architecture.tex
+++ b/doc/developer/architecture.tex
@@ -40,7 +40,7 @@ between \cil and several modules of the \framac kernel (\eg the ASTs).
The \framac architecture design is presented in this chapter, and summarized in
Figure~\ref{fig:architecture}. In this figure, each of the four rounded colored
boxes represents a subdirectory $d$ of directory \texttt{src}, while each of the
-small square boxes represents a subdirectory in one subdirectoy
+small square boxes represents a subdirectory in one subdirectory
\texttt{src/$d$}. The remaining sections will explain the goal of each of these
boxes. They do not detail each module of each directory: use the API
documentation generated by \texttt{make doc} for that purpose.
@@ -127,7 +127,7 @@ contains modules defining datastructures directly based upon the AST (module
\texttt{Globals}\codeidx{Globals}), functions (module
\texttt{Kernel\_function}\codeidx{Kernel\_function}), annotations (module
\texttt{Annotations}\codeidx{Annotations}) and so on. A related directory is
-\texttt{src/kernel\_servces/ast\_queries}. It contains modules which provides
+\texttt{src/kernel\_services/ast\_queries}. It contains modules which provides
specific operations in order to get information about AST-related values.
In the same way, an untyped AST quite close of the \C input source is defined in
diff --git a/doc/developer/changes.tex b/doc/developer/changes.tex
index b2acdb7043ad6ba8e1ac5c4ec989d058439d3b53..5d081cc3ab841b6d43a367d6e769afb3f7bdceef 100644
--- a/doc/developer/changes.tex
+++ b/doc/developer/changes.tex
@@ -158,7 +158,7 @@ We list changes of previous releases below.
\item \textbf{Project}: no more \texttt{rehash} in datatypes
\item \textbf{Initialisation Steps}: fixed according to the current
implementation
-\item \textbf{Plug-in Registration and Access}: updateed according to API
+\item \textbf{Plug-in Registration and Access}: updated according to API
changes
\item \textbf{Documentation}: updated and improved
\item \textbf{Introduction}: is aware of the \framac user manual
@@ -180,7 +180,7 @@ We list changes of previous releases below.
\item \textbf{Writing messages}: fully documented
\item \textbf{Initialization Steps}: the different stages are more
precisely defined. The implementation has been modified to take into
- account specifities of dynamically linked plug-ins
+ account specificities of dynamically linked plug-ins
\item \textbf{Project Management System}: mention value \texttt{descr} in
Datatype
\item \textbf{Makefile.plugin}: add documentation for additional parameters
diff --git a/doc/developer/refman.tex b/doc/developer/refman.tex
index 9af475f8b62895915b1fa589e9d99d264c297c0d..3d2254979cb2027118e22749951ba86b8cbbe274 100644
--- a/doc/developer/refman.tex
+++ b/doc/developer/refman.tex
@@ -537,7 +537,7 @@ developer\index{Plug-in!Kernel-integrated}. More details are provided below.
\texttt{Makefile}.}\label{fig:make-sections}
\end{figure}
\begin{enumerate}
-\item \textbf{Working directories} (splitted between
+\item \textbf{Working directories} (split between
\texttt{Makefile.config.in} and \texttt{Makefile.common} defines the main
directories of \framac. In particular, it declares the variable
\texttt{FRAMAC\_SRC\_DIRS}\codeidxdef{FRAMAC\_SRC\_DIRS} which should be extended
diff --git a/doc/developer/tutorial.tex b/doc/developer/tutorial.tex
index 17889df93390ea6a988e42fb3b9f849713bba264..e83f5e0175aa4bb540b70a0a93ce056dfb9cb027 100644
--- a/doc/developer/tutorial.tex
+++ b/doc/developer/tutorial.tex
@@ -159,7 +159,7 @@ creates a \texttt{hello.out} file in the current directory.
To make this script better integrated into \framac, its code must register
itself as a plug-in. Such a registration provides general services, such as
-outputing on the \framac console, or extending \framac with new command-line
+outputting on the \framac console, or extending \framac with new command-line
options.
Registering a plug-in is achieved through the use of the
@@ -905,10 +905,10 @@ once per function.
One can see the effects of the dependency on the \texttt{Value} plug-in
by first launching the value analysis, inspecting the CFG for the
-\texttt{f} function, then chaning the entry point to \texttt{f} in the
+\texttt{f} function, then changing the entry point to \texttt{f} in the
CFG and re-running the value analysis. The console indicates that the
\texttt{CFG} have been recomputed. Indeed the state of the
-\texttt{Value} plug-in, and of its dependencies, was resetted when the
+\texttt{Value} plug-in, and of its dependencies, was reset when the
entry point was changed.
Another way to observe how \framac automatically handles states is to display a
@@ -985,7 +985,7 @@ To summarize:
\item A \emph{project} is a consistent version of all the states in
\framac, together with a version of the AST;
\item A \emph{session} is a set of \emph{projects};
-\item \framac transparently handles the versionning of states when
+\item \framac transparently handles the versioning of states when
changing or duplicating projects, saving and reloading sessions from
disk, etc.
\item The version of the state in a project can change; by default
@@ -997,7 +997,7 @@ To summarize:
when the former is modified in an incompatible way. For instance, it would
have been incorrect to not call
\texttt{State\_selection.with\_dependencies}
- \scodeidx{State\_selection}{with\_dependencies} in the last code snippset of
+ \scodeidx{State\_selection}{with\_dependencies} in the last code snippet of
this tutorial.
\end{itemize}
diff --git a/doc/release/intro.tex b/doc/release/intro.tex
index 9ff6dbf54e4745d3645700f4b38a7d230a14eef4..64f267866d8778a9644e027c18cd0857acb42295 100644
--- a/doc/release/intro.tex
+++ b/doc/release/intro.tex
@@ -2,8 +2,8 @@
This manual is intended for driving the release process of \FramaC
distribution. It covers several topics: people involved in the release effort,
-repository ressources and web site maintenance. The last chapter provides the
-utimate procedure for releasing a new distribution of \FramaC.
+repository resources and web site maintenance. The last chapter provides the
+ultimate procedure for releasing a new distribution of \FramaC.
\section{Roles}
@@ -33,7 +33,7 @@ A \FramaC release consists of the following main steps:
\item \textbf{The branch stage.} A branch is created, in which the release
will be prepared. It will ultimately become the released version.
The development of unstable features may continue in the trunk, while the
- branche is dedicated to the ongoing release.
+ branch is dedicated to the ongoing release.
\item \textbf{The build stage.} The source files are setup by the
developers, and the bug tracking system is updated to reflect the
diff --git a/doc/release/website.tex b/doc/release/website.tex
index aa630b8554353327da6d4506d35d939ba5c022f9..3f6e75d34dc213882b7ccec83aa61d521029f34d 100644
--- a/doc/release/website.tex
+++ b/doc/release/website.tex
@@ -76,7 +76,7 @@ The current (\emph{awkward}) procedure is as follows:
\item Add a new \texttt{selector-download\_NAME} macro.
\item Add a link back to that downloading page into the \texttt{selector-download\_PREVIOUS\_NAME} macro.
\item Check the occurrences of references to the previous release
- ressources, and update them. A good practice is to \texttt{grep}
+ resources, and update them. A good practice is to \texttt{grep}
\texttt{*.prehtml} \texttt{*.def} against the name of the release.
You should at least update the links to reference documentation from the
\texttt{support.prehtml} page.
diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index b5402be1ba80b1b3bd97f27bc70f30b8978d22bd..b6e51dbe00645e0ddb158f0aee31ec91d3d8316e 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -34,7 +34,7 @@ release. First we list changes of the last release.
\item \textbf{Normalizing the Source Code:} document new options
\texttt{-asm-contracts} and\\ \texttt{-asm-contracts-auto-validate}
\item \textbf{Graphical User Interface:} Option \texttt{-collect-messages} is
- active by default, and cannot be deactived.
+ active by default, and cannot be deactivated.
\end{itemize}
\section*{Magnesium-20151001}
diff --git a/doc/userman/user-start.tex b/doc/userman/user-start.tex
index e179a25957582e44009f9bcb5c7bd2a704521cd6..fd924431fa31f168a36fa8be24a8676f2880683b 100644
--- a/doc/userman/user-start.tex
+++ b/doc/userman/user-start.tex
@@ -402,7 +402,7 @@ only copies it to a file. Also, only messages which are effectively printed
\subsection{Terminal Capabilities}
-Some plug-ins can take advandage of terminal capabilities to enrich
+Some plug-ins can take advantage of terminal capabilities to enrich
output. These features are automatically turned off when the \FramaC
standard output channel is not a terminal, which typically occurs when you
redirect it into a file or through a pipe.
diff --git a/doc/value/slicing.tex b/doc/value/slicing.tex
index 80b392e234bf5c96517090faaac5939bb3efa7fe..a02ac602fcb44e249c37ae4ce71faa2801be1ebe 100644
--- a/doc/value/slicing.tex
+++ b/doc/value/slicing.tex
@@ -9,7 +9,7 @@ Parmi les options utilisables depuis la ligne de commande
\begin{description}
\item {\tt -slice-print} :
- {\sl pretty print the sliced code to the standard out, or esle
+ {\sl pretty print the sliced code to the standard out, or else
into the file specified with the {\tt -ocode} option.}
\item {\tt -slice-undef-functions} :
@@ -61,15 +61,15 @@ effectuer en précisant ce en quoi l'utilisateur est intéressé~:
\item {\tt -slice-value v1,...vn} :
{\sl select the result of left-values {\tt v1},...,{\tt vn}
at the end of the function given as entry point
- (the addresses are evaluated at the begining of the function given as entry point).}
+ (the addresses are evaluated at the beginning of the function given as entry point).}
\item {\tt -slice-rd v1,...vn} :
{\sl select the read access to left-values {\tt v1},...,{\tt vn}
- (the addresses are evaluated at the begining of the function given as entry point).}
+ (the addresses are evaluated at the beginning of the function given as entry point).}
\item {\tt -slice-wr v1,...vn} :
{\sl select the write access to left-values {\tt v1},...,{\tt vn}
- (the addresses are evaluated at the begining of the function given as entry point).}
+ (the addresses are evaluated at the beginning of the function given as entry point).}
\end{description}
diff --git a/headers/headache_config.txt b/headers/headache_config.txt
index f334be6c6ebdeb4cb091852c1b586c96b4dc4865..6582d030537c66c63c539b2b77f99905a5c2032b 100644
--- a/headers/headache_config.txt
+++ b/headers/headache_config.txt
@@ -42,7 +42,7 @@
| ".*\.perl" -> frame open:"#" line:"#" close:"#"
#########################
-# MS-Windows Ressources #
+# MS-Windows Resources #
#########################
| ".*\.rc" -> frame open:"#" line:"#" close:"#"
diff --git a/share/Makefile.plugin.template b/share/Makefile.plugin.template
index f9598c81b4b35f9e42dd8ee1a151d59c093bb039..c1517f8ff86c630182a71b3658713fdaf5fea74f 100644
--- a/share/Makefile.plugin.template
+++ b/share/Makefile.plugin.template
@@ -124,7 +124,7 @@ PLUGIN_NO_DEFAULT_TEST?= # Set it to a non-empty value if you don't want the
PLUGIN_INTERNAL_TEST?= # Set it to a non-empty value if the tests of the plugin
# are in Frama-C's tests directory and not a tests
# subdirectory of the plugin (internal use only,
- # obsolete and not recommanded way to handle tests)
+ # obsolete and not recommended way to handle tests)
# Distribution
# ------------
@@ -297,7 +297,7 @@ endif
@PLUGIN_NAME@_GUI_CMX:=$(PLUGIN_GUI_CMX)
@PLUGIN_NAME@_GUI_CMI:=$(PLUGIN_GUI_CMI)
-# Inteface for the the packed pluins
+# Interface for the the packed plugins
TARGET_MLI:= $(PLUGIN_LIB_DIR)/@PLUGIN_NAME@.mli
TARGET_CMI:= $(TARGET_MLI:.mli=.cmi)
diff --git a/share/machdep.c b/share/machdep.c
index 4aaf96666c05bd4a7138b7957fe526a4b0db5636..43caa42a4518daa1c158a031c1103d6c9d26ceb3 100644
--- a/share/machdep.c
+++ b/share/machdep.c
@@ -281,7 +281,7 @@ int main() {
// (int)(&((struct s1*)0)->ca));
}
- /* The alignement of an __aligned__ type */
+ /* The alignment of an __aligned__ type */
{
#ifdef __TURBOC__
printf("\t alignof_aligned = 8;\n");
diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll
index 3b463ccf4934dda9e3db983fdcb23a96c7de2787..ebf9d3ab836fc8e8dd231755a2c2d76b8fad1ca4 100644
--- a/src/kernel_internals/parsing/clexer.mll
+++ b/src/kernel_internals/parsing/clexer.mll
@@ -249,7 +249,7 @@ let scan_ident id =
let init ~(filename: string) : Lexing.lexbuf =
init_lexicon ();
- (* Inititialize the pointer in Errormsg *)
+ (* Initialize the pointer in Errormsg *)
Lexerhack.add_type := add_type;
Lexerhack.push_context := push_context;
Lexerhack.pop_context := pop_context;
diff --git a/src/kernel_internals/typing/alpha.ml b/src/kernel_internals/typing/alpha.ml
index 53ecb8d5bf2ff60b0b26632e1b34ee36e0eed7b9..7efe8438a3bca3bc2279125003708bc798db0815 100644
--- a/src/kernel_internals/typing/alpha.ml
+++ b/src/kernel_internals/typing/alpha.ml
@@ -49,7 +49,7 @@ let alphaSeparator = "_"
let alphaSeparatorLen = String.length alphaSeparator
(** For each prefix we remember the next integer suffix to use and the list
- * of suffixes, each with some data assciated with the newAlphaName that
+ * of suffixes, each with some data associated with the newAlphaName that
* created the suffix. *)
type 'a alphaTableData = Big_int.big_int * (string * 'a) list
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index e126060d2f83e3a7a334a795f06c006ec167e27a..e8bf34710e112a035dce5b3281c23aed73bda29f 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -581,7 +581,7 @@ let process_pragmas_pack_align_field_attributes fi fattrs cattr =
* accomplish this we'll add a local variable to store the target of the
* goto. *)
-(* The local variable in which to put the detination of the goto and the
+(* The local variable in which to put the detonation of the goto and the
* statement where to jump *)
let gotoTargetData: (varinfo * stmt) option ref = ref None
@@ -2341,7 +2341,7 @@ type combineWhat =
| CombineFunarg of bool
(* Comparing a function argument type with an old prototype argument.
arg is [true] for an old-style declaration, which
- triggers some ad'hoc treatment in GCC mode. *)
+ triggers some ad hoc treatment in GCC mode. *)
| CombineFunret (* Comparing the return of a function with that from an old
* prototype *)
| CombineOther
@@ -2760,7 +2760,7 @@ let conditionalConversion (t2: typ) (t3: typ) : typ =
| TPtr _, TInt _ -> t2 (* most likely comparison with 0 *)
| TInt _, TPtr _ -> t3 (* most likely comparison with 0 *)
- (* When we compare two pointers of diffent type, we combine them
+ (* When we compare two pointers of different types, we combine them
* using the same algorithm when combining multiple declarations of
* a global *)
| (TPtr _) as t2', (TPtr _ as t3') -> begin
@@ -2784,7 +2784,7 @@ let logicConditionalConversion t1 t2 =
Cil_printer.pp_typ t2 Cil_printer.pp_typ t1
| _ -> conditionalConversion t1 t2
-(* Some utilitites for doing initializers *)
+(* Some utilities for doing initializers *)
type preInit =
| NoInitPre
@@ -5016,7 +5016,7 @@ and makeCompType ghost (isstruct: bool)
* a construct like "typedef struct foo { ... } A, B;". This is dangerous
* because at the time B is processed some forward references in { ... }
* appear as backward references, which could lead to circularity in
- * the type structure. We do a thourough check and then we reuse the type
+ * the type structure. We do a thorough check and then we reuse the type
* for A *)
if List.length comp.cfields <> List.length flds
|| (List.exists2 (fun f1 f2 -> not (Cil_datatype.Typ.equal f1.ftype f2.ftype))
@@ -6542,7 +6542,7 @@ and doExp local_env
begin
match !pargs with
| [ arg;_ ] ->
- (* Keep all side-effects, including those steming
+ (* Keep all side-effects, including those stemming
from the second argument. This is quite strange but
compliant with GCC's behavior. *)
piscall := false;
@@ -6947,7 +6947,7 @@ and doExp local_env
end
| A.LABELADDR l -> begin (* GCC's taking the address of a label *)
- let l = lookupLabel l in (* To support locallly declared labels *)
+ let l = lookupLabel l in (* To support locally declared labels *)
let addrval =
try H.find gotoTargetHash l
with Not_found -> begin
@@ -8139,7 +8139,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
Kernel.error ~once:true ~current:true
"Variable-sized array cannot have initializer";
let se0 =
- (* add an assertion to ensure the given size is correcly bound:
+ (* add an assertion to ensure the given size is correctly bound:
assert alloca_bounds: 0 < elt_size * array_size <= max_bounds
*)
(se0 +++ (
diff --git a/src/kernel_internals/typing/cfg.ml b/src/kernel_internals/typing/cfg.ml
index 09736aa282281b49b3da184da13daa66e0f07d27..7bb00b18a2bf40f3069be0a750f27fd823c167f2 100644
--- a/src/kernel_internals/typing/cfg.ml
+++ b/src/kernel_internals/typing/cfg.ml
@@ -214,7 +214,7 @@ and cfgStmt (s: stmt) next break cont =
for more information. *)
addBlockSucc t;
cfgBlock t next break cont;
- (* If there are some auxiliary types catched by the clause, the cfg
+ (* If there are some auxiliary types caught by the clause, the cfg
goes from the conversion block to the main block of the catch clause *)
List.iter
(fun (c,b) ->
diff --git a/src/kernel_internals/typing/infer_annotations.ml b/src/kernel_internals/typing/infer_annotations.ml
index 70bf32fe0153806778e30c2e73bc3398131b9673..0cc78b649ac6d0c1c0e26cdc46528917ce01343c 100644
--- a/src/kernel_internals/typing/infer_annotations.ml
+++ b/src/kernel_internals/typing/infer_annotations.ml
@@ -209,7 +209,7 @@ generating default assigns from the prototype"
in
if bhv.b_assigns = WritesAny then
(* case 2.2 : some assigns have to be generated *)
- (* step 2.1: looks at ungarded behaviors and then at complete
+ (* step 2.1: looks at unguarded behaviors and then at complete
behaviors *)
let warn_if_not_builtin explicit_name name orig_name =
if not (is_frama_c_builtin name) then
diff --git a/src/kernel_internals/typing/logic_builtin.ml b/src/kernel_internals/typing/logic_builtin.ml
index 05a8e16d2312c1bfeb28cb34975732e71622fce5..b937d6b16ba370e739635dc593cfc2cdb722894f 100644
--- a/src/kernel_internals/typing/logic_builtin.ml
+++ b/src/kernel_internals/typing/logic_builtin.ml
@@ -188,7 +188,7 @@ let init =
"\\ceil", [], ["x",Lreal], Linteger ;
"\\floor", [], ["x",Lreal], Linteger ;
- (* transcendantal functions *)
+ (* transcendental functions *)
"\\exp", [], ["x",Lreal], Lreal ;
"\\log", [], ["x",Lreal], Lreal ;
"\\log10", [], ["x",Lreal], Lreal ;
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 6dc74339d427ef94120800ba9f3b5801fad7d1ce..4a4e47782cef81faeac32546f5012bb850884bdf 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -570,7 +570,7 @@ let lvEq = VolatileMerging.create_eq_table 111
let mfEq = ModelMerging.create_eq_table 111
(* Sometimes we want to merge synonyms. We keep some tables indexed by names.
- * Each name is mapped to multiple exntries *)
+ * Each name is mapped to multiple entries *)
let vSyn = PlainMerging.create_syn_table 111
let iSyn = PlainMerging.create_syn_table 111
let sSyn = PlainMerging.create_syn_table 111
@@ -865,7 +865,7 @@ let rec combineTypes (what: combineWhat)
if bytesSizeOfInt oldk=bytesSizeOfInt k && isSigned oldk=isSigned k
then
(* the types contain the same sort of values but are not equal.
- For example on x86_16 machep unsigned short and unsigned int. *)
+ For example on x86_16 machdep unsigned short and unsigned int. *)
if rank oldk<rank k then k else oldk
else
(* GCC allows a function definition to have a more precise integer
diff --git a/src/kernel_services/abstract_interp/abstract_interp.ml b/src/kernel_services/abstract_interp/abstract_interp.ml
index 3802bced80dfd3f4b4ba7140a5aa605496209fcc..a2cac39ea1525ff0f2ea1a4be437ac1c6f16d007 100644
--- a/src/kernel_services/abstract_interp/abstract_interp.ml
+++ b/src/kernel_services/abstract_interp/abstract_interp.ml
@@ -613,7 +613,7 @@ module Int = struct
end
-(* Typing constraints are enfored directly in the .mli *)
+(* Typing constraints are enforced directly in the .mli *)
module Rel = struct
include Int
diff --git a/src/kernel_services/abstract_interp/abstract_interp.mli b/src/kernel_services/abstract_interp/abstract_interp.mli
index 910fb6a313c19ac04f65a1f6dbfeaed2da6f442a..212ee51ebd8233b0315de429cf35549eb9f14015 100644
--- a/src/kernel_services/abstract_interp/abstract_interp.mli
+++ b/src/kernel_services/abstract_interp/abstract_interp.mli
@@ -100,7 +100,7 @@ module Make_Hashconsed_Lattice_Set
applied. The [O] module passed as argument is the same as [O] in the
result. It is passed here to avoid having multiple modules calling
[Hptset.Make] on the same argument (which is forbidden by the datatype
- library, and would cause hashconding problems) *)
+ library, and would cause hashconsing problems) *)
module type Collapse = sig val collapse : bool end
diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml
index 687840565435cc9568d5a8da8fe72e538dc36e1f..7d6606e9951992ff1a667d557512e52e5f1ed9f1 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -482,7 +482,7 @@ module LiteralStrings =
(Datatype.Int.Hashtbl)
(Base)
(struct
- let name = "litteral strings"
+ let name = "literal strings"
let dependencies = [ Ast.self ]
let size = 17
end)
diff --git a/src/kernel_services/abstract_interp/base.mli b/src/kernel_services/abstract_interp/base.mli
index d14c7b4f9fac3e52c67d89fc636630bea7faa96f..fed956fefd857d8520bfd20eef62ab5f066c1088 100644
--- a/src/kernel_services/abstract_interp/base.mli
+++ b/src/kernel_services/abstract_interp/base.mli
@@ -43,7 +43,7 @@ type base = private
(** Base for a standard C variable. *)
| CLogic_Var of Cil_types.logic_var * Cil_types.typ * validity
(** Base for a logic variable that has a C type. *)
- | Null (** Base for an addresse like [(int* )0x123] *)
+ | Null (** Base for an address like [(int* )0x123] *)
| String of int (** unique id of the constant string (one per code location)*)
* cstring (** contents of the constant string *)
| Allocated of Cil_types.varinfo * validity
diff --git a/src/kernel_services/abstract_interp/fval.ml b/src/kernel_services/abstract_interp/fval.ml
index 165cb80d8bea1c4a646394daf9e778df028be294..7123f40a4b2b446cd1d2d710336a4537014840c0 100644
--- a/src/kernel_services/abstract_interp/fval.ml
+++ b/src/kernel_services/abstract_interp/fval.ml
@@ -1177,7 +1177,7 @@ let nan_fmod = an_alarm (ANaN "division by zero")
(* Emits a warning if there may be a division by zero.
Raises [Builtin_invalid_domain] if there must be a division by zero.
- Evalutes the function for y ∉ {+0.0,-0.0}. *)
+ Evaluates the function for y ∉ {+0.0,-0.0}. *)
let fmod (FRange.I(b1, e1) as x) (FRange.I(b2, e2) as y) =
let alarms = if contains_a_zero y then nan_fmod else no_alarm in
if is_a_zero y then
diff --git a/src/kernel_services/abstract_interp/fval.mli b/src/kernel_services/abstract_interp/fval.mli
index 9c54ba11aa3e0072edb06067d4439f9e5c8ffe07..abd1cbb4dba2b1b0d3cb56795b104ee8e7a514bc 100644
--- a/src/kernel_services/abstract_interp/fval.mli
+++ b/src/kernel_services/abstract_interp/fval.mli
@@ -30,7 +30,7 @@ module F : sig
type t
val packed_descr : Structural_descr.pack
- val of_float : float -> t (** fails on NaNs, but allows infinites. *)
+ val of_float : float -> t (** fails on NaNs, but allows infinities. *)
val to_float : t -> float
val compare : t -> t -> int
@@ -44,11 +44,11 @@ module F : sig
val next_float : float -> float
(** First double strictly above the argument. Must be called on non-NaN
- floats. Returns +infty on MAX_FLT. Infinites are left unchanged. *)
+ floats. Returns +infty on MAX_FLT. Infinities are left unchanged. *)
val prev_float : float -> float
(** First double strictly below the argument. Must be called on non-NaN
- floats. Returns -infty on -MAX_FLT. Infinites are left unchanged. *)
+ floats. Returns -infty on -MAX_FLT. Infinities are left unchanged. *)
end
type t
@@ -96,7 +96,7 @@ type float_kind =
val next_after : float_kind -> F.t -> F.t -> F.t
(** [inject] creates an abstract float interval.
- Does not handle infinites or NaN.
+ Does not handle infinities or NaN.
Does not enlarge subnormals to handle flush-to-zero modes *)
val inject : F.t -> F.t -> t
@@ -138,7 +138,7 @@ val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
val pretty_overflow: Format.formatter -> t -> unit
(** This pretty-printer does not display -FLT_MAX and FLT_MAX as interval
- bounds. Instead, the specical notation [--.] is used. *)
+ bounds. Instead, the special notation [--.] is used. *)
val hash : t -> int
@@ -236,7 +236,7 @@ val backward_comp_left :
[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
- acount. [op] must be [Eq], [Ne], [Le], [Ge], [Lt] or [Gt] *)
+ account. [op] must be [Eq], [Ne], [Le], [Ge], [Lt] or [Gt] *)
val cast_float_to_double_inverse: t -> t
(** [cast_float_to_double_inverse d] return all possible float32 [f] such that
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index 68df66f7dff6d00876e6a5b0c4e475b7c50c74e3..f65fd0961afa14193ba984076b5836d9a737c212 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -734,7 +734,7 @@ let _modular_inverse a m =
assert (Int.equal Int.one gcd);
x
-(* This function provides solutions to the chinese remainder theorem,
+(* This function provides solutions to the Chinese remainder theorem,
i.e. it finds the solutions x such that:
x == r1 mod m1 && x == r2 mod m2.
diff --git a/src/kernel_services/abstract_interp/lmap.mli b/src/kernel_services/abstract_interp/lmap.mli
index 53caae5a2e77fbf295a291a03a0ce73d7a4c4a7a..406c2cc5a0e7964b237e88e54cdda61675479301 100644
--- a/src/kernel_services/abstract_interp/lmap.mli
+++ b/src/kernel_services/abstract_interp/lmap.mli
@@ -53,7 +53,7 @@ module Make_LOffset
in particular when maintaining canonicity w.r.t. default contents.
It describes the contents [c] of the offsetmap
resulting from [default_offsetmap b]. The possible values are:
- - [Bottom] means that [c] is [V.bottom] everywhere, and furthemore
+ - [Bottom] means that [c] is [V.bottom] everywhere, and furthermore
that [V.bottom] has an empty concretization. We deduce from this
fact that unmapped keys do not contribute to a join, and that
[join c v] is never [c] as soon as [v] is not itself [v].
diff --git a/src/kernel_services/abstract_interp/lmap_sig.mli b/src/kernel_services/abstract_interp/lmap_sig.mli
index ce2d2440cc39544ae06f7ec847daa71750756a38..70e647bb95be0a992783e4d736574b7e69fbf242 100644
--- a/src/kernel_services/abstract_interp/lmap_sig.mli
+++ b/src/kernel_services/abstract_interp/lmap_sig.mli
@@ -91,7 +91,7 @@ val copy_offsetmap :
bool * offsetmap Bottom.or_bottom
(** [copy_offsetmap alarms loc size m] returns the superposition of the
ranges of [size] bits starting at [loc] within [m]. [size] must be strictly
- greater than zero. Return [None] if all pointed adresses are invalid in [m].
+ greater than zero. Return [None] if all pointed addresses are invalid in [m].
The boolean returned indicates that the location may be invalid.
@raise Error_Top when the location or the state are Top, and there
@@ -165,7 +165,7 @@ val remove_base : Base.t -> t -> t
(** Notice that some iterators require an argument of type {!map}: the
cases {!Top} and {!Bottom} must be handled separately. All the iterators
- belowonly present bases that are bound to non-default values, according
+ below only present bases that are bound to non-default values, according
to the function [is_default_offsetmap] of the function {!Lmap.Make_Loffset}.
*)
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index 46cf3d735a93f02786b05d8ec94e77b7b2f7c606..24115a3dd7c7210548701dbb31b8ab2491c1e72a 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -79,7 +79,7 @@ type 'a offsetmap =
* otherwise, two truncated instances of the value are stored
consecutively.
- strictly less than [max+1]: the value is stored more than once,
- and implictly repeats itself to fill the entire interval. *) *
+ and implicitly repeats itself to fill the entire interval. *) *
int
(** tag: hash-consing id of the node, plus an additional boolean.
Not related to the contents of the tree. *)
@@ -746,7 +746,7 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
(** Inclusion functions *)
- (* Auxiliary fonction for inclusion: check that, between [mabs_min] and
+ (* Auxiliary function for inclusion: check that, between [mabs_min] and
[mabs_max], the values (r1, m1, v1) and (r2, m2, v2), respectively
bound between (amin1, amax1) and (amin2, amax2), are included. *)
let is_included_nodes_values (amin1 : Integer.t) (amax1 : Integer.t) r1 m1 v1 amin2 amax2 r2 m2 v2 mabs_min mabs_max =
@@ -1998,7 +1998,7 @@ let update_under ~validity ~exact ~offsets ~size v t =
else
(* This is a struct or an array. Either the result will be imprecise
because catenating semi-imprecise values through merge_bits
- wil result in something really imprecise at the end, or we will
+ will result in something really imprecise at the end, or we will
build very big integers, which is not really helpful either. *)
find_imprecise_between (Int.zero, Int.pred size) src
in
diff --git a/src/kernel_services/abstract_interp/offsetmap_sig.mli b/src/kernel_services/abstract_interp/offsetmap_sig.mli
index 1eec8a7d9529ece4a54fe8c4cc06de5100de7b49..12b9eece32990cef98fe6fa1888281f23dae8136 100644
--- a/src/kernel_services/abstract_interp/offsetmap_sig.mli
+++ b/src/kernel_services/abstract_interp/offsetmap_sig.mli
@@ -138,7 +138,7 @@ type map2_decide =
val map2_on_values:
Hptmap_sig.cache_type -> (t -> t -> map2_decide) -> (v -> v -> v) -> t -> t -> t
(** [map2_on_values cache decide join m1 m2] applies [join] pointwise to
- all the elements of [m1] and [m2] and buils the resulting map. This function
+ all the elements of [m1] and [m2] and builds the resulting map. This function
can only be called if [m1] and [m2] contain isotropic values. [decide]
is called during the iteration, and can be used to return early; it is
always correct to return {!Recurse}. Depending on [cache], the results of
@@ -214,7 +214,7 @@ val update :
of size [size], each [offsets] in [m]; [m] must be of the size implied by
[validity]. [~exact=true] results in a strong update, while
[~exact=false] performs a weak update. If [offsets] contains too many
- offsets, or if [offsers] and [size] are not compatible, [offsets] and/or
+ offsets, or if [offsets] and [size] are not compatible, [offsets] and/or
[v] are over-approximated. In this case, [origin] is used as the source of
the resulting imprecision. Returns [`Bottom] when all offsets are invalid.
The boolean returned indicates a potential alarm. *)
diff --git a/src/kernel_services/abstract_interp/origin.mli b/src/kernel_services/abstract_interp/origin.mli
index 1549309d2381e8af4e5d6acdf6512eb16c7ca5bf..537bcbf8dd1e447e91c85282a77bdca5e9ffb3d2 100644
--- a/src/kernel_services/abstract_interp/origin.mli
+++ b/src/kernel_services/abstract_interp/origin.mli
@@ -40,7 +40,7 @@ end
source locations where the operation took place. *)
type origin =
| Misalign_read of LocationSetLattice.t (** Read of not all the bits of a
- pointer, typicaller through a pointer cast *)
+ pointer, typically through a pointer cast *)
| Leaf of LocationSetLattice.t (** Result of a function without a body *)
| Merge of LocationSetLattice.t (** Join between two control-flows *)
| Arith of LocationSetLattice.t (** Arithmetic operation that cannot be
diff --git a/src/kernel_services/analysis/bit_utils.ml b/src/kernel_services/analysis/bit_utils.ml
index a175dffbd2bfa906e2a55f1467957dfef49365a2..a61a9d5b76fa18ad467b7076e45b89c36d63df70 100644
--- a/src/kernel_services/analysis/bit_utils.ml
+++ b/src/kernel_services/analysis/bit_utils.ml
@@ -243,7 +243,7 @@ let rec pretty_bits_internal env bfinfo typ ~align ~start ~stop =
if (not env.use_align) && Integer.compare req_size size = 0
then
update_types typ (* do not print sub-fields if the size is exactly
- the right one and the alignement is not important *)
+ the right one and the alignment is not important *)
else begin
try
let full_fields_to_print = List.fold_left
@@ -461,7 +461,7 @@ type offset_match =
| MatchSize of Integer.t
| MatchFirst
-(* Comparaison of the shape of two types. Attributes are completely ignored. *)
+(* Comparison of the shape of two types. Attributes are completely ignored. *)
let rec equal_type_no_attribute t1 t2 =
match Cil.unrollType t1, Cil.unrollType t2 with
| TVoid _, TVoid _ -> true
diff --git a/src/kernel_services/analysis/dataflow.ml b/src/kernel_services/analysis/dataflow.ml
index 0f32f243ea5bc82263f5468fe0fe5c99a6075e18..d65f32ff4c0cc00ee944af5af3690dd8320e25f7 100644
--- a/src/kernel_services/analysis/dataflow.ml
+++ b/src/kernel_services/analysis/dataflow.ml
@@ -627,7 +627,7 @@ struct
(** Helper utility that finds all of the statements of a function.
- It also lists the return statments (including statements that
+ It also lists the return statements (including statements that
fall through the end of a void function). Useful when you need an
initial set of statements for BackwardsDataFlow.compute. *)
let sinkFinder sink_stmts all_stmts = object
diff --git a/src/kernel_services/analysis/dataflow.mli b/src/kernel_services/analysis/dataflow.mli
index 802f0605e28eed44f2e1451de1340ccafcd4ff7d..94421fdc2a3a6b9ca0d5baa7b3b11c3a4bfa7839 100644
--- a/src/kernel_services/analysis/dataflow.mli
+++ b/src/kernel_services/analysis/dataflow.mli
@@ -254,7 +254,7 @@ end
val find_stmts: Cil_types.fundec -> (Cil_types.stmt list * Cil_types.stmt list)
(** @return (all_stmts, sink_stmts), where all_stmts is a list of the statements
- in a function, and sink_stmts is a list of the return statments (including
+ in a function, and sink_stmts is a list of the return statements (including
statements that fall through the end of a void function). Useful when you
need an initial set of statements for BackwardsDataFlow.compute. *)
diff --git a/src/kernel_services/analysis/dataflow2.ml b/src/kernel_services/analysis/dataflow2.ml
index 4286d8ec203afa820e85f148fef8048d3e4a5146..5fbca66581c1092810a61c6d2cd328c78751a10c 100644
--- a/src/kernel_services/analysis/dataflow2.ml
+++ b/src/kernel_services/analysis/dataflow2.ml
@@ -95,7 +95,7 @@ module type WORKLIST = sig
(** Remove a statement from the worklist. *)
val clear: t -> stmt -> unit
-(** Tells wheter a statement is in the worklist or not. *)
+(** Tells whether a statement is in the worklist or not. *)
val mem : t -> stmt -> bool
@@ -233,7 +233,7 @@ module Worklist(MaybeReverse:MAYBE_REVERSE):WORKLIST = struct
(* We reached the end of the current connex component. The
trick is that OCamlgraph's topological ordering guarantee
that elements of the same connex component have
- congiguous indexes, so we know that we have reached the
+ contiguous indexes, so we know that we have reached the
end of the current connex component. Check if we should
start over in the same connex component, or continue to
the next cc. *)
@@ -243,7 +243,7 @@ module Worklist(MaybeReverse:MAYBE_REVERSE):WORKLIST = struct
| Some(i) -> restart_from i)
with Not_found ->
(* We found no further work, but it could be because the graph
- ends with a non-trival connex component (e.g. the function
+ ends with a non-trivial connex component (e.g. the function
ends with a loop). *)
(match t.must_restart_cc with
| None -> raise Empty
@@ -391,7 +391,7 @@ module Forwards(T : ForwardsTransfer) = struct
| Switch (exp_sw, _, _, _) ->
let cases, default = Cil.separate_switch_succs s in
- (* Auxiliary function that iters on all the labels of
+ (* Auxiliary function that iterates on all the labels of
the switch. The accumulator is the state after the
evaluation of the label, and the default case *)
let iter_all_labels f =
@@ -504,7 +504,7 @@ module Forwards(T : ForwardsTransfer) = struct
let compute_strategy (sources: stmt list) (strategy : Wto_statement.wto) =
check_initial_stmts sources;
let worklist = init_worklist sources in
- (* the reference "change" tracks wether something has been computed *)
+ (* the reference "change" tracks whether something has been computed *)
let rec process_wto change wto =
List.iter (process_element change) wto
and process_element change = function
@@ -667,7 +667,7 @@ struct
(** Helper utility that finds all of the statements of a function.
- It also lists the return statments (including statements that
+ It also lists the return statements (including statements that
fall through the end of a void function). Useful when you need an
initial set of statements for BackwardsDataFlow.compute. *)
let sinkFinder sink_stmts all_stmts = object
diff --git a/src/kernel_services/analysis/dataflow2.mli b/src/kernel_services/analysis/dataflow2.mli
index 254c13ec36e0cd2292b158be029a2d439e53ce77..afe2a006914f28bdec926e6aa8cb2d5ad8d15f80 100644
--- a/src/kernel_services/analysis/dataflow2.mli
+++ b/src/kernel_services/analysis/dataflow2.mli
@@ -213,7 +213,7 @@ end
val find_stmts: Cil_types.fundec -> (Cil_types.stmt list * Cil_types.stmt list)
(** @return (all_stmts, sink_stmts), where all_stmts is a list of the statements
- in a function, and sink_stmts is a list of the return statments (including
+ in a function, and sink_stmts is a list of the return statements (including
statements that fall through the end of a void function). Useful when you
need an initial set of statements for BackwardsDataFlow.compute. *)
diff --git a/src/kernel_services/analysis/dataflows.mli b/src/kernel_services/analysis/dataflows.mli
index a9c785b5f642a1010ec39b88f8d3d99296d78e7a..f3afd2f3d4bb375de5e025a2199049085cf8d9c5 100644
--- a/src/kernel_services/analysis/dataflows.mli
+++ b/src/kernel_services/analysis/dataflows.mli
@@ -47,7 +47,7 @@
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
+ dataflows. Simpler-to-instantiate dataflows are instances of the
more general dataflows. *)
open Cil_types;;
@@ -125,7 +125,7 @@ module Simple_backward(Fenv:FUNCTION_ENV)(P:BACKWARD_MONOTONE_PARAMETER) : sig
val post_state: stmt -> P.t
val pre_state: stmt -> P.t
(** This function calls [transfer_stmt] on the result of [post_state]. Beware
- if [transfert_stmt] is impure or costly *)
+ if [transfer_stmt] is impure or costly *)
(** {3 Iterations on the results of the dataflow.}
@@ -184,7 +184,7 @@ module Simple_forward(Fenv:FUNCTION_ENV)(P:FORWARD_MONOTONE_PARAMETER) : sig
val pre_state: stmt -> P.t
val post_state: stmt -> P.t
(** This function calls [transfer_stmt] on the result of [pre_state]. Beware
- if [transfert_stmt] is impure or costly *)
+ if [transfer_stmt] is impure or costly *)
(** {3 Iterations on the results of the dataflow.}
diff --git a/src/kernel_services/analysis/loop.ml b/src/kernel_services/analysis/loop.ml
index 1ea3490675c133ca0c67b1815fec6af58cdf65d8..5a774ef161c32f36586bb90197dcde1bdcfd35e3 100644
--- a/src/kernel_services/analysis/loop.ml
+++ b/src/kernel_services/analysis/loop.ml
@@ -42,7 +42,7 @@ let pretty_natural_loops fmt loops =
Format.fprintf fmt ")@\n";)
loops
-(** Compute the start of the natural loops of the fonction. For each start,
+(** Compute the start of the natural loops of the function. For each start,
we also return the origins of the back edges. *)
let findNaturalLoops (f: fundec) =
let loops =
diff --git a/src/kernel_services/analysis/ordered_stmt.mli b/src/kernel_services/analysis/ordered_stmt.mli
index a745f0beec041e57a10b91a27d1dbcd2d1fc064e..cab45617cfe599bbf3c937da95b726c1843bc83d 100644
--- a/src/kernel_services/analysis/ordered_stmt.mli
+++ b/src/kernel_services/analysis/ordered_stmt.mli
@@ -23,7 +23,7 @@
open Cil_types
(** An [ordered_stmt] is an int representing a stmt in a particular
- function. They are sorted by the topological orderering of
+ function. They are sorted by the topological ordering of
stmts (s1 < s2 if s1 precedes s2, or s2 does not precede s1); they
are contiguous and start from 0.
diff --git a/src/kernel_services/analysis/stmts_graph.mli b/src/kernel_services/analysis/stmts_graph.mli
index 5317836b7c0829b3eb21eb09f5357684dab29ecb..0d2e5af1916d5064e50ff12f470b65845bffbfe6 100644
--- a/src/kernel_services/analysis/stmts_graph.mli
+++ b/src/kernel_services/analysis/stmts_graph.mli
@@ -36,7 +36,7 @@ val stmt_can_reach_filtered : (stmt -> bool) -> stmt -> stmt -> bool
on its input *)
val stmt_is_in_cycle : stmt -> bool
- (** [stmt_is_in_cycle s] is [true] iff [s] is reachable through a non trival path
+ (** [stmt_is_in_cycle s] is [true] iff [s] is reachable through a non trivial path
* starting at [s]. *)
val stmt_is_in_cycle_filtered : (stmt -> bool) -> stmt -> bool
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index 9743197b2e77944054a1d06ceb3f4c7b3a6cee61..16c3e1322617aa3dcc5df25083bcc65ff1b67f0b 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -623,7 +623,7 @@ let to_annot_aux kinstr ?(loc=Kinstr.loc kinstr) alarm =
let by_emitter = State.find kinstr in
match find_alarm_in_emitters by_emitter alarm with
| None ->
- (* somes alarms already associated to this [kinstr],
+ (* some alarms already associated to this [kinstr],
but not this [alarm] *)
add alarm, true, by_emitter
| Some (annot, _kf, _stmt, _) ->
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index 8c8aae8c93a85f8fc8eafbfb8c798ad412a62717..78f1c02e4fe0eaa8ce73da33d143d9338a00c8f9 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -847,7 +847,7 @@ let add_behaviors ?(register_children=true) e kf ?stmt ?active bhvs =
Thus, if register_children is true, we need to update
the property status table.
For the other clauses (requires, assumes, ensures) we just need to
- add the additional ip, nothing whill be removed.
+ add the additional ip, nothing will be removed.
*)
if register_children then begin
let ip = Property.ip_from_of_behavior kf ki active bhv in
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 6e1c769e6e2445f28883994b6d9758b92e020a65..42b0721eb660316824c0776fdaffbcd7849fd77e 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -51,7 +51,7 @@
(* A first test to see if something has been broken by a change is to launch*)
(* ptests.byte -add-options '-files-debug "-check -copy"' *)
(* In addition, it is a good idea to add some invariant checks in the *)
-(* check_file class in frama-c/src/file.ml (before lauching the tests) *)
+(* check_file class in frama-c/src/file.ml (before launching the tests) *)
(****************************************************************************)
(* ************************************************************************* *)
@@ -1501,7 +1501,7 @@ and predicate_node =
(** the pointed function has a type compatible with the one of pointer. *)
| Pinitialized of logic_label * term (** the given locations are initialized. *)
| Pdangling of logic_label * term (** the given locations contain dangling
- adresses. *)
+ addresses. *)
| Pallocable of logic_label * term (** the given locations can be allocated. *)
| Pfreeable of logic_label * term (** the given locations can be free. *)
| Pfresh of logic_label * logic_label * term * term
diff --git a/src/kernel_services/ast_data/globals.ml b/src/kernel_services/ast_data/globals.ml
index a96082ded5f8d477e1990b3a7b7ad04653328bfb..ce9e69ee92917d332aa4cc02653b4d895d56aa35 100644
--- a/src/kernel_services/ast_data/globals.ml
+++ b/src/kernel_services/ast_data/globals.ml
@@ -145,7 +145,7 @@ module Functions = struct
let self = State.self
(* Maintain an alphabetical ordering of the functions, so that
- iteration stays independent from vid numerotation scheme. *)
+ iteration stays independent from vid numbering scheme. *)
module VarinfoAlphaOrderSet = struct
let compare_alpha x y =
let res = String.compare x.vname y.vname in
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 9e73d1630d1c07504713df490c70e8fbcb4f8262..6d4f25e3bad671251ea28a6b1c7e8dc8e5796eb7 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -701,7 +701,7 @@ module Names = struct
| IPOther(s,Some kf,ki) -> (kf_prefix kf) ^ (ki_prefix ki) ^ s
| IPOther(s,None,ki) -> (ki_prefix ki) ^ s
- (** function used to normanize basename *)
+ (** function used to normalize basename *)
let normalize_basename s =
let is_valid_char_id = function
| 'a'..'z' | 'A' .. 'Z' | '0' .. '9' | '_' -> true
diff --git a/src/kernel_services/ast_data/property_status.mli b/src/kernel_services/ast_data/property_status.mli
index 36d6ede6ec6c68d4d88a9174bf68eac4bc18f854..8e8bb08ea3f7e4c530537840bdb4593cc53ac63a 100644
--- a/src/kernel_services/ast_data/property_status.mli
+++ b/src/kernel_services/ast_data/property_status.mli
@@ -152,7 +152,7 @@ module Consolidation: sig
The argument is for internal use only *)
| Considered_valid
- (** Nobody succeeds to verifiy the property, but it is expected to be
+ (** Nobody succeeds to verify the property, but it is expected to be
verified by another way (manual review, ...) *)
| Valid of Emitter.Usable_emitter.Set.t
@@ -246,7 +246,7 @@ val register: Property.t -> unit
(** Register the given property. It must not be already registered. *)
val register_property_add_hook: (Property.t -> unit) -> unit
-(** add an hook that will be called for any newly registred property
+(** add an hook that will be called for any newly registered property
@since Neon-20140301 *)
val remove: Property.t -> unit
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 22596985ebd9c6bb5ca59a03e4926745101b1c55..2b9d94d4d776ddacbdcaf46e8dc1c453aafcaaf6 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1409,7 +1409,7 @@ class cil_printer () = object (self)
(* If the function has attributes then print a prototype because
* GCC cannot accept function attributes in a definition *)
let oldattr = fundec.svar.vattr in
- (* Always pring the file name before function declarations *)
+ (* Always print the file name before function declarations *)
(* Prototype first *)
if oldattr <> [] then
(self#line_directive fmt l;
@@ -1853,7 +1853,7 @@ class cil_printer () = object (self)
true
| s, _ when s = Cil.bitfield_attribute_name && not state.print_cil_as_is ->
false
- | _ -> (* This is the dafault case *)
+ | _ -> (* This is the default case *)
(* Add underscores to the name *)
let an' =
if Cil.msvcMode () then "__" ^ an else "__" ^ an ^ "__"
@@ -1941,7 +1941,7 @@ class cil_printer () = object (self)
else fprintf fmt " __attribute__((";
Pretty_utils.pp_list ~sep:",@ "
Format.pp_print_string fmt in__attr__;
- if not block (* reversed so that hightlighting matches *)
+ if not block (* reversed so that highlighting matches *)
then fprintf fmt "))"
else fprintf fmt ") %s" (for_cil "*/")
end
diff --git a/src/kernel_services/ast_printing/cprint.ml b/src/kernel_services/ast_printing/cprint.ml
index 22a9049ebbc970afc0ede106d87c868bf6d22d2a..a104d412d42c5426497396298c2bde823a858094 100644
--- a/src/kernel_services/ast_printing/cprint.ml
+++ b/src/kernel_services/ast_printing/cprint.ml
@@ -237,7 +237,7 @@ and print_struct_name_attr keyword fmt (name, extraAttrs) =
(pp_cond (extraAttrs <> [])) "@ "
print_attributes extraAttrs name
-(* This is the main printer for declarations. It is easy bacause the
+(* This is the main printer for declarations. It is easy because the
* declarations are laid out as they need to be printed. *)
and print_decl (n: string) fmt = function
JUSTBASE ->
diff --git a/src/kernel_services/ast_printing/description.mli b/src/kernel_services/ast_printing/description.mli
index 36313bba3a99878f052f9e0fe8f8e78001089dc5..c466144f9ade2b2d98e80b0ace49887636b9177a 100644
--- a/src/kernel_services/ast_printing/description.mli
+++ b/src/kernel_services/ast_printing/description.mli
@@ -45,7 +45,7 @@ val pp_for : Format.formatter -> string list -> unit
(** prints nothing or " for 'b1,...,bn'" *)
val pp_bhv : Format.formatter -> funbehavior -> unit
-(** prints nothing for default behavior, and " for 'b'" otherwize *)
+(** prints nothing for default behavior, and " for 'b'" otherwise *)
val pp_property : Format.formatter -> Property.t -> unit
(** prints an identified property *)
diff --git a/src/kernel_services/ast_printing/printer_api.mli b/src/kernel_services/ast_printing/printer_api.mli
index 3eba911e6ddd076409a2e5699100d1f0220e7cf1..765b782f4da57a4fed26cd55c59637e474c0310f 100644
--- a/src/kernel_services/ast_printing/printer_api.mli
+++ b/src/kernel_services/ast_printing/printer_api.mli
@@ -324,7 +324,7 @@ type state =
(** Whether to print the CIL as they are, without trying to be smart and
print nicer code. Normally this is false, in which case the pretty
printer will turn the while(1) loops of CIL into nicer loops, will not
- print empty "else" blocks, etc. These is one case howewer in which if
+ print empty "else" blocks, etc. These is one case however in which if
you turn this on you will get code that does not compile: if you use
varargs the __builtin_va_arg function will be printed in its internal
form. *)
diff --git a/src/kernel_services/ast_queries/ast_info.ml b/src/kernel_services/ast_queries/ast_info.ml
index 54d5fb2bbc5fe2d4d25ca2da73155f3df2ae05d1..971bf4404e386d768d8a50c4c9319008dfa63bbb 100644
--- a/src/kernel_services/ast_queries/ast_info.ml
+++ b/src/kernel_services/ast_queries/ast_info.ml
@@ -186,8 +186,8 @@ let merge_assigns_internal (get:'b -> 'c assigns) (origin:'b -> string list)
in List.fold_left (* find the smallest one *)
cmp_assigns acc bhvs
-(** Returns the assigns from complete behaviors and ungarded behaviors. *)
-let merge_assigns_from_complete_bhvs ?warn ?(ungarded=true) bhvs complete_bhvs =
+(** Returns the assigns from complete behaviors and unguarded behaviors. *)
+let merge_assigns_from_complete_bhvs ?warn ?(unguarded=true) bhvs complete_bhvs =
let merge_assigns_from_complete_bhvs bhv_names =
try (* For merging assigns of a "complete" set of behaviors *)
let behaviors = match bhv_names with
@@ -201,7 +201,7 @@ let merge_assigns_from_complete_bhvs ?warn ?(ungarded=true) bhvs complete_bhvs =
in
(* Merges the assigns of the complete behaviors.
Once one of them as no assumes, that means the merge
- of the ungarded behavior did already the job *)
+ of the unguarded behavior did already the job *)
Writes
(List.fold_left
(fun acc b -> match b.b_assigns with
@@ -212,9 +212,9 @@ let merge_assigns_from_complete_bhvs ?warn ?(ungarded=true) bhvs complete_bhvs =
WritesAny
in
let acc =
- if ungarded then (* Looks first at unguarded behaviors. *)
+ if unguarded then (* Looks first at unguarded behaviors. *)
let unguarded_bhvs = List.filter (fun b -> b.b_assumes = []) bhvs
- in merge_assigns_internal (* Chooses the smalest one *)
+ in merge_assigns_internal (* Chooses the smallest one *)
(fun b -> b.b_assigns) (fun b -> [b.b_name])
None unguarded_bhvs
else None
@@ -225,7 +225,7 @@ let merge_assigns_from_complete_bhvs ?warn ?(ungarded=true) bhvs complete_bhvs =
acc
| _ ->
(* Look at complete behaviors *)
- merge_assigns_internal (* Chooses the smalest one *)
+ merge_assigns_internal (* Chooses the smallest one *)
merge_assigns_from_complete_bhvs
(fun bhvnames -> bhvnames)
acc
@@ -248,7 +248,7 @@ let merge_assigns_from_complete_bhvs ?warn ?(ungarded=true) bhvs complete_bhvs =
end;
a
-(** Returns the assigns from complete behaviors and ungarded behaviors. *)
+(** Returns the assigns from complete behaviors and unguarded behaviors. *)
let merge_assigns_from_spec ?warn (spec :funspec) =
merge_assigns_from_complete_bhvs
?warn spec.spec_behavior spec.spec_complete_behaviors
diff --git a/src/kernel_services/ast_queries/ast_info.mli b/src/kernel_services/ast_queries/ast_info.mli
index a1500650ff6438c31dcc720c48b3a573a0978e6e..c68e4c0a8dcc0091f2e5548469a459a75197e5da 100644
--- a/src/kernel_services/ast_queries/ast_info.mli
+++ b/src/kernel_services/ast_queries/ast_info.mli
@@ -90,8 +90,8 @@ val complete_behaviors : funspec -> string list -> predicate
@since Nitrogen-20111001 *)
val merge_assigns_from_complete_bhvs:
- ?warn:bool -> ?ungarded:bool -> funbehavior list -> string list list -> identified_term assigns
- (** @return the assigns of an unguarded behavior (when [ungarded]=true)
+ ?warn:bool -> ?unguarded:bool -> funbehavior list -> string list list -> identified_term assigns
+ (** @return the assigns of an unguarded behavior (when [unguarded]=true)
or a set of complete behaviors.
- the funbehaviors can come from either a statement contract or a function
contract.
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index f7401b5733b4bb475815f2ddcb707a0e20477ca7..77ae52aa0d0af8c3b93e469d7b5dab16b0be7123 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -44,7 +44,7 @@
(* Modified by TrustInSoft *)
(*
- * CIL: An intermediate language for analyzing C progams.
+ * CIL: An intermediate language for analyzing C programs.
*
* Version Tue Dec 12 15:21:52 PST 2000
* Scott McPeak, George Necula, Wes Weimer
@@ -1518,7 +1518,7 @@ let copy_visit_gen fresh prj =
try Cil_datatype.Fieldinfo.Hashtbl.find fieldinfos x
with Not_found ->
let _ = temp_memo_compinfo x.fcomp in
- (* memo_compinfo fills the field correspondance table as well *)
+ (* memo_compinfo fills the field correspondence table as well *)
let new_x = Cil_datatype.Fieldinfo.Hashtbl.find fieldinfos x in
Cil_datatype.Fieldinfo.Hashtbl.add fieldinfos x new_x;
Cil_datatype.Fieldinfo.Hashtbl.add orig_fieldinfos new_x x;
@@ -1734,7 +1734,7 @@ class type cilVisitor = object
(** Attribute parameters. *)
(** Add here instructions while visiting to queue them to
- * preceede the current statement or instruction being processed *)
+ * precede the current statement or instruction being processed *)
method queueInstr: instr list -> unit
(** Gets the queue of instructions and resets the queue *)
@@ -4537,7 +4537,7 @@ let isCharPtrType t =
(* Hack to prevent infinite recursion in alignments *)
let ignoreAlignmentAttrs = ref false
- (* Get the minimum aligment in bytes for a given type *)
+ (* Get the minimum alignment in bytes for a given type *)
let rec bytesAlignOf t =
let alignOfType () = match t with
| TInt((IChar|ISChar|IUChar|IBool), _) -> 1
@@ -4561,7 +4561,7 @@ let rec bytesAlignOf t =
(* On GCC the zero-width fields do not contribute to the alignment. On
* MSVC only those zero-width that _do_ appear after other
* bitfields contribute to the alignment. So we drop those that
- * do not occur after othe bitfields *)
+ * do not occur after other bitfields *)
(* This is not correct for Diab-C compiler. *)
let rec dropZeros (afterbitfield: bool) = function
| f :: rest when f.fbitfield = Some 0 && not afterbitfield ->
@@ -5317,7 +5317,7 @@ let intTypeIncluded kind1 kind2 =
(* CEA: moved from cabs2cil.ml. See cil.mli for infos *)
(* Weimer
* multi-character character constants
- * In MSCV, this code works:
+ * In MSVC, this code works:
*
* long l1 = 'abcd'; // note single quotes
* char * s = "dcba";
@@ -6826,7 +6826,7 @@ let mkCastT ?(force=false) ~(e: exp) ~(oldt: typ) ~(newt: typ) =
end
let lenOfArray eo = Integer.to_int (lenOfArray64 eo)
-(*** Make an initializer for zeroe-ing a data type ***)
+(*** Make an initializer for zeroing a data type ***)
let rec makeZeroInit ~loc (t: typ) : init =
match unrollType t with
TInt (ik, _) ->
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 37629dee94cc5a9f4c4d94f88017375bd722e36f..c494e12c6a7fb9f8320cb8e55d7f13ca6946b35d 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -201,12 +201,12 @@ val setFormalsDecl: varinfo -> typ -> unit
@since Oxygen-20120901 *)
val removeFormalsDecl: varinfo -> unit
-(** replace to formals of a function declaration with the given
+(** replace formals of a function declaration with the given
list of varinfo.
*)
val unsafeSetFormalsDecl: varinfo -> varinfo list -> unit
-(** iters the given function on declared prototypes.
+(** iterate the given function on declared prototypes.
@since Oxygen-20120901
*)
val iterFormalsDecl: (varinfo -> varinfo list -> unit) -> unit
@@ -629,7 +629,7 @@ val splitFunctionTypeVI:
[vtemp] field in type {!Cil_types.varinfo}.
The [source] argument defaults to [true], and corresponds to the field
[vsource] .
- The first unnmamed argument specifies whether the varinfo is for a global and
+ The first unnamed argument specifies whether the varinfo is for a global and
the second is for formals. *)
val makeVarinfo:
?source:bool -> ?temp:bool -> bool -> bool -> string -> typ -> varinfo
@@ -771,7 +771,7 @@ val isConstant: exp -> bool
(** True if the expression is a compile-time integer constant *)
val isIntegerConstant: exp -> bool
-(** True if the given offset contains only field nanmes or constant indices. *)
+(** True if the given offset contains only field names or constant indices. *)
val isConstantOffset: offset -> bool
(** True if the given expression is a (possibly cast'ed) integer or character
@@ -794,7 +794,7 @@ val interpret_character_constant:
(** Given the character c in a (CChr c), sign-extend it to 32 bits.
(This is the official way of interpreting character constants, according to
ISO C 6.4.4.4.10, which says that character constants are chars cast to ints)
- Returns CInt64(sign-extened c, IInt, None) *)
+ Returns CInt64(sign-extended c, IInt, None) *)
val charConstToInt: char -> Integer.t
val charConstToIntConstant: char -> constant
@@ -1582,14 +1582,14 @@ class type cilVisitor = object
(** Attribute parameters. *)
method queueInstr: instr list -> unit
- (** Add here instructions while visiting to queue them to preceede the
+ (** Add here instructions while visiting to queue them to precede the
current statement or instruction being processed. Use this method only
when you are visiting an expression that is inside a function body, or a
statement, because otherwise there will no place for the visitor to place
your instructions. *)
(** Gets the queue of instructions and resets the queue. This is done
- automatically for you when you visit statments. *)
+ automatically for you when you visit statements. *)
method unqueueInstr: unit -> instr list
method current_stmt: stmt option
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 29bb1b0327e12bd644be4f26abac3b1b75315dcb..63bae4b6608f636a5b6e4f3d4fa9187da21dcf1a 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -244,11 +244,11 @@ let rec aux loc =
let singleton_coerce =
{ t with term_node = TLogic_coerce(nset, t); term_type = nset }
in
- (* see wether we have to coerce the set type itself. *)
+ (* see whether we have to coerce the set type itself. *)
if is_same_type oset nset then singleton_coerce
else { loc with term_node = TLogic_coerce(oset, singleton_coerce) }
(* if we a term of type set, try to apply f to each
- element of x by using a comprehension, and see wether we can get
+ element of x by using a comprehension, and see whether we can get
rid of said comprehension afterwards. *)
| _ when is_set_type loc.term_type ->
let elt_type = type_of_set_elem loc.term_type in
@@ -3540,7 +3540,7 @@ let add_label info lab =
let rec multiple_post_clauses_state_env l =
match l with
| [] -> env
- | [x] -> post_state_env x (* Usuual case*)
+ | [x] -> post_state_env x (* Usual case*)
(* The two cases below are used in the ACSL importer plugin *)
| (Returns|Normal)::r ->
diff --git a/src/kernel_services/ast_transformations/filter.mli b/src/kernel_services/ast_transformations/filter.mli
index 15a1a1db57e2c9088ba6482b025f399f6c4df64f..f3099e23a024e40cbbf90a59b9c90445387b8f0d 100644
--- a/src/kernel_services/ast_transformations/filter.mli
+++ b/src/kernel_services/ast_transformations/filter.mli
@@ -119,7 +119,7 @@ module type RemoveInfo = sig
*)
val result_visible : kernel_function -> fct -> bool
- (** [cond_edge_visible f s] emplies that [s] is an 'if' in [f]. The
+ (** [cond_edge_visible f s] implies that [s] is an 'if' in [f]. The
first returned boolean indicates that the 'then' edge is useful,
the second one the 'else' is. Setting one or both to true will
lead to the simplification in the 'if'. *)
diff --git a/src/kernel_services/cmdline_parameters/cmdline.mli b/src/kernel_services/cmdline_parameters/cmdline.mli
index 95f0fb8ccd39b194b3c51cd3c9fdd8af108f4f25..695210545decf74dac328189e622ed4e1881cfa4 100644
--- a/src/kernel_services/cmdline_parameters/cmdline.mli
+++ b/src/kernel_services/cmdline_parameters/cmdline.mli
@@ -382,7 +382,7 @@ val quiet: bool
val deterministic: bool
(** Indicates that the plugins should strive to be as deterministic as
possible in their outputs. Higher memory consumption or analysis time
- are acceptable, as reproductibility is more important.
+ are acceptable, as reproducibility is more important.
@since Aluminium-20160501 *)
val last_project_created_by_copy: (unit -> string option) ref
diff --git a/src/kernel_services/cmdline_parameters/parameter_builder.ml b/src/kernel_services/cmdline_parameters/parameter_builder.ml
index 042adcfedfd569baf574feb1ba713776e27eeb3b..2da9ef02340b81d5cd85b7223a714326ebdb56c1 100644
--- a/src/kernel_services/cmdline_parameters/parameter_builder.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_builder.ml
@@ -637,7 +637,7 @@ struct
| '\\', (Start | Word _) -> read_char_in_word (fun x -> x) Escaped
| ',', (Start | Word _) -> read_char_in_word (fun x -> x) Start
| (' ' | '\t' | '\n' | '\r'), Start ->
- (* ignore whitespaces at beginnning of words (must be escaped) *)
+ (* ignore whitespace at beginning of words (must be escaped) *)
aux acc pos next s
| '@', (Start | Word true) when use_category ->
read_char_in_word set_category_flag (Word false)
diff --git a/src/kernel_services/cmdline_parameters/parameter_customize.mli b/src/kernel_services/cmdline_parameters/parameter_customize.mli
index 6534b9ba715659d01e5250b398675676aa00daab..933cf5214e6b6653639fca74428cc0f184f114e9 100644
--- a/src/kernel_services/cmdline_parameters/parameter_customize.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_customize.mli
@@ -22,7 +22,7 @@
(** Configuration of command line options.
- You can apply the below functions juste before applying one of the functors
+ You can apply the functions below just before applying one of the functors
provided by the functor {!Plugin.Register} and generating a new
parameter.
diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.mli b/src/kernel_services/cmdline_parameters/parameter_sig.mli
index cbbd63f5f31545deb803d468a6ed9ed7cdda8ca3..7c5206c5ea64a98de133e91f4bb1f0093105bc36 100644
--- a/src/kernel_services/cmdline_parameters/parameter_sig.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_sig.mli
@@ -143,7 +143,7 @@ module type S_no_parameter = sig
(** Set the option. *)
val add_set_hook: (t -> t -> unit) -> unit
- (** Add a hook to be called whenafter the function {!set} is called.
+ (** Add a hook to be called after the function {!set} is called.
The first parameter of the hook is the old value of the parameter while
the second one is the new value. *)
@@ -303,7 +303,7 @@ module type Specific_dir = sig
val dir: ?error:bool -> unit -> string
(** [dir ~error ()] returns the specific directory name, if
- any. Otherwise, Frama-C halts on an user error if [error] orelse the
+ any. Otherwise, Frama-C halts on an user error if [error] or if the
behavior depends on [force_dir]. Default of [error] is [true].
@raise No_dir if there is no share directory for this plug-in and [not
error] and [not force_dir]. *)
@@ -311,7 +311,7 @@ module type Specific_dir = sig
val file: ?error:bool -> string -> string
(** [file basename] returns the complete filename of a file stored in [dir
()]. If there is no such directory, Frama-C halts on an user error if
- [error] orelse the behavior depends on [force_dir]. Default of [error] is
+ [error] or if the behavior depends on [force_dir]. Default of [error] is
[true].
@raise No_dir if there is no share directory for this plug-in and [not
error] and [not force_dir]. *)
diff --git a/src/kernel_services/cmdline_parameters/typed_parameter.mli b/src/kernel_services/cmdline_parameters/typed_parameter.mli
index 35976b7772092c6e3c4b96036d3bdff2a090b362..48ba08f2b205a0a376f67589d31650172eb2a771 100644
--- a/src/kernel_services/cmdline_parameters/typed_parameter.mli
+++ b/src/kernel_services/cmdline_parameters/typed_parameter.mli
@@ -21,7 +21,7 @@
(**************************************************************************)
(** Parameter settable through a command line option.
- This is a low level API, internaly used by the kernel. As a plug-in
+ This is a low level API, internally used by the kernel. As a plug-in
developer, you certainly prefer to use the API of {!Plugin} instead.
@since Nitrogen-20111001 *)
diff --git a/src/kernel_services/parsetree/cabs.ml b/src/kernel_services/parsetree/cabs.ml
index d17eb2af3eb7a665c92c7a8d0e013c3b13469495..f0b7b94f54b7175e0d449fcea597299ff8c1a9c8 100644
--- a/src/kernel_services/parsetree/cabs.ml
+++ b/src/kernel_services/parsetree/cabs.ml
@@ -229,18 +229,18 @@ and raw_statement =
(* Exception mechanism *)
| THROW of expression option * cabsloc
(** throws the corresponding expression. [None] corresponds to
- re-throwing the exception currently being catched (thus is only
+ re-throwing the exception currently being caught (thus is only
meaningful in a catch clause). This node is not generated by the
C parser, but can be used by external front-ends.
*)
| TRY_CATCH of statement * (single_name option * statement) list * cabsloc
(** [TRY_CATCH(s,clauses,loc)] catches exceptions thrown by execution of
[s], according to [clauses]. An
- exception [e] is catched by the first clause
+ exception [e] is caught by the first clause
[(spec,(name, decl, _, _)),body]
such that the type of [e] is compatible with [(spec,decl)]. [name]
is then associated to a copy of [e], and [body] is executed. If the
- [single_name] is [None], all exceptions are catched by the corresponding
+ [single_name] is [None], all exceptions are caught by the corresponding
clause.
The corresponding [TryCatch] node in {!Cil_types.stmtkind} has a refined
@@ -316,7 +316,7 @@ and cabsexp =
and constant =
| CONST_INT of string (* the textual representation *)
- | CONST_FLOAT of string (* the textual representaton *)
+ | CONST_FLOAT of string (* the textual representation *)
| CONST_CHAR of int64 list
| CONST_WCHAR of int64 list
| CONST_STRING of string
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 2ba894afceabe2faa810a51ae031a6a04f7e2287..e7b0d6f04e8815382367d083f110b2fa26116436 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -403,7 +403,7 @@ module Value : sig
valid memory zones that correspond to the location that [lv] evaluates
to in [state]. If [for_writing] is true, [zone_lv] is restricted to
memory zones that are writable. [exact] indicates that [lv] evaluates
- to a valid locatio of cardinal at most one. *)
+ to a valid location of cardinal at most one. *)
val lval_to_precise_loc_with_deps_state:
(state -> deps:Locations.Zone.t option -> lval ->
@@ -847,7 +847,7 @@ module PostdominatorsTypes: sig
end
end
-(** Syntaxic postdominators plugin.
+(** Syntactic postdominators plugin.
@see <../postdominators/index.html> internal documentation. *)
module Postdominators: PostdominatorsTypes.Sig
@@ -897,7 +897,7 @@ module Constant_Propagation: sig
empty; and casts can be introduced when [cast_intro] is true. *)
val compute: (unit -> unit) ref
- (** Propage constant into the functions given by the parameters (in the
+ (** Propagate constant into the functions given by the parameters (in the
same way that {!get}. Then pretty print the resulting program.
@since Beryllium-20090901 *)
@@ -986,14 +986,14 @@ module Pdg : sig
val find_ret_output_node : (t -> PdgTypes.Node.t) ref
(** Get the node corresponding return stmt.
- @raise Not_found if the ouptut state in unreachable
+ @raise Not_found if the output state in unreachable
@raise Bottom if given PDG is bottom.
@raise Top if the given pdg is top. *)
val find_output_nodes :
(t -> PdgIndex.Signature.out_key -> t_nodes_and_undef) ref
(** Get the nodes corresponding to a call output key in the called pdg.
- @raise Not_found if the ouptut state in unreachable
+ @raise Not_found if the output state in unreachable
@raise Bottom if given PDG is bottom.
@raise Top if the given pdg is top. *)
@@ -1378,7 +1378,7 @@ module Slicing : sig
val mk_project : (string -> t) ref
(** To use to start a new slicing project.
Several projects from a same current project can be managed.
- @raise Existing_Project if an axisting project has the same name.*)
+ @raise Existing_Project if an existing project has the same name.*)
val from_unique_name : (string -> t) ref
(** Find a slicing project from its name.
@@ -1429,7 +1429,7 @@ module Slicing : sig
* (if not, it can be used for a slice)
* - [num_slice] gives the number of the slice to name.
* The entry point function is only exported once :
- * it is VERY recommanded to give to it its original name,
+ * it is VERY recommended to give to it its original name,
* even if it is sliced.
* *)
@@ -1452,11 +1452,11 @@ module Slicing : sig
end
- (** Acces to slicing results. *)
+ (** Access to slicing results. *)
module Mark : sig
type t = SlicingTypes.sl_mark
- (** Abtract data type for mark value. *)
+ (** Abstract data type for mark value. *)
val dyn_t : t Type.t
(** For dynamic type checking and journalization. *)
@@ -1710,7 +1710,7 @@ module Slicing : sig
(kernel_function -> ?select:t -> Locations.Zone.t -> Mark.t -> t) ref
(** Internally used to select the statements that modify the
* given zone considered as in output.
- * Be careful that it is NOT the same than selectiong the zone at end !
+ * Be careful that it is NOT the same as selecting the zone at the end!
* ( the 'undef' zone is not propagated...)
* *)
@@ -1748,7 +1748,7 @@ module Slicing : sig
module Slice : sig
type t = SlicingTypes.sl_fct_slice
- (** Abtract data type for function slice. *)
+ (** Abstract data type for function slice. *)
val dyn_t : t Type.t
(** For dynamic type checking and journalization. *)
@@ -1813,7 +1813,7 @@ module Slicing : sig
end
(** Requests for slicing jobs.
- Slicing resquests are part of a slicing project.
+ Slicing requests are part of a slicing project.
So, user requests affect slicing project. *)
module Request : sig
@@ -1845,7 +1845,7 @@ module Slicing : sig
val add_selection_internal:
(Project.t -> Select.t -> unit) ref
(** Internally used to add a selection request to the project requests.
- This selection will be applied to every slicies of the function
+ This selection will be applied to every slices of the function
(already existing or created later). *)
val add_call_slice:
@@ -1905,7 +1905,7 @@ module Slicing : sig
recursively then apply pending requests *)
val pretty : (Format.formatter -> Project.t -> unit) ref
- (** For debugging... Pretty print the resquest list. *)
+ (** For debugging... Pretty print the request list. *)
end
diff --git a/src/kernel_services/plugin_entry_points/dynamic.ml b/src/kernel_services/plugin_entry_points/dynamic.ml
index 7573b4e50f7bbaa723ec68825619ce4fa855a1bf..effc8d2cfbd5dc37c1b0139d1b5399c22d750b2f 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.ml
+++ b/src/kernel_services/plugin_entry_points/dynamic.ml
@@ -63,7 +63,7 @@ let dynlib_error name = function
error ~name ~message:"system error" ~details:(Printexc.to_string e)
| Unloadable details ->
error ~name ~message:"incompatible with current set-up" ~details
- (* the three next errors may be raised in case of incompatibilites with
+ (* the three next errors may be raised in case of incompatibilities with
another plug-in *)
| Incompatible_type s ->
error ~name ~message:"code incompatibility" ~details:s
diff --git a/src/kernel_services/plugin_entry_points/emitter.ml b/src/kernel_services/plugin_entry_points/emitter.ml
index 36872c0502631c36753f4f5e8bd79b3ac69303f3..c4e473630a2be13f3aab52de490635dcfa22cba7 100644
--- a/src/kernel_services/plugin_entry_points/emitter.ml
+++ b/src/kernel_services/plugin_entry_points/emitter.ml
@@ -191,7 +191,7 @@ module Usable_emitters_of_emitter =
(Datatype.Pair
(Datatype.Ref(Usable_emitter)) (* current usable emitter with the
current parameter values *)
- (Datatype.Ref(Usable_emitter.Set))) (* existing usables emitters with
+ (Datatype.Ref(Usable_emitter.Set))) (* existing usable emitters with
the old parameter values *)
(struct
let name = "Emitter.Usable_emitters_of_emitter"
@@ -355,7 +355,7 @@ let register_tuning_parameter name p =
the previous session but not in the current one. In this case, there
is nothing to do.
- Additionnally, even if it still exists, it could be not yet restored
+ Additionally, even if it still exists, it could be not yet restored
since the project library does not ensure that it restores the table
of emitters before the states of parameters. In such a case, it is
also possible to do nothing since the right table in the right state
diff --git a/src/kernel_services/plugin_entry_points/journal.mli b/src/kernel_services/plugin_entry_points/journal.mli
index 6d4836bb32c289931e7a4ee27ad3782c6a267fab..dc0391c7b70e680916c299b15f89ced9b2bf184a 100644
--- a/src/kernel_services/plugin_entry_points/journal.mli
+++ b/src/kernel_services/plugin_entry_points/journal.mli
@@ -46,7 +46,7 @@ val register:
Set [is_dyn] to [true] to journalize a dynamic function. *)
val never_write: string -> 'a -> 'a
- (** [never_write name f] returns a closure [g] observationaly equal to [f]
+ (** [never_write name f] returns a closure [g] observationally equal to [f]
except that trying to write a call to [g] in the journal is an error. If
[f] is not a closure, then [never_write name f] raises
[Invalid_argument]. *)
@@ -107,7 +107,7 @@ val restore: unit -> unit
(* ****************************************************************************)
val keep_file: string -> unit
- (** This function has not to be used explictely. Only offers functions
+ (** This function has not to be used explicitly. Only offers functions
retrieving when running a journal file. *)
val get_session_file: (string -> string) ref
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 77900249ee9ce951327cb08273829370c962f985..079cdcea00cb2a0ba0553fe4597f56507ba00957 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -342,7 +342,7 @@ module Unicode = struct
let help = "use utf8 in messages"
end)
(* This function behaves nicely with the Gui, that detects if command-line
- arguments have been set by the user at some point. One possible improvment
+ arguments have been set by the user at some point. One possible improvement
would be to bypass journalization entirely, but this requires an API
change in Plugin *)
let without_unicode f arg =
@@ -1289,7 +1289,7 @@ let _ =
(object
method fold: 'a. (Project.t -> 'a -> 'a) -> 'a -> 'a =
fun f acc -> Project.fold_on_projects (fun acc p -> f p acc) acc
- method mem _p = true (* impossible to build an unregistred project *)
+ method mem _p = true (* impossible to build an unregistered project *)
end)
let _ =
diff --git a/src/kernel_services/plugin_entry_points/log.ml b/src/kernel_services/plugin_entry_points/log.ml
index 08bf94274c2bf23fa821f39fb820a4218d996767..b9f75d1a5be2a426db20cb48ecf776a14d93d517 100644
--- a/src/kernel_services/plugin_entry_points/log.ml
+++ b/src/kernel_services/plugin_entry_points/log.ml
@@ -772,7 +772,7 @@ struct
let internal_register_tag_handlers _c (_ope,_close) = ()
(* BM->LOIC: I need to keep this code around to be able to handle
- marks ands tags correctly.
+ marks and tags correctly.
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.
diff --git a/src/kernel_services/plugin_entry_points/log.mli b/src/kernel_services/plugin_entry_points/log.mli
index da896ca36a2b10a29accc3cc15bdb35defd4a1b9..d93f983026bb019aa08e48d5ac4eabb3a57c6cce 100644
--- a/src/kernel_services/plugin_entry_points/log.mli
+++ b/src/kernel_services/plugin_entry_points/log.mli
@@ -46,7 +46,7 @@ type 'a pretty_printer =
Generic type for the various logging channels which are not aborting
Frama-C.
- When [current] is [false] (default for most of the channels),
- no location is output. When it is [true], the last registred location
+ no location is output. When it is [true], the last registered location
is used as current (see {!Cil_const.CurrentLoc}).
- [source] is the location to be output. If nil, [current] is used to
determine if a location should be output
@@ -192,7 +192,7 @@ module type Messages = sig
val not_yet_implemented : ('a,formatter,unit,'b) format4 -> 'a
(** raises [FeatureRequest] but {i does not} send any message.
- If the exception is not catched, Frama-C displays a feature-request
+ If the exception is not caught, Frama-C displays a feature-request
message to the user.
@since Beryllium-20090901 *)
diff --git a/src/kernel_services/visitors/cabsvisit.mli b/src/kernel_services/visitors/cabsvisit.mli
index 6091cf42ff4d8ced552484c3121eb6118e2d2ed8..4df5f481a41d9e39145b7f84aae16d7cde627b17 100644
--- a/src/kernel_services/visitors/cabsvisit.mli
+++ b/src/kernel_services/visitors/cabsvisit.mli
@@ -85,7 +85,7 @@ val visitCabsTypeSpecifier: cabsVisitor ->
Cabs.typeSpecifier -> Cabs.typeSpecifier
val visitCabsSpecifier: cabsVisitor -> Cabs.specifier -> Cabs.specifier
-(** Visits a decl_type. The bool argument is saying whether we are ina
+(** Visits a decl_type. The bool argument is saying whether we are in a
* function definition and thus the scope in a PROTO should extend until the
* end of the function *)
val visitCabsDeclType: cabsVisitor -> bool -> Cabs.decl_type -> Cabs.decl_type
diff --git a/src/kernel_services/visitors/visitor.ml b/src/kernel_services/visitors/visitor.ml
index e6cd12f3e30c742008763b42b8c46c991a094d6a..f9da857ba9e6fe49993e95b75dab82bac78680a4 100644
--- a/src/kernel_services/visitors/visitor.ml
+++ b/src/kernel_services/visitors/visitor.ml
@@ -659,7 +659,7 @@ object(self)
Anyway, this is only used for SkipChildren and JustCopy/JustCopyPost
(and for a copy visitor)
If user sticks to DoChildren, s/he'll still have the proper
- correspondance between annotations and emitters.
+ correspondence between annotations and emitters.
*)
let get_spec () = match g with
| GFun _ | GFunDecl _ when Ast.is_def_or_last_decl g ->
diff --git a/src/libraries/datatype/datatype.mli b/src/libraries/datatype/datatype.mli
index 5bb81c6b20ae2a1f8ddb3e935091f518b34f1a34..0c9e2da056012d49bb30f9187cb10d561e24ccdd 100644
--- a/src/libraries/datatype/datatype.mli
+++ b/src/libraries/datatype/datatype.mli
@@ -63,7 +63,7 @@ module type S_no_copy = sig
(** Packed version of the descriptor. *)
val reprs: t list
- (** List of representents of the descriptor. *)
+ (** List of representants of the descriptor. *)
val equal: t -> t -> bool
(** Equality: same spec than [Pervasives.(=)]. *)
@@ -175,7 +175,7 @@ end
end] *)
module Undefined: Undefined
-(** Same as {!Undefined}, but the type is supposed to be marshalable by the
+(** Same as {!Undefined}, but the type is supposed to be marshallable by the
standard OCaml way (in particular, no hash-consing or projects inside
the type).
@plugin development guide *)
diff --git a/src/libraries/datatype/descr.mli b/src/libraries/datatype/descr.mli
index b2cd632eceba1edc11df3f35c9810f565b1d1192..c420a202157d33a862db64e5dd0d6fd9b6acddf6 100644
--- a/src/libraries/datatype/descr.mli
+++ b/src/libraries/datatype/descr.mli
@@ -24,7 +24,7 @@
This module provides a safe API on top of modules {!Unmarshal} of
{!Structural_descr}, using module {!Type}. This module offers the same
- powerfulness than {!Unmarshal}, but in a safe way. *)
+ power as {!Unmarshal}, but in a safe way. *)
(* ********************************************************************** *)
(** {2 Type declaration} *)
@@ -47,7 +47,7 @@ val t_int64 : int64 t
val t_nativeint : nativeint t
val unmarshable: 'a t
-(** Descriptor for unmarshalable types.
+(** Descriptor for unmarshallable types.
@since Carbon-20101201 *)
val is_unmarshable: 'a t -> bool
diff --git a/src/libraries/datatype/type.ml b/src/libraries/datatype/type.ml
index 054ddf898763602ab03461e1427eda7f033e9348..7215f383564b9dbc000a701d6f225f799fc5b983 100644
--- a/src/libraries/datatype/type.ml
+++ b/src/libraries/datatype/type.ml
@@ -700,7 +700,7 @@ end = struct
else if tag = Obj.closure_tag then
(* Buggy code with OCaml 4.01, deactivated for now
(* assumes that the first word of a closure does not change in
- any way (even by Gc.compact invokation). *)
+ any way (even by Gc.compact invocation). *)
Obj.magic (Obj.field x 0)*)
(* to be tested (suggested by Damien D.): add a 'xor 0' *)
(* Obj.magic (Obj.field x 0)*)
diff --git a/src/libraries/datatype/type.mli b/src/libraries/datatype/type.mli
index 2433dd2364ad33b3fdcdb872600795fbb3340774..42a2a17bbc76bef042278e6f39e75d9a84b9f0df 100644
--- a/src/libraries/datatype/type.mli
+++ b/src/libraries/datatype/type.mli
@@ -232,8 +232,8 @@ module Function : sig
val instantiate:
?label:(string * (unit -> 'a) option) -> 'a t -> 'b t -> ('a -> 'b) t * bool
(** Possibility to add a label for the parameter.
- - [~label:(p,None)] for a mandatory labelized parameter [p];
- - [~label:(p,Some f)] for an optional labelized parameter [p],
+ - [~label:(p,None)] for a mandatory labeled parameter [p];
+ - [~label:(p,Some f)] for an optional labeled parameter [p],
with default value [f ()]. *)
val is_instance_of: 'a t -> bool
val get_instance: ('a -> 'b) t -> 'a t * 'b t * string option
diff --git a/src/libraries/project/state.mli b/src/libraries/project/state.mli
index ea98a6161dbd0b6b30d2eeee2b920e584e8e61c3..b67cf7eb11527e74ee691d924e0f1ec560e957da 100644
--- a/src/libraries/project/state.mli
+++ b/src/libraries/project/state.mli
@@ -48,7 +48,7 @@ module type Local = sig
val clear: t -> unit
(** How to clear a state. After clearing, the state should be
- observationaly the same that after its creation (see invariant 2
+ observationally the same that after its creation (see invariant 2
below). *)
val get: unit -> t
diff --git a/src/libraries/project/state_builder.mli b/src/libraries/project/state_builder.mli
index cd5ec62c5a89c56256c508f48b3b48b4a76b1041..7ae3c2ec42e76efffd0bd1b4ad86311d51c57ae1 100644
--- a/src/libraries/project/state_builder.mli
+++ b/src/libraries/project/state_builder.mli
@@ -284,7 +284,7 @@ module Hashconsing_tbl_weak: Hashconsing_tbl
(** Hash table for hashconsing, but the internal table is _not_ weak
(it is a regular hash table). This module should be used only in case
- perfect reproductibility matters, as the table will never be emptied by
+ perfect reproducibility matters, as the table will never be emptied by
the GC.
@since Aluminium-20160501 *)
module Hashconsing_tbl_not_weak: Hashconsing_tbl
diff --git a/src/libraries/stdlib/extlib.ml b/src/libraries/stdlib/extlib.ml
index 1d76856cac00215439cd795d425f8b9a62401975..7e176edf36b16855326822d916d7737570cdaacf 100644
--- a/src/libraries/stdlib/extlib.ml
+++ b/src/libraries/stdlib/extlib.ml
@@ -343,7 +343,7 @@ let try_finally ~finally f x =
(*[LC] due to Unix.exec calls, at_exit might be cloned into child process
and executed when they are canceled early.
- The alternative, such as registering an dameon that raises an exception,
+ The alternative, such as registering an daemon that raises an exception,
hence interrupting the process, might not work: child processes still need to
run some daemons, such as [Pervasives.flush_all] which is registered by default. *)
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index 53e533497e003d1368f2e40334d6a709728714e6..6ed2a0a8fae6f2c4cc5742d92af5ed06d6e5bbd4 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -58,7 +58,7 @@ val mk_labeled_fun: string -> 'a
@raise Unregistered_function when not properly initialized *)
val mk_fun: string -> ('a -> 'b) ref
- (** Build a reference to an unitialized function
+ (** Build a reference to an uninitialized function
@raise Unregistered_function when not properly initialized *)
(* ************************************************************************* *)
diff --git a/src/libraries/utils/c_bindings.c b/src/libraries/utils/c_bindings.c
index 2760c0b57bddab606e6daa0373f2612229ed992a..4dbaa607890f0fac5539e9771ec84ace97bfd9de 100644
--- a/src/libraries/utils/c_bindings.c
+++ b/src/libraries/utils/c_bindings.c
@@ -234,7 +234,7 @@ value float_is_negative(value v)
return (Val_int((int)((uv.i) >> 63)));
}
-/* Some compilers apply the C90 standard stricly and do not
+/* Some compilers apply the C90 standard strictly and do not
prototype strtof() although it is available in the C library. */
float strtof(const char *, char **);
diff --git a/src/libraries/utils/command.mli b/src/libraries/utils/command.mli
index f3b5e1dba4c0d273b9d7289c30098e0f8bddc09c..30f9dcb9176adeb0e077832cef915834e563e28c 100644
--- a/src/libraries/utils/command.mli
+++ b/src/libraries/utils/command.mli
@@ -41,7 +41,7 @@ val bincopy : bytes -> in_channel -> out_channel -> unit
(** [copy buffer cin cout] reads [cin] until end-of-file
and copy it in [cout].
[buffer] is a temporary string used during the copy.
- Recommanded size is [2048].
+ Recommended size is [2048].
@modify Silicon-20161101 [buffer] has now type [bytes] instead of [string]
*)
@@ -66,7 +66,7 @@ type 'a result = Result of 'a | Error of exn
val catch : ('a -> 'b) -> 'a -> 'b result
val return : 'a result -> 'a
val time : ?rmax:timer -> ?radd:timer -> ('a -> 'b) -> 'a -> 'b
- (** Compute the ellapsed time with [Sys.time].
+ (** Compute the elapsed time with [Sys.time].
The [rmax] timer is maximized and the [radd] timer is cumulated.
Computed result is returned, or exception is re-raised. *)
diff --git a/src/libraries/utils/hptmap_sig.mli b/src/libraries/utils/hptmap_sig.mli
index 33b238f21332a3c178c4e970763f01c15ac016f5..fa1ac37bce5ae2afdf78c644b66dd91a8ac7b618 100644
--- a/src/libraries/utils/hptmap_sig.mli
+++ b/src/libraries/utils/hptmap_sig.mli
@@ -221,7 +221,7 @@ module type S = sig
decide_both:(key -> v -> v -> bool) ->
t -> t -> bool
(** Same functionality as [generic_predicate] but with a different signature.
- All decisin functions return a boolean that are combined differently
+ All decision functions return a boolean that are combined differently
depending on whether the predicate is existential or universal. *)
val generic_symmetric_predicate :
diff --git a/src/libraries/utils/hptset.ml b/src/libraries/utils/hptset.ml
index d96321d7fbd94e4760378ba4b74fe9aa310e0cb7..dd5eabebd286a729014a6f92ea060e89bac4677a 100644
--- a/src/libraries/utils/hptset.ml
+++ b/src/libraries/utils/hptset.ml
@@ -188,7 +188,7 @@ module Make(X: Hptmap.Id_Datatype)
let from_shape m = from_shape (fun _ _ -> ()) m
- (* Partial application is needed becauses of caches *)
+ (* Partial application is needed because of caches *)
let fold2_join_heterogeneous ~cache ~empty_left ~empty_right ~both ~join ~empty =
let both k () v = both k v in
fold2_join_heterogeneous ~cache ~empty_left ~empty_right ~both ~join ~empty
diff --git a/src/libraries/utils/pretty_utils.mli b/src/libraries/utils/pretty_utils.mli
index 24332ed0f24bb4ffa9c3b327398dbe0dbb383b64..4829f39539df7b039e52cf421c4fc62f287d3d50 100644
--- a/src/libraries/utils/pretty_utils.mli
+++ b/src/libraries/utils/pretty_utils.mli
@@ -156,7 +156,7 @@ val pp_items :
is called twice: one for computing the maximal size of {i titles},
obtained {i via} function [~title] for each item. The second pass
pretty-print each item using [~pp_item pp] where the passed [pp] printer
- can be used to pretty-print titles with alignement.
+ can be used to pretty-print titles with alignment.
A typical usage for printing [values], a list of [(string*int)] items:
{[
@@ -196,7 +196,7 @@ val marger : unit -> marger (** Create an empty marger *)
val add_margin : marger -> ?margin:int -> ?min:int -> ?max:int -> string -> unit
(** Updates the marger with new text dimension.
The marger width is updated with the width of the provided text.
- The optional parameters are used to ajust the text width as follows:
+ The optional parameters are used to adjust the text width as follows:
- [?margin] is added to text size (default [0])
- [?min] minimum size ([~margin] included, default [0])
- [?max] maximum size ([~margin] included, default [80]) *)
diff --git a/src/libraries/utils/rgmap.mli b/src/libraries/utils/rgmap.mli
index e7a2c251a336e0f4f3b4f32b4abc385fddcf79fd..35a75229078ef2aa03c1301c8a005dceee3c9268 100644
--- a/src/libraries/utils/rgmap.mli
+++ b/src/libraries/utils/rgmap.mli
@@ -27,7 +27,7 @@
structure is well suited to attach tags to AST-nodes in GUI, where
each node is associated to buffer offset ranges.
- When seveal entries cover a range, precedence goes to the tightest ones.
+ When several entries cover a range, precedence goes to the tightest ones.
When overlapping entries with the same width applies, the result of lookup is
not specified. Remark that for AST-based ranges, overlapping ranges
are always included one in the order.
@@ -41,7 +41,7 @@ type 'a t
(** The type of range maps, containing of collection of ['a entry]. *)
type 'a entry = int * int * 'a
-(** Entry [(a,b,v)] maps range [a..b] (both inclued) to value [v] in the map. *)
+(** Entry [(a,b,v)] maps range [a..b] (both included) to value [v] in the map. *)
val empty : 'a t
(** The empty map. *)
@@ -53,7 +53,7 @@ val add : ?overlap:bool -> 'a entry -> 'a t -> 'a t
maps. *)
val find : int -> int -> 'a t -> 'a entry
-(** Find the tighest entry containing the specified range.
+(** Find the tightest entry containing the specified range.
@raise Not_found if no entry applies *)
val find_all : int -> int -> 'a t -> 'a entry list
diff --git a/src/libraries/utils/task.mli b/src/libraries/utils/task.mli
index d00f39c2b5525e372d371981e738201ea3c56153..eec28be5ca5f107a13609a7e428d98290063a71c 100644
--- a/src/libraries/utils/task.mli
+++ b/src/libraries/utils/task.mli
@@ -100,7 +100,7 @@ val (>>?) : 'a task -> ('a status -> unit) -> 'a task (** [finally] infix. *)
val (>>!) : 'a task -> ('a status -> unit) -> unit task (** [callback] infix. *)
(* ************************************************************************* *)
-(** {2 Synchroneous Command} *)
+(** {2 Synchronous Command} *)
(* ************************************************************************* *)
type mutex
@@ -147,7 +147,7 @@ val shared : descr:string -> retry:bool -> (unit -> 'a task) -> 'a shared
instance is required but no shared instance task is actually running.
Interrupted tasks (by Cancel or Timeout) are retried for further
instances. If the task failed, it can be re-launch if [retry] is [true].
- Otherwize, further instances will return [Failed] status. *)
+ Otherwise, further instances will return [Failed] status. *)
val share : 'a shared -> 'a task
(** New instance of shared task. *)
diff --git a/src/libraries/utils/wto.mli b/src/libraries/utils/wto.mli
index ca87e711ce9b991df31ccbedc498fe6f0ea95ed6..a6313d69150512018d00d19660bf494637ded349 100644
--- a/src/libraries/utils/wto.mli
+++ b/src/libraries/utils/wto.mli
@@ -20,10 +20,10 @@
(* *)
(**************************************************************************)
-(** Weak topological orderings (WTOs) are a hierarchical decompositions of the
+(** Weak topological orderings (WTOs) are a hierarchical decomposition of the
a graph where each layer is topologically ordered and strongly connected
- components are agregated and oredered recursively. This is a very
- convenient reprentation to describe an evaluation order to reach a
+ components are aggregated and ordered recursively. This is a very
+ convenient representation to describe an evaluation order to reach a
fixpoint. *)
@@ -36,7 +36,7 @@ type 'n component =
(** A strongly connected component, described by its head node and the
remaining sub-components topologically ordered *)
| Node of 'n
- (** A signe node without self loop *)
+ (** A single node without self loop *)
(** A list of strongly connected components, sorted topologically *)
and 'n partition = 'n component list
diff --git a/src/plugins/aorai/aorai_register.ml b/src/plugins/aorai/aorai_register.ml
index f27271f18abba3d959ccbb6a70ae3e9c8335bf77..b8c9e0905203b6680a5e47e872dcae24a8f1149e 100644
--- a/src/plugins/aorai/aorai_register.ml
+++ b/src/plugins/aorai/aorai_register.ml
@@ -39,7 +39,7 @@ let ltl2ba_params = " -l -p -o "
let ltl_to_promela = Hashtbl.create 7
-let set_ltl_correspondance h =
+let set_ltl_correspondence h =
Hashtbl.clear ltl_to_promela;
Hashtbl.iter (fun x y -> Hashtbl.add ltl_to_promela x y) h
@@ -85,7 +85,7 @@ let ltl_to_ltlLight f_ltl f_out =
let (ltl_form,exprs) = Ltllexer.parse c in
close_in c;
Ltl_output.output ltl_form f_out;
- set_ltl_correspondance exprs
+ set_ltl_correspondence exprs
with
| Not_found -> Aorai_option.abort "Unknown LTL file %s" f_ltl
| Ltllexer.Error (loc,msg) -> syntax_error loc msg
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 359d12f4f69d77e7e3ffe4a9d67a19e9b4f7de23..dfc4fa866b03d9cb49dc568a420f0e9c8964c7c6 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -47,7 +47,7 @@ let rename_pred v1 v2 p =
Visitor.visitFramacPredicate r p
(** Given a transition a function name and a function status (call or
- return) it returns if the cross condition can be statisfied with
+ return) it returns if the cross condition can be satisfied with
only function status.
*)
let isCrossable tr func st =
@@ -109,7 +109,7 @@ let find_enum, set_enum =
(* ************************************************************************* *)
(** Given a transition a function name and a function status (call or return)
- it returns if the cross condition can be statisfied with only
+ it returns if the cross condition can be satisfied with only
function status. *)
let isCrossableAtInit tr func =
(* When in doubt, return true anyway. More clever plug-ins will take care
@@ -735,7 +735,7 @@ let is_out_of_state_pred state =
Logic_const.tvar (Data_for_aorai.get_state_logic_var state))
(* In the deterministic case, we only assign the unique state variable
- to a specific enumerated constant. Non-determistic automata on the other
+ to a specific enumerated constant. Non-deterministic automata on the other
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 ()
@@ -1287,7 +1287,7 @@ let partition_action trans =
List.fold_left treat_one_trans Cil_datatype.Term_lval.Map.empty trans
(* TODO: this must be refined to take pebbles into account: in that
- case, disjointness condition is on pebble set for each state. *)
+ case, disjointedness condition is on pebble set for each state. *)
let disjoint_states loc _ states precond =
let states = Data_for_aorai.Aorai_state.Set.elements states in
let rec product acc l =
diff --git a/src/plugins/aorai/aorai_utils.mli b/src/plugins/aorai/aorai_utils.mli
index 713e4e233530cbd37290bb8332bfb1df8cdd21ae..5ccf05a9a783a86a38c0e4355a48da985e2fcd5e 100644
--- a/src/plugins/aorai/aorai_utils.mli
+++ b/src/plugins/aorai/aorai_utils.mli
@@ -27,7 +27,7 @@ open Cil_types
open Promelaast
(** Given a transition a function and a function status (call or return)
- it returns if the cross condition can be statisfied
+ it returns if the cross condition can be satisfied
with only function status.
*)
@@ -35,7 +35,7 @@ val isCrossable:
(typed_condition * action) trans -> kernel_function -> funcStatus -> bool
(** Given a transition and the main entry point it returns if
- the cross condition can be statisfied at the beginning of the program. *)
+ the cross condition can be satisfied at the beginning of the program. *)
val isCrossableAtInit:
(typed_condition * action) trans -> kernel_function -> bool
diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index e9350cde1ebb90d00f3c00f144c03a6585ca75f4..0f5b485abb57a87c2e05aa951801c3709945cece 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -451,7 +451,7 @@ let get_unchanged_aux_var loc current_state =
Data_for_aorai.Aorai_state.Map.fold treat_one_pre_state current_state []
(**
- This visitor adds a specification to each fonction and to each loop,
+ This visitor adds a specification to each function and to each loop,
according to specifications stored into Data_for_aorai.
*)
class visit_adding_pre_post_from_buch treatloops =
diff --git a/src/plugins/aorai/data_for_aorai.mli b/src/plugins/aorai/data_for_aorai.mli
index ffca4f6477d1d0b106ddea3874a1b1cf5fc60ff9..7179248f97e6d8320e9d59e95dc9404bc66e5b0c 100644
--- a/src/plugins/aorai/data_for_aorai.mli
+++ b/src/plugins/aorai/data_for_aorai.mli
@@ -124,10 +124,10 @@ val loopInit : string
(** C variables *)
-(** Name of curOp C generated variable (Name of the curent operation) *)
+(** Name of curOp C generated variable (Name of the current operation) *)
val curOp : string
-(** Name of curOpStatus C generated variable (Status Return or Call of the curent operation) *)
+(** Name of curOpStatus C generated variable (Status Return or Call of the current operation) *)
val curOpStatus : string
(** Name of curState C generated variable (Table of states that can be synchronized with the program) *)
diff --git a/src/plugins/aorai/promelalexer.mll b/src/plugins/aorai/promelalexer.mll
index a28414e90badfefdf5060451b2ab78f1e8cf1bbe..68b97db0d6392b48413729df326aa4bb60a55290 100644
--- a/src/plugins/aorai/promelalexer.mll
+++ b/src/plugins/aorai/promelalexer.mll
@@ -87,9 +87,9 @@ rule token = parse
PROMELA_CALLORRETURNOF s }
- | "callof_" { raise_located (loc lexbuf) "Illegal fonction name in Promela file." }
- | "returnof_" { raise_located (loc lexbuf) "Illegal fonction name in Promela file." }
- | "callorreturnof_" { raise_located (loc lexbuf) "Illegal fonction name in Promela file." }
+ | "callof_" { raise_located (loc lexbuf) "Illegal function name in Promela file." }
+ | "returnof_" { raise_located (loc lexbuf) "Illegal function name in Promela file." }
+ | "callorreturnof_" { raise_located (loc lexbuf) "Illegal function name in Promela file." }
diff --git a/src/plugins/aorai/promelalexer_withexps.mll b/src/plugins/aorai/promelalexer_withexps.mll
index 7909d7e05a6008d952c29a0e8a398a588b3bce8b..ce3a7c9e9311ef6926e10acd714edec86fdc520d 100644
--- a/src/plugins/aorai/promelalexer_withexps.mll
+++ b/src/plugins/aorai/promelalexer_withexps.mll
@@ -92,9 +92,9 @@ rule token = parse
PROMELA_CALLORRETURNOF s }
- | "callof_" { raise_located (loc lexbuf) "Illegal fonction name in Promela file." }
- | "returnof_" { raise_located (loc lexbuf) "Illegal fonction name in Promela file." }
- | "callorreturnof_" { raise_located (loc lexbuf) "Illegal fonction name in Promela file." }
+ | "callof_" { raise_located (loc lexbuf) "Illegal function name in Promela file." }
+ | "returnof_" { raise_located (loc lexbuf) "Illegal function name in Promela file." }
+ | "callorreturnof_" { raise_located (loc lexbuf) "Illegal function name in Promela file." }
| rD+ | '-' rD+ { PROMELA_INT (lexeme lexbuf) }
diff --git a/src/plugins/callgraph/cg.ml b/src/plugins/callgraph/cg.ml
index 2a2b94156d476ddef85e59675370151ca704bebb..1a7605b05d9ff278d90015d31503699cc6e093af 100644
--- a/src/plugins/callgraph/cg.ml
+++ b/src/plugins/callgraph/cg.ml
@@ -24,7 +24,7 @@ open Cil_types
(* Kernel functions with a custom function [compare] independent of vids. So the
callgraph and its iterations are independent from the vids generator and is
- only dependent of the analyzed program itsef. *)
+ only dependent of the analyzed program itself. *)
module Kf_sorted = struct
type t = Kernel_function.t
let equal = Kernel_function.equal
@@ -154,7 +154,7 @@ let syntactic_compute g =
pointed;
Cil.SkipChildren
| _ ->
- (* skip childrens for efficiency *)
+ (* skip children for efficiency *)
Cil.SkipChildren
(* for efficiency purpose, skip many items *)
@@ -165,7 +165,7 @@ let syntactic_compute g =
method !vbehavior _ = Cil.SkipChildren
end in
Visitor.visitFramacFileSameGlobals o (Ast.get ());
- (* now remove the potential unrelevant nodes wrt selected options *)
+ (* now remove the potential irrelevant nodes wrt selected options *)
if not (Options.Uncalled.get () && Options.Uncalled_leaf.get ()) then
G.iter_vertex
(fun kf ->
diff --git a/src/plugins/callgraph/cg_viewer.ml b/src/plugins/callgraph/cg_viewer.ml
index a5cfda94e0ad2599100a47d49228c5ecd4e015ed..d58bbd570d12721b7e794d9c74bffcf72fac8feb 100644
--- a/src/plugins/callgraph/cg_viewer.ml
+++ b/src/plugins/callgraph/cg_viewer.ml
@@ -50,7 +50,7 @@ class ['v, 'e, 'c] services_view view = object (self)
let deployed, nodes = Hashtbl.find services service in
assert (not !deployed);
deployed := true;
- (* itering on nodes of the current service *)
+ (* iterating on nodes of the current service *)
List.iter
(fun n ->
n#compute ();
@@ -71,7 +71,7 @@ class ['v, 'e, 'c] services_view view = object (self)
let deployed, nodes = Hashtbl.find services service in
assert !deployed;
deployed := false;
- (* itering on nodes of the current service *)
+ (* iterating on nodes of the current service *)
List.iter
(fun n ->
if not (self#is_root n) then n#hide ();
diff --git a/src/plugins/constant_propagation/register.ml b/src/plugins/constant_propagation/register.ml
index ea4abeade421007515cb023f09104e5e19d7fd3d..d1055928d2ae555fae365cb2f26e4438294498c7 100644
--- a/src/plugins/constant_propagation/register.ml
+++ b/src/plugins/constant_propagation/register.ml
@@ -81,7 +81,7 @@ class propagate project fnames ~cast_intro = object(self)
(* introduce a new cast from [oldt] to [newt] or do not expand [e] *)
method private add_cast ~ignore_const_cast ~oldt ~newt e =
- (* strip the superfleous 'const' attribute (see bts #1787) on
+ (* strip the superfluous 'const' attribute (see bts #1787) on
pointed values. *)
let oldt, newt =
if ignore_const_cast then
diff --git a/src/plugins/from/callwise.ml b/src/plugins/from/callwise.ml
index 17550dc355d003043236b979cabb268220121f6f..5c59508b7b59ea7ebd32a62eda61182f22a0628a 100644
--- a/src/plugins/from/callwise.ml
+++ b/src/plugins/from/callwise.ml
@@ -54,7 +54,7 @@ type from_state = {
(** The state of the callwise From analysis. Only the top of this callstack
is accessed. New calls are pushed on the stack when Value starts the
- analysis of a function, and popped when the analysis finisheds. This
+ analysis of a function, and popped when the analysis finishes. This
stack is manually synchronized with Value's callstack. *)
let call_froms_stack : from_state list ref = ref []
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index 2f5430b62e34520143d02453b419d88537518439..0cb7fe51fdbc0c68b751706c83f0f9162754c8c4 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -334,7 +334,7 @@ struct
let join old new_ = fst (join_and_is_included old new_)
let is_included old new_ = snd (join_and_is_included old new_)
- (** Handle an assignement [lv = ...], the dependencies of the right-hand
+ (** Handle an assignment [lv = ...], the dependencies of the right-hand
side being stored in [deps_right]. *)
let transfer_assign stmt lv deps_right state =
(* The assigned location is [loc], whose address is computed from
@@ -413,7 +413,7 @@ struct
substitute !state_with_formals additional_deps
in
(* From state just after the call,
- but before the result assigment *)
+ but before the result assignment *)
let deps_after_call =
let before_call = state.deps_table in
let open Function_Froms in
@@ -422,7 +422,7 @@ struct
Memory.compose call_substituted before_call
in
let state = {state with deps_table = deps_after_call } in
- (* Treatement for the possible assignement
+ (* Treatment for the possible assignment
of the call result *)
match lvaloption with
| None -> state
diff --git a/src/plugins/from/from_compute.mli b/src/plugins/from/from_compute.mli
index e5c1785469b1a664262d18234946088fe253db2e..8daa78f2989bf831b95c1e0dea2077f075723444 100644
--- a/src/plugins/from/from_compute.mli
+++ b/src/plugins/from/from_compute.mli
@@ -41,7 +41,7 @@ sig
in [false].) *)
(** Clean the given from (that have been computed for the given function),
- optionally save them, and return the cleant result. *)
+ optionally save them, and return the cleaned result. *)
val cleanup_and_save : kernel_function -> Function_Froms.t -> Function_Froms.t
end
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index 5772ea04141acac8c11b16764cea746a849cc7b8..868a66fd4db267685a039a592bfab22202490fdb 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -1459,7 +1459,7 @@ class main_window () : main_window_extension_points =
in
display_warnings ();
- (* Gestion of navigation history *)
+ (* Management of navigation history *)
ignore (History.create_buttons (self#menu_manager ()));
History.set_display_elt_callback
(function
@@ -1505,7 +1505,7 @@ class main_window () : main_window_extension_points =
try
(* Retrieve a potential varinfo from the selection *)
let vi = Gui_printers.varinfo_of_link s in
- (* Now that we have a varinfo, we re-synthetize a kinstr from
+ (* Now that we have a varinfo, we re-synthesize a kinstr from
the current localizable, as it must be supplied to the callbacks *)
match History.selected_localizable () with
| None -> ()
diff --git a/src/plugins/gui/design.mli b/src/plugins/gui/design.mli
index 42036e30c6a276a0ca9fbf59e7cb85144a9d0edb..706249837d75ca4255d03f8b2b35da6d7ef3d7ed 100644
--- a/src/plugins/gui/design.mli
+++ b/src/plugins/gui/design.mli
@@ -188,7 +188,7 @@ class type main_window_extension_points = object
(** Reset the GUI and its extensions to its initial state *)
method rehighlight : unit -> unit
- (** Force to rehilight the current displayed buffer.
+ (** Force to rehighlight the current displayed buffer.
Plugins should call this method whenever they have changed the states
on which the function given to [register_source_highlighter] have been
updated. *)
diff --git a/src/plugins/gui/file_manager.ml b/src/plugins/gui/file_manager.ml
index 95082fa5a7436cc47b9f48755237684154442959..d4d0173ced66b32f96da54ab9f3dd2738882e62b 100644
--- a/src/plugins/gui/file_manager.ml
+++ b/src/plugins/gui/file_manager.ml
@@ -62,7 +62,7 @@ let reparse (host_window: Design.main_window_extension_points) =
Extlib.may History.push new_helt;
host_window#reset ();
(** The buffer is not ready yet, modification of its vadjustement
- is unrealiable *)
+ is unreliable *)
let set () =
let adj = host_window#source_viewer_scroll#vadjustment in
adj#set_value (old_scroll *. (adj#upper-.adj#lower) +. adj#lower)
diff --git a/src/plugins/gui/filetree.ml b/src/plugins/gui/filetree.ml
index 3b36f8105c6482cf09d01433261685befcdeb7b0..f32f90eb9c58681470d07eddf286a1a9cc788d1d 100644
--- a/src/plugins/gui/filetree.ml
+++ b/src/plugins/gui/filetree.ml
@@ -25,7 +25,7 @@ open Cil_datatype
open Extlib
open Gtk_helper
-(* To debug performance related to heigth of lines *)
+(* To debug performance related to height of lines *)
let fixed_height = false
type filetree_node =
diff --git a/src/plugins/gui/filetree.mli b/src/plugins/gui/filetree.mli
index c066a1cdd9bf555da877930bb97cc810f11515b2..21f534cef98ff7fdb6ac8457a412968bef0772ca 100644
--- a/src/plugins/gui/filetree.mli
+++ b/src/plugins/gui/filetree.mli
@@ -97,7 +97,7 @@ class type t = object
(** [append_pixbuf_column title f visible] appends a new column with name
[title] to the file tree and registers [f] as a callback computing the
list of properties for this column. Do not forget that properties need
- to be set and unset explictely. The argument [visible] is used by the
+ to be set and unset explicitly. The argument [visible] is used by the
column to decide whether it should appear. The returned function
can be used to force an update on the display of the column
[`Visibility] means that the column must be show or hidden. [`Contents]
diff --git a/src/plugins/gui/gtk_helper.mli b/src/plugins/gui/gtk_helper.mli
index 13242edf0dbf7c6ae3af67fe36b2203a834deead..21ba828186bf10870357ce1a2c05ef95c83e1915 100644
--- a/src/plugins/gui/gtk_helper.mli
+++ b/src/plugins/gui/gtk_helper.mli
@@ -37,7 +37,7 @@ module Icon: sig
| Feedback of Property_status.Feedback.t
(** Generic icons available in every proper install of Frama-C.
To be able to use [Custom s] you must have called
- [register ~name:s ~file] orelse you will get an generic icon
+ [register ~name:s ~file], otherwise you will get a generic icon
placeholder. *)
val register: name:string -> file:string -> unit
diff --git a/src/plugins/gui/history.ml b/src/plugins/gui/history.ml
index 8f33c4cc86c9fac2f09466cd018842ba860877d3..badc51ebb0593ce6cf098f56904036e544d28024 100644
--- a/src/plugins/gui/history.ml
+++ b/src/plugins/gui/history.ml
@@ -93,7 +93,7 @@ module CurrentHistory =
let default _ = default_history
end)
-(* This is correct because the implementation makes sur that [.current = None]
+(* This is correct because the implementation makes sure that [.current = None]
implies [.forward = [] && .back = []] *)
let is_empty () = (CurrentHistory.get ()).current = None
let can_go_back () = (CurrentHistory.get ()).back <> []
diff --git a/src/plugins/gui/menu_manager.mli b/src/plugins/gui/menu_manager.mli
index bf0b1b6930bdb07867c6d0d67c50f2ebb4362496..54f6d65801ac1a26e4272c078adfc2a1084e423b 100644
--- a/src/plugins/gui/menu_manager.mli
+++ b/src/plugins/gui/menu_manager.mli
@@ -36,7 +36,7 @@ type where =
with checkboxes in menus, or as toggle buttons in toolbars. They receive the
after-click state as argument. The state of the button with the second
argument of [Bool_callback]. Currently checks menus cannot have images in
- Gtk, sor the [GtkStock.id] fields of [where] are ignored.
+ Gtk, or the [GtkStock.id] fields of [where] are ignored.
@since Nitrogen-20111001 *)
type callback_state =
diff --git a/src/plugins/gui/warning_manager.mli b/src/plugins/gui/warning_manager.mli
index 65c5d3088b74b749187db06a7950159cc880c29d..83d623f9051ba6deb2f5353a6f70e117bb480eb1 100644
--- a/src/plugins/gui/warning_manager.mli
+++ b/src/plugins/gui/warning_manager.mli
@@ -34,7 +34,7 @@ val append: t -> Log.event -> unit
(** Append a new message warning. *)
val clear: t -> unit
-(** Clear all the stored warnigns. *)
+(** Clear all the stored warnings. *)
(*
Local Variables:
diff --git a/src/plugins/gui/wbox.mli b/src/plugins/gui/wbox.mli
index 357aada3dc636d4f8897b4011071141535156260..7529975f046507d2eb0368145a1ad73a305ae37e 100644
--- a/src/plugins/gui/wbox.mli
+++ b/src/plugins/gui/wbox.mli
@@ -31,7 +31,7 @@ type expand =
| W (** Stay at widget's size. *)
| H (** Expands horizontally. Typically, a text-field. *)
| V (** Expands vertically. Typically a side-bar. *)
- | HV (** Expanfs in both directions. Typically, a text editor. *)
+ | HV (** Expands in both directions. Typically, a text editor. *)
(** Generic packing. Without [~widget], a space is created instead.
@@ -63,10 +63,10 @@ val label : ?fill:bool -> ?style:style -> ?align:align -> ?padding:int -> string
val hbox : box list -> widget (** Pack a list of boxes horizontally. *)
val vbox : box list -> widget (** Pack a list of boxes vertically. *)
-(** Pack a list of widgets horizontally, with all widgets sticked to the same width *)
+(** Pack a list of widgets horizontally, with all widgets stuck to the same width *)
val hgroup : widget list -> widget
-(** Pack a list of widgets vertically, with all widgets sticked to the same width *)
+(** Pack a list of widgets vertically, with all widgets stuck to the same width *)
val vgroup : widget list -> widget
(** The first list is packed to the left side of the toolbar.
diff --git a/src/plugins/gui/wfile.mli b/src/plugins/gui/wfile.mli
index b5758b144f975af5ed0730419eef4a286e661872..b9e769747c009185119a6b9391fa81902aebd480 100644
--- a/src/plugins/gui/wfile.mli
+++ b/src/plugins/gui/wfile.mli
@@ -55,7 +55,7 @@ class button :
inherit dialog
inherit [string] selector (** Holds the selected filename, [""] by default. *)
method set_tooltip : (string -> string) -> unit
- (** Set the pretty-printer for tooptip. *)
+ (** Set the pretty-printer for tooltip. *)
method set_display : (string -> string) -> unit
(** Set the pretty-printer for button. *)
end
diff --git a/src/plugins/gui/widget.mli b/src/plugins/gui/widget.mli
index afdbb9810270f725c143fd6987b7b91776209627..5090510f24a744ff624be951b68e1ebee3a45270 100644
--- a/src/plugins/gui/widget.mli
+++ b/src/plugins/gui/widget.mli
@@ -50,7 +50,7 @@ class type ['a] signal =
method lock : (unit -> unit) -> unit
(** If not locked,
- lock and execute the continutation and {i finally} release the lock. *)
+ lock and execute the continuation and {i finally} release the lock. *)
method connect : ('a -> unit) -> unit
(** [connect f] calls [f s] on each signal [s]. *)
@@ -192,7 +192,7 @@ class popup : unit ->
(** Adds an item. *)
method add_separator : unit
(** Inserts a separator.
- Consecutives and trailing separators are eliminated. *)
+ Consecutive and trailing separators are eliminated. *)
method run : unit -> unit
(** Run the menu. *)
end
diff --git a/src/plugins/gui/wpane.ml b/src/plugins/gui/wpane.ml
index 160cdb2b69201770ba456d2be683f939d92cb9b3..b46b12942b9d5fa65e68a9e6641b45a9de9ddfa3 100644
--- a/src/plugins/gui/wpane.ml
+++ b/src/plugins/gui/wpane.ml
@@ -34,8 +34,8 @@ class form () =
let box = GPack.table ~columns:2 ~col_spacings:16 ~homogeneous:false () in
object(self)
val mutable line = 0
- val mutable left = false (* left column feeded on current line *)
- val mutable right = false (* right column feeded on current line *)
+ val mutable left = false (* left column fed on current line *)
+ val mutable right = false (* right column fed on current line *)
val mutable xpadding = 0 (* set with sections *)
inherit Wutil.gobj_widget box
diff --git a/src/plugins/gui/wpane.mli b/src/plugins/gui/wpane.mli
index c50c9466467a44f6fb4bfc9ce402b81181243f3b..b23978d2321154b9d0b463e38f37af67b544a404 100644
--- a/src/plugins/gui/wpane.mli
+++ b/src/plugins/gui/wpane.mli
@@ -50,7 +50,7 @@ class form : unit ->
inherit widget
method add_newline : unit
- (** Inserts an emty line. *)
+ (** Inserts an empty line. *)
method add_section : string -> unit
(** Starts a new section. *)
@@ -129,7 +129,7 @@ type 'a action =
(** Dialog Window.
- Dialog window are asynchroneous and modal. To open the dialog,
+ Dialog window are asynchronous and modal. To open the dialog,
invoke [run]. The method returns immediately. When running, the
main window is no more sensitive (dialog is modal). When an
action-button is pressed, or the method [select] is invoked, the
@@ -148,6 +148,6 @@ class ['a] dialog :
?label:string -> ?icon:icon -> ?tooltip:string ->
unit -> unit (** Closes the dialog. *)
method select : 'a -> unit (** Closes the dialog. *)
- method run : unit -> unit (** Opens the dialog (asynchroneously). *)
+ method run : unit -> unit (** Opens the dialog (asynchronously). *)
inherit ['a] signal (** Emitted when the dialog is closed. *)
end
diff --git a/src/plugins/gui/wtext.mli b/src/plugins/gui/wtext.mli
index 222e391eac1aff5525c6b69417dd8cb6b31d1e0d..e432fd8332b57b02827fe07b8af283fc5665ca8d 100644
--- a/src/plugins/gui/wtext.mli
+++ b/src/plugins/gui/wtext.mli
@@ -70,7 +70,7 @@ class text : ?autoscroll:bool -> ?width:int -> ?indent:int -> unit ->
- ["it"] italic style
- ["ul"] underlined
- ["st"] striked through
- - ["blue"], ["red"], ["orange"], ["green"] predifined foreground color
+ - ["blue"], ["red"], ["orange"], ["green"] predefined foreground color
- ["hover"] background green (default for highlighter)
- ["link"] underlined blue
- ["fg:<color name>"] foreground color
@@ -123,7 +123,7 @@ class text : ?autoscroll:bool -> ?width:int -> ?indent:int -> unit ->
method select : ?scroll:bool -> int -> int -> unit
(** When [scroll:false] (default), only minimal scrolling is performed to make
- the selection visible. Otherwize, the window is scrolled to center the selection
+ the selection visible. Otherwise, the window is scrolled to center the selection
at screen. *)
method get_view: GText.view
diff --git a/src/plugins/impact/compute_impact.ml b/src/plugins/impact/compute_impact.ml
index ff60e8be87aa7ee14a3627dff8cf19dbfa661721..bb4f81d0cdca27d774eb8f3b8fd709b740d3e57d 100644
--- a/src/plugins/impact/compute_impact.ml
+++ b/src/plugins/impact/compute_impact.ml
@@ -54,7 +54,7 @@ and todolist = todo NM.t
(* All nodes that have been found to be impacted. Presented as a map from
Kf, because this information cannot be recovered from the PDG nodes.
- (Also, this speeds up somes operations *)
+ (Also, this speeds up some operations *)
type result = nodes KFM.t
(* Modelization of a call. The first function (the caller) calls the second
@@ -248,7 +248,7 @@ let add_to_do_aux ~init wl kf pdg (pn, zone as n) =
let initial_to_do_list wl kf pdg nodes =
List.iter (fun n -> add_to_do_aux true wl kf pdg n) nodes
-(** Mark a new node as impacted, and simultaneouly mark that it is equivalent
+(** Mark a new node as impacted, and simultaneously mark that it is equivalent
to nodes that are all initial nodes *)
let add_to_do_part_of_initial wl kf pdg n =
add_to_do_aux ~init:true wl kf pdg n;
diff --git a/src/plugins/inout/cumulative_analysis.mli b/src/plugins/inout/cumulative_analysis.mli
index 0d905d5dbd126db37695bc7a1153e26d3ab0d1d1..ddc7f5f6e39981481be945e3d9d45503fdac20ac 100644
--- a/src/plugins/inout/cumulative_analysis.mli
+++ b/src/plugins/inout/cumulative_analysis.mli
@@ -55,7 +55,7 @@ class virtual ['a] cumulative_visitor : object
method virtual compute_kf: kernel_function -> 'a
(** Virtual function to use when one needs to compute the effect
- of a function call. This function carries implictly a context:
+ of a function call. This function carries implicitly a context:
thus calling [self#compute_kf k1; self#compute_kf k2]
is different from calling one within the other *)
end
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index 8f3b5188e5c14e515b3c7d88326e01c075b2eddc..5545a8ab13ac1b89322498ab6b629112ff65030d 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -23,9 +23,9 @@
open Cil_types
open Locations
-(* Computation of over-approximed operational inputs:
- An acurate computation of these inputs needs the computation of
- under-approximed outputs.
+(* Computation of over-approximated operational inputs:
+ An accurate computation of these inputs needs the computation of
+ under-approximated outputs.
*)
type t = Inout_type.t = {
@@ -295,7 +295,7 @@ end) = struct
let new_sure_outs =
if exact then
(* There is only one modified zone. So, this is an exact output.
- Add it into the under-approximed outputs. *)
+ Add it into the under-approximated outputs. *)
Zone.link data.under_outputs_d new_outs
else data.under_outputs_d
in {
diff --git a/src/plugins/loop_analysis/region_analysis.ml b/src/plugins/loop_analysis/region_analysis.ml
index 731cb7447d76b799e16434ca14416fe946cd9ca4..737b2f8bc1552a06acebf94b01b4f2ed2f54d3c0 100644
--- a/src/plugins/loop_analysis/region_analysis.ml
+++ b/src/plugins/loop_analysis/region_analysis.ml
@@ -37,7 +37,7 @@
would mean creation of closures or a costly substitution; this
algorithm avoids function composition.
- The algorithm could be extended to handle non-natural loops. Intead
+ The algorithm could be extended to handle non-natural loops. Instead
of using the notion of back edges, we could use that of retreating
edge, starting from a spanning tree of the graph. It should be
possible to compile strongly connected components with multiple
@@ -51,7 +51,7 @@
include Region_analysis_sig;;
module Make(N:Node):sig
- (* Function computing from an entry abstracat value the "after"
+ (* Function computing from an entry abstract value the "after"
state, which is a map from each outgoing edge to its respective
value. *)
val after: N.abstract_value -> N.abstract_value N.Edge_Dict.t
diff --git a/src/plugins/loop_analysis/region_analysis.mli b/src/plugins/loop_analysis/region_analysis.mli
index dd692a28d184e09cadd15c4ee96b6baefacff5a2..de502a6823218a197133f223a61bc42bbf6ff2b4 100644
--- a/src/plugins/loop_analysis/region_analysis.mli
+++ b/src/plugins/loop_analysis/region_analysis.mli
@@ -34,7 +34,7 @@
include module type of Region_analysis_sig;;
module Make(N:Node):sig
- (* Function computing from an entry abstracat value the "after"
+ (* Function computing from an entry abstract value the "after"
state, which is a map from each outgoing edge to its respective
value. *)
val after: N.abstract_value -> N.abstract_value N.Edge_Dict.t
diff --git a/src/plugins/metrics/metrics_base.mli b/src/plugins/metrics/metrics_base.mli
index ca6509b1fb57536b727d03e16806f457544a46e6..e48d4864b2cc591fa88ca53ebfd63f50ff38038c 100644
--- a/src/plugins/metrics/metrics_base.mli
+++ b/src/plugins/metrics/metrics_base.mli
@@ -82,7 +82,7 @@ module BasicMetrics : sig
(** Compute cyclomatic complexity from base_metrics record type. *)
val compute_cyclo: t -> int;;
- (** Matrix-like representation of the record in "Title: value" stytle *)
+ (** Matrix-like representation of the record in "Title: value" style *)
val to_list : t -> string list list ;;
(** Pretty printers for base metrics as text or html. *)
@@ -93,7 +93,7 @@ end
;;
(** Local varinfo map and set where the comparison function is the
- lexicographic one on their respectives names. *)
+ lexicographic one on their respective names. *)
module VInfoMap: FCMap.S with type key = Cil_types.varinfo
module VInfoSet: FCSet.S with type elt = Cil_types.varinfo
;;
diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml
index 754c4e5921929f49e8339994136b44e17b6c906d..261399b5f0fd6fe6f75593b1b70e48e553eb4fbb 100644
--- a/src/plugins/metrics/metrics_cilast.ml
+++ b/src/plugins/metrics/metrics_cilast.ml
@@ -49,7 +49,7 @@ class type sloc_visitor = object
(* Global variables with 'Extern' storage *)
method extern_global_vars: Metrics_base.VInfoSet.t
- (* Get the computed metris *)
+ (* Get the computed metrics *)
method get_metrics: BasicMetrics.t
(* Print the metrics of a file [string] to a formatter
diff --git a/src/plugins/metrics/metrics_cilast.mli b/src/plugins/metrics/metrics_cilast.mli
index db6eb4d07427251e94485ab7cb8160e6ea407723..96e240ddffb78cf0ffaa602f91e84b74085b34db 100644
--- a/src/plugins/metrics/metrics_cilast.mli
+++ b/src/plugins/metrics/metrics_cilast.mli
@@ -37,7 +37,7 @@ class type sloc_visitor = object
method fundef_calls: int Metrics_base.VInfoMap.t
method extern_global_vars: Metrics_base.VInfoSet.t
- (* Get the computed metris *)
+ (* Get the computed metrics *)
method get_metrics: Metrics_base.BasicMetrics.t
(* Print the metrics of a file [string] to a formatter
diff --git a/src/plugins/metrics/metrics_coverage.mli b/src/plugins/metrics/metrics_coverage.mli
index 0227d3da6106150a0733fc5e9e296328055e7b67..5a9a387e17823c5c26f98410578af79047bd5102 100644
--- a/src/plugins/metrics/metrics_coverage.mli
+++ b/src/plugins/metrics/metrics_coverage.mli
@@ -39,7 +39,7 @@ type coverage_metrics = {
val percent_coverage : coverage_metrics -> float ;;
val compute : libc:bool -> coverage_metrics ;;
-(** Computes both syntatic and semantic coverage information. *)
+(** Computes both syntactic and semantic coverage information. *)
val compute_coverage_by_fun: Cil_datatype.Varinfo.Set.t ->
(Cil_types.kernel_function * int * int * float) list
@@ -61,7 +61,7 @@ class semantic_printer : libc:bool -> coverage_metrics -> object
method pp_value_coverage: Format.formatter -> unit
(** Pretty-print value coverage information, including functions
- syntacticallly and semantically reachable from the entry point,
+ syntactically and semantically reachable from the entry point,
as well as coverage percentage. *)
method pp_stmts_reached_by_function: Format.formatter -> unit
diff --git a/src/plugins/metrics/metrics_gui.ml b/src/plugins/metrics/metrics_gui.ml
index cc2c0c388fa688a33e2cb66ad32989b88ecb88c4..ed160ff8b19d0e11410b15c155e9a57b05572cbb 100644
--- a/src/plugins/metrics/metrics_gui.ml
+++ b/src/plugins/metrics/metrics_gui.ml
@@ -28,7 +28,7 @@ type ('a, 'b, 'c) metrics_panel = {
;;
(* The option type for top and bottom GTK objects is compulsory in order not to
- have warnings at runtim.
+ have warnings at runtime.
Creation of GTK objects cannot be made before the general window is
initialized.
The option type with a None value marks the fact that this value is not
@@ -110,7 +110,7 @@ let reset_panel _ =
let coerce_panel_to_ui panel_box _main_ui = "Metrics", panel_box#coerce, None ;;
(** Add a new metrics to its dedicated panel.
- The text is added to the combox box while the action is added to the
+ The text is added to the combo box while the action is added to the
association lists of possible actions.
*)
let register_metrics name display_function =
diff --git a/src/plugins/metrics/metrics_gui.mli b/src/plugins/metrics/metrics_gui.mli
index 8b6d2d657ab873af77a655951c1d1f4321d6ebb1..682d3edbbf9bfcc0c1a9a5bed673515cc49dff85 100644
--- a/src/plugins/metrics/metrics_gui.mli
+++ b/src/plugins/metrics/metrics_gui.mli
@@ -31,10 +31,10 @@ val init_panel : Design.main_window_extension_points -> GPack.box ;;
(** @returns a value allowing to register the panel into the main GUI *)
val coerce_panel_to_ui : < coerce : 'a; .. > -> 'b -> string * 'a * 'c option ;;
-(** Diplay the list of list of strings in a LablgGTK table object *)
+(** Display the list of list of strings in a LablGTK table object *)
val display_as_table : string list list -> GPack.box -> unit ;;
-(** Reset metrics panel to pristine conditions by removeing children from
+(** Reset metrics panel to pristine conditions by removing children from
bottom container
*)
val reset_panel : 'a -> unit ;;
diff --git a/src/plugins/metrics/metrics_parameters.mli b/src/plugins/metrics/metrics_parameters.mli
index fbb029f3b28cdbc4930f89e398db93acaf1bed90..d5f1da0fc6d4a0c89b82e549413bb474a6f7c87a 100644
--- a/src/plugins/metrics/metrics_parameters.mli
+++ b/src/plugins/metrics/metrics_parameters.mli
@@ -33,7 +33,7 @@ module ValueCoverage: Parameter_sig.With_output
Only works on CIL AST. *)
module AstType: Parameter_sig.String
-(** Set the ASTs on which the metrics should be computetd *)
+(** Set the ASTs on which the metrics should be computed *)
module OutputFile: Parameter_sig.String
(** Pretty print metrics to the given file.
diff --git a/src/plugins/pdg/build.ml b/src/plugins/pdg/build.ml
index 70962e4421b66b83bd82f5be072aba735ae65cc0..886b976570fa46236e1c763f6f89e446e37e2448 100644
--- a/src/plugins/pdg/build.ml
+++ b/src/plugins/pdg/build.ml
@@ -22,12 +22,12 @@
(** Build graphs (PDG) for the function
(see module {!module: Build.BuildPdg})
- to represente the dependencies between instructions
+ to represent the dependencies between instructions
in order to use it for slicing purposes.
A function is processed using a forward dataflow analysis
(see module {{: ../html/Dataflow2.html}Dataflow2}
- which is instanciated with the module
+ which is instantiated with the module
{!module: Build.Computer} below).
*)
@@ -346,7 +346,7 @@ let is_variadic kf =
Pdg_state.add_loc_node state_before_call exact l_loc new_node in
new_state
- (** for skip statement : we want to add a node in the PDG in ordrer to be able
+ (** for skip statement : we want to add a node in the PDG in order to be able
* to store information (like marks) about this statement later on *)
let process_skip pdg _state stmt =
ignore (add_elem pdg (Key.stmt_key stmt));
@@ -445,7 +445,7 @@ let is_variadic kf =
let process_jump pdg stmt controlled_stmts =
ignore (mk_jump_node pdg stmt controlled_stmts)
- (** like [process_jump] but also add data dependencies on the datas and their
+ (** like [process_jump] but also add data dependencies on the data and their
declarations. Use for conditional jumps and returns.
*)
let process_jump_with_exp pdg stmt controlled_stmts state loc_cond decls_cond =
diff --git a/src/plugins/pdg/ctrlDpds.ml b/src/plugins/pdg/ctrlDpds.ml
index 1485dad9c6ce81b547c7b463bf7f72ba9e7b5900..2ce81a28ecff14d580ff41dfebd7b7cdf0f11cde 100644
--- a/src/plugins/pdg/ctrlDpds.ml
+++ b/src/plugins/pdg/ctrlDpds.ml
@@ -152,7 +152,7 @@ end = struct
end
(*============================================================================*)
-(** Postdominators (with infine path extension) *)
+(** Postdominators (with infinite path extension) *)
(*============================================================================*)
(** This backward dataflow implements a variant of postdominators that verify
the property P enunciated in bts 963: a statement postdominates itself
diff --git a/src/plugins/pdg/pdg_state.ml b/src/plugins/pdg/pdg_state.ml
index 2d7bd3c0b441ea695c5bd8472a5aeb035baa54c2..ee2560cec085efff4858ef342d0a8907efd0c4d9 100644
--- a/src/plugins/pdg/pdg_state.ml
+++ b/src/plugins/pdg/pdg_state.ml
@@ -113,7 +113,7 @@ let get_loc_nodes_and_part state loc =
let z =
if Locations.Zone.equal loc z
then Some loc
- (* Be carreful not ot put None here, because if we have n_1 : (s1 =
+ (* Be careful not ot put None here, because if we have n_1 : (s1 =
s2) and then n_2 : (s1.b = 3) the state looks like :
s1.a -> n_1; s1.b -> n_2 ; s1.c -> n_1. And if we
look for s1.a in that state, we get n_1 but this node
diff --git a/src/plugins/pdg/sets.ml b/src/plugins/pdg/sets.ml
index a039fab7d60ab364b4ef6b8de64adde79b5f33f3..2ecfd16cb5ad2f89043bf4205ee9ef80b37dd216 100644
--- a/src/plugins/pdg/sets.ml
+++ b/src/plugins/pdg/sets.ml
@@ -151,7 +151,7 @@ let find_location_nodes_at_stmt pdg stmt ~before loc =
let find_location_nodes_at_end pdg loc =
find_loc_nodes pdg (get_last_state pdg) loc
-(* be carreful that begin is different from init because
+(* be careful that begin is different from init because
* init_state only contains implicit inputs
* while begin contains only formal arguments *)
let find_location_nodes_at_begin pdg loc =
diff --git a/src/plugins/pdg_types/pdgIndex.ml b/src/plugins/pdg_types/pdgIndex.ml
index 22f7ebafcc2a0170afdb2782fb67e8fc4a520fa8..975adc7bf5220c15ade5b67bcb0ebc68edc016da 100644
--- a/src/plugins/pdg_types/pdgIndex.ml
+++ b/src/plugins/pdg_types/pdgIndex.ml
@@ -419,7 +419,7 @@ module RKey = struct
| Key.VarDecl v -> 17 * Cil_datatype.Varinfo.hash v
| Key.Stmt s -> 29 * Cil_datatype.Stmt.hash s
| Key.Label (s, _l) ->
- (* Intentionnaly buggy: ignore the label and consider only the statement.
+ (* Intentionally buggy: ignore the label and consider only the statement.
There seems to be bug in the pdg, only one 'case :' per statement is
present. This avoids removing the other 'case' clauses
(see tests/slicing/switch.c *)
@@ -444,7 +444,7 @@ end
module FctIndex = struct
type ('node_info, 'call_info) t = {
- (** inputs and ouputs of the function *)
+ (** inputs and outputs of the function *)
mutable sgn : 'node_info Signature.t ;
(** calls signatures *)
mutable calls :
diff --git a/src/plugins/pdg_types/pdgMarks.mli b/src/plugins/pdg_types/pdgMarks.mli
index 41d190ed2933b157865d6dfdf6a874351be45d48..cec8092445797ed824f9c1f1f3d4a51392177216 100644
--- a/src/plugins/pdg_types/pdgMarks.mli
+++ b/src/plugins/pdg_types/pdgMarks.mli
@@ -23,11 +23,11 @@
(** This module provides elements to mapped information (here called 'marks')
* to PDG elements and propagate it along the dependencies.
*
-* Some more functions are defined in the PDG pluggin itself
+* Some more functions are defined in the PDG plugin itself
* (in [pdg/marks]):
* the signatures of these public functions can be found in file [Pdg.mli] *)
-(** Signature of the module to use in order to instanciate the computation *)
+(** Signature of the module to use in order to instantiate the computation *)
module type Mark = sig
(** type of the information mapped to the nodes *)
@@ -129,7 +129,7 @@ type 't_mark call_m2m =
Cil_types.stmt option -> PdgTypes.Pdg.t -> 't_mark m2m
(** this is the type of the functor dedicated to interprocedural propagation.
- It is defined in PDG pluggin *)
+ It is defined in PDG plugin *)
module type Proj = sig
type t
diff --git a/src/plugins/pdg_types/pdgTypes.ml b/src/plugins/pdg_types/pdgTypes.ml
index d4298f06f06e41e55d5e38f9345b3eb62838ea6b..79856f8e41eec00c6774d774a5f0f3c9bd8405e1 100644
--- a/src/plugins/pdg_types/pdgTypes.ml
+++ b/src/plugins/pdg_types/pdgTypes.ml
@@ -267,7 +267,7 @@ end
module G = struct
(* Hashtbl to maps of nodes to dpdzone. Used to encode one-directional graphs
- whoses nodes are Node.t, and labels on edges are DpdZone. *)
+ whose nodes are Node.t, and labels on edges are DpdZone. *)
module E = struct
type t = Node.t * DpdZone.t * Node.t
type label = DpdZone.t
diff --git a/src/plugins/pdg_types/pdgTypes.mli b/src/plugins/pdg_types/pdgTypes.mli
index d9bd5d9f52958d746e6293365a20f99fcb0d6e75..4a3d4a35ad957474e7bccd28b45d09bf7a0e34cc 100644
--- a/src/plugins/pdg_types/pdgTypes.mli
+++ b/src/plugins/pdg_types/pdgTypes.mli
@@ -119,7 +119,7 @@ module Pdg : sig
exception Top
(** can be raised by most of the functions when called with a Top PDG.
- Top means that we were not abled to compute the PDG for this
+ Top means that we were not able to compute the PDG for this
function. *)
exception Bottom
diff --git a/src/plugins/report/tests/report/multi_emitters.ml b/src/plugins/report/tests/report/multi_emitters.ml
index 43884570e53e20b6668d3f51a18d6d34677dfa5d..055953df5d1a0b7a9626fe21dd0ea713909c773a 100644
--- a/src/plugins/report/tests/report/multi_emitters.ml
+++ b/src/plugins/report/tests/report/multi_emitters.ml
@@ -32,9 +32,9 @@ let main () =
print_status ();
set_status emitter1 Property_status.Dont_know;
set_status emitter2 Property_status.Dont_know;
- (* unknow /\ unknown *)
+ (* unknown /\ unknown *)
print_status ();
- (* unknow /\ true *)
+ (* unknown /\ true *)
set_status emitter1 Property_status.True;
print_status ();
(* true /\ true *)
diff --git a/src/plugins/rte/options.ml b/src/plugins/rte/options.ml
index 1d81cea21e8f55382a67ff694795779abaad16d9..772eab7ab707a7f42b2c5efce66edc5d0826f686 100644
--- a/src/plugins/rte/options.ml
+++ b/src/plugins/rte/options.ml
@@ -95,7 +95,7 @@ they trivially hold"
(* For functions having an ACSL contract,
generates a corresponding statement contract before each function's call
- statement (provided the call is not performed thorugh a function pointer).
+ statement (provided the call is not performed through a function pointer).
*)
module DoCalledPrecond =
False
diff --git a/src/plugins/rte/rte.ml b/src/plugins/rte/rte.ml
index 6261cfd879faa0b3a40cf9ad05d7b466ae4d38f0..c2c72c0fc70cc9ede02b5a9ef154ceabbf1b9e04 100644
--- a/src/plugins/rte/rte.ml
+++ b/src/plugins/rte/rte.ml
@@ -213,7 +213,7 @@ let signed_div_assertion ~remove_trivial ~on_alarm (exp, lexp, rexp) =
(* Signed division: overflow occurs when dividend is equal to the
the minimum (negative) value for the signed integer type,
and divisor is equal to -1. Under the hypothesis (cf Value) that
- integers are represented in two's completement.
+ integers are represented in two's complement.
Nothing done for modulo (the result of TYPE_MIN % -1 is 0, which does not
overflow).
Still it may be dangerous on a number of compilers / architectures
@@ -255,7 +255,7 @@ let shift_alarm ~remove_trivial ~on_alarm (exp, upper_bound) =
| None -> alarm ()
| Some c64 ->
(* operand is constant:
- check it is nonnegative and stricly less than the upper bound (if
+ check it is nonnegative and strictly less than the upper bound (if
any) *)
let upper_bound_ok = match upper_bound with
| None -> true
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index 682c55293e63089d1c2492b3417b574e45373068..71134d7870d57dda8fda18cff3477d30384650ea 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -484,10 +484,10 @@ class annot_visitor kf to_annot on_alarm = object (self)
(* Looking for management of default assigns clause. *)
(match Ast_info.merge_assigns_from_complete_bhvs ~warn:false bhvs [] with
WritesAny ->
- (* Case 1: it isn't possible to find good assigns from ungarded
+ (* Case 1: it isn't possible to find good assigns from unguarded
behaviors. S, looks at assigns from complete behaviors clauses. *)
(match Ast_info.merge_assigns_from_complete_bhvs
- ~warn:true ~ungarded:false bhvs spec.spec_complete_behaviors
+ ~warn:true ~unguarded:false bhvs spec.spec_complete_behaviors
with
| WritesAny ->
(* Case 1.1: no better thing to do than nothing *)
@@ -574,7 +574,7 @@ class annot_visitor kf to_annot on_alarm = object (self)
in
(* Update the dependencies between the original require, and the
copy at the syntactic call-site. Done once all the requires
- and behaviors have been created by the visitore *)
+ and behaviors have been created by the visitor *)
let requires_deps () =
let kf_call = Kernel_function.find_englobing_kf call_stmt in
let ki_call = Kstmt call_stmt in
@@ -894,7 +894,7 @@ let annotate_kf kf =
let do_precond kf =
annotate_kf_aux { annotate_nothing with precond = true } kf
-(* annonate for all rte + unsigned overflows (which are not rte), for a given
+(* annotate for all rte + unsigned overflows (which are not rte), for a given
function *)
let do_all_rte kf =
let to_annot =
diff --git a/src/plugins/scope/datascope.ml b/src/plugins/scope/datascope.ml
index 194f39772b89dc6582311c5edd453b41ff2628dd..81e9e55e5d636c10d9e1114a97d7af059d61974e 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -440,7 +440,7 @@ let get_prop_scope_at_stmt kf stmt ?(proven=CA_Map.empty) annot =
"[get_annot_zone] don't know how to compute zone: skip this annotation";
acc
-(** Collect the annotations that can be removed because they are redondant. *)
+(** Collect the annotations that can be removed because they are redundant. *)
class check_annot_visitor = object(self)
inherit Visitor.frama_c_inplace
@@ -485,7 +485,7 @@ let f_check_asserts () =
visitor#proven ()
let check_asserts () =
- R.feedback "check if there are some redondant assertions...";
+ R.feedback "check if there are some redundant assertions...";
let to_be_removed = f_check_asserts () in
let n = CA_Map.cardinal to_be_removed in
R.result "[check_asserts] %d assertion(s) could be removed@." n;
diff --git a/src/plugins/scope/dpds_gui.ml b/src/plugins/scope/dpds_gui.ml
index b0052bb9de9e28f933f82c883b6804486618fc43..ad052a26ef819e569bb269908ffb7943e701b027 100644
--- a/src/plugins/scope/dpds_gui.ml
+++ b/src/plugins/scope/dpds_gui.ml
@@ -484,7 +484,7 @@ let check_value (main_ui:Design.main_window_extension_points) =
else false
-(** To add a sensitive/unsensitive menu item to a [factory].
+(** To add a sensitive/insensitive menu item to a [factory].
* The menu item is insensitive when [arg_opt = None],
* else, when the item is selected, the callback is called with the argument.
* If [~use_values], check if the value analysis has been computed.
diff --git a/src/plugins/security_slicing/components.ml b/src/plugins/security_slicing/components.ml
index 88e7c23c8ec776993b453c14d003c3a8340e12cd..0e01b7962fc8419eef13f58e95856f4a201a3b9c 100644
--- a/src/plugins/security_slicing/components.ml
+++ b/src/plugins/security_slicing/components.ml
@@ -202,7 +202,7 @@ end = struct
current_kf =
{ fundec =
(* do not use Cil.emptyFunction here since it changes the
- numerotation of variables *)
+ numbering of variables *)
Declaration
(spec,
Cil_datatype.Varinfo.dummy,
diff --git a/src/plugins/slicing/fct_slice.ml b/src/plugins/slicing/fct_slice.ml
index 5b85b043ed0005ff10ce18fff83f97690b8408f4..42124fa3651d7099b0245d0b231a697e4bcda7e7 100644
--- a/src/plugins/slicing/fct_slice.ml
+++ b/src/plugins/slicing/fct_slice.ml
@@ -835,7 +835,7 @@ let after_marks_modifications ff to_prop =
let apply_examine_calls ff call_outputs = examine_calls ff call_outputs
(** quite internal function that only computes the marks.
-* Dont't use it alone because it doesn't take care of the calls and so on.
+* Don't use it alone because it doesn't take care of the calls and so on.
* See [apply_add_marks] or [add_marks_to_fi] for higher level functions. *)
let add_marks fct_marks nodes_marks =
SlicingParameters.debug ~level:2 "add_marks@.";
diff --git a/src/plugins/slicing/register_gui.ml b/src/plugins/slicing/register_gui.ml
index 8d3296a006d3eca0e2d653f3c8adb86c6a971f31..bf6a38b55a378057cf5d6475fd9e8d67110e04a5 100644
--- a/src/plugins/slicing/register_gui.ml
+++ b/src/plugins/slicing/register_gui.ml
@@ -64,7 +64,7 @@ let mk_slice selection =
!Db.Slicing.Project.set_project (Some project);
new_project
-(* To add a sensitive/unsensitive menu item to a [factory] *)
+(* To add a sensitive/insensitive menu item to a [factory] *)
let add_item (factory:GMenu.menu GMenu.factory) ~callback name arg_opt =
match arg_opt with
| None ->
diff --git a/src/plugins/slicing/slicingActions.ml b/src/plugins/slicing/slicingActions.ml
index 2631b4dc299a29775a1c067d9a72e0c16629d569..70590fb5fd0f8ca0f0b7ac947a65e40ab8a96f20 100644
--- a/src/plugins/slicing/slicingActions.ml
+++ b/src/plugins/slicing/slicingActions.ml
@@ -21,7 +21,7 @@
(**************************************************************************)
(** This module deals with the action management.
- * It consiste of the definitions of the different kind of actions,
+ * It consists of the definitions of the different kinds of actions,
* and the management of the action list.
*)
diff --git a/src/plugins/slicing/slicingCmds.ml b/src/plugins/slicing/slicingCmds.ml
index b74fe55619d0a127c1dc30d0fd28b9ab590d477a..529f0446efa26fa84cd169475ccbd5b1ba4023f8 100644
--- a/src/plugins/slicing/slicingCmds.ml
+++ b/src/plugins/slicing/slicingCmds.ml
@@ -81,7 +81,7 @@ struct
assert (Db.Value.is_computed ());
let lval_process read_zone stmt 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
+ (* The modified locations are [looking_for], those address are
function of [deps]. *)
let state = Db.Value.get_stmt_state stmt in
let deps, zloc, _exact =
@@ -158,7 +158,7 @@ let select_stmt set ~spare stmt kf =
(** Add a selection to the entrance of the function [kf]
and add a selection to its return if [~return] is true
and add a selection to [~inputs] parts of its inputs
- and add a selection to [~ouputs] parts of its outputs*)
+ and add a selection to [~outputs] parts of its outputs*)
let select_entry_point_and_some_inputs_outputs set ~mark kf ~return ~outputs ~inputs =
SlicingParameters.debug ~level:3
"select_entry_point_and_some_inputs_outputs %a"
@@ -245,7 +245,7 @@ let select_func_calls_to set ~spare kf =
generic_select_func_calls select_stmt set ~spare kf
(** Registered as a slicing selection function:
- Add selection of function ouputs. *)
+ Add selection of function outputs. *)
let select_func_zone set mark zone kf =
let selection = !Db.Slicing.Select.select_zone_at_end_internal kf zone mark
in add_to_selection set selection
@@ -529,7 +529,7 @@ let select_func_annots set mark ~spare ~threat ~user_assert ~slicing_pragma ~loo
in select_ZoneAnnot_zones_decl_vars set mark (get_or_raise zones_decl_vars) kf
(** Registered as a slicing selection function:
- Add selection of function ouputs.
+ Add selection of function outputs.
Variables of [lval_str] string are bounded
relatively to the whole scope of the function [kf].
The interpretation of the address of the lvalues is
diff --git a/src/plugins/slicing/slicingMarks.ml b/src/plugins/slicing/slicingMarks.ml
index e8c03f7edb316b5d868594f5875f50dc49220e35..ad00843722dd49bd4efeb3adcba6303ec8d6d69d 100644
--- a/src/plugins/slicing/slicingMarks.ml
+++ b/src/plugins/slicing/slicingMarks.ml
@@ -29,7 +29,7 @@ let debug = false
(**/**)
(** a [Mark] is used to represent some information about the status of
- * a PDF element in a slice.
+ * a PDG element in a slice.
*)
module Mark : sig
val bottom : SlicingInternals.mark
@@ -337,7 +337,7 @@ module SigMarks = struct
Signature.fold_all_inputs (fun acc (_, m) -> MarkPair.merge_user_marks acc m)
bottom_mark cm
- (** @return an under-approxamation of the mark for the given location.
+ (** @return an under-approximation of the mark for the given location.
* If the location is not included in the union of the implicit inputs,
* it returns bottom.
* Else, it returns the intersection of the inputs that intersect the location.
diff --git a/src/plugins/slicing/slicingProject.ml b/src/plugins/slicing/slicingProject.ml
index 74b74a5d774ee4f3d6489bd1a89a0890b85aeeaf..39ff546ca446f1f30b8ebc94e01a30598ade4244 100644
--- a/src/plugins/slicing/slicingProject.ml
+++ b/src/plugins/slicing/slicingProject.ml
@@ -224,7 +224,7 @@ let pretty_slice fmt ff =
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
(** {2 Managing (and applying) requests} *)
-(** apply the given criterion and returns the list of new criterions to
+(** apply the given criterion and returns the list of new criteria to
add to the project worklist. *)
let apply_fct_crit ff to_select =
let actions = Fct_slice.apply_add_marks ff to_select in
diff --git a/src/plugins/slicing_types/slicingInternals.ml b/src/plugins/slicing_types/slicingInternals.ml
index 986a4ccca31e1029591952ab029ced956ad094b0..2f7b8263fb3260f340707cfe5755b6a3c108bf0c 100644
--- a/src/plugins/slicing_types/slicingInternals.ml
+++ b/src/plugins/slicing_types/slicingInternals.ml
@@ -153,7 +153,7 @@ and
and
(** Base criterion for the functions. These are the only one that can
- really generate function slices. All the other criterions are
+ really generate function slices. All the other criteria are
translated in more basic ones.
Note that to build such a base criterion, the PDG has to be already
computed.
@@ -212,7 +212,7 @@ and
* When it a a slice, it might be an existing slice that will be modified,
* or a new one will be created during application.
* When it is the source function, it means what the criterion has to be
- * applied on each existing slice, and stored into the inititial marks of
+ * applied on each existing slice, and stored into the initial marks of
* the function.
*)
cf_info : fct_crit
diff --git a/src/plugins/slicing_types/slicingTypes.ml b/src/plugins/slicing_types/slicingTypes.ml
index 5ea4c68a4bac0e21240fb946b4f37acc7bbf265c..d8639a98542c3e338acecaf73cffd88caaaa4d1a 100644
--- a/src/plugins/slicing_types/slicingTypes.ml
+++ b/src/plugins/slicing_types/slicingTypes.ml
@@ -32,7 +32,7 @@ exception WrongSlicingLevel
* *)
exception OnlyOneEntryPointSlice
-(** raised when one triesy to select something in a function where we are not
+(** raised when one tries to select something in a function where we are not
* able to compute the Pdg. *)
exception NoPdg
@@ -141,7 +141,7 @@ let pp_sl_mark p fmt m =
| _, SlicingInternals.Spare -> None
| SlicingInternals.Cav mark1, SlicingInternals.Cav mark2 ->
if (PdgTypes.Dpd.is_bottom mark2) then
- (* use [!Db.Slicing.Mark.make] contructor *)
+ (* use [!Db.Slicing.Mark.make] constructor *)
Some (fun fmt ->
Format.fprintf fmt "@[<hv 2>!Db.Slicing.Mark.make@;~addr:%b@;~data:%b@;~ctrl:%b@]"
(PdgTypes.Dpd.is_addr mark1)
diff --git a/src/plugins/sparecode/globs.ml b/src/plugins/sparecode/globs.ml
index 51046be16b70fa4cb956691fbee47134e375d4b8..d7935fb3720bc26648a9b362f7a35014ba44a5f8 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 comparison
+ (* we use the type name because direct 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/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index 227b168541295dffd1f83cdf5dc972100aebdc72..37403ba54711d17cf62db58242ffde7196d45a77 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -179,9 +179,9 @@ module type Transfer = sig
- [kinstr] is the statement of the assignment, or Kglobal for the
initialization of a global variable.
- [v] carries the value being assigned to [lv], i.e. the value of the
- expression [expr]. [v] also denotes the kind of assignement: Assign for
+ expression [expr]. [v] also denotes the kind of assignment: Assign for
the default assignment of the value, or Copy for the exact copy of a
- location if the right expresssion [expr] is a lvalue.
+ location if the right expression [expr] is a lvalue.
- [valuation] is a cache of all sub-expressions and locations computed
for the evaluation of [lval] and [expr]; it can also be used to reduce
the state. *)
diff --git a/src/plugins/value/domains/apron/apron_domain.ok.ml b/src/plugins/value/domains/apron/apron_domain.ok.ml
index 0957fcc10ca2f4053662d29d02e623073840fa68..aa450924e547c6546a5d97b021687054d74c937f 100644
--- a/src/plugins/value/domains/apron/apron_domain.ok.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ok.ml
@@ -282,7 +282,7 @@ let rec translate_expr eval oracle expr = match expr.enode with
match Cil.constFoldToInt expr with
| None -> raise (Out_of_Scope "translate_expr sizeof alignof")
| Some i -> Texpr1.Cst (Coeff.s_of_int (Integer.to_int i))
-(* Expresssions that cannot be translated by [translate_expr] are replaced
+(* Expressions that cannot be translated by [translate_expr] are replaced
using an oracle. Of course, this oracle must be sound!. If the oracle
cannot find a suitable replacement, it can re-raise the expresssion. *)
and translate_expr_linearize eval oracle expr =
diff --git a/src/plugins/value/domains/cvalue/builtins_malloc.ml b/src/plugins/value/domains/cvalue/builtins_malloc.ml
index 935bdbda827557f989c1788f97691810d5be9ed2..5b3e7281e6f92ee07eb7a532e89280c890419477 100644
--- a/src/plugins/value/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/value/domains/cvalue/builtins_malloc.ml
@@ -242,7 +242,7 @@ let add_uninitialized state base max_valid_bits =
let new_offsm =
try
let cur = match Model.find_base_or_default base state with
- | `Top -> assert false (* Value nevers passes Top as state *)
+ | `Top -> assert false (* Value never passes Top as state *)
| `Bottom -> assert false (* implicitly checked by offsm_with_uninit *)
| `Value m -> m
in
@@ -402,10 +402,10 @@ let () = Builtins.register_builtin
(** {1 Free} *)
(* Change all references to bases into ESCAPINGADDR into the given state,
- and remove thoses bases from the state entirely when [exact] holds *)
+ and remove those bases from the state entirely when [exact] holds *)
let free ~exact bases state =
(* No need to remove the freed bases from the state if [exact] is false,
- because they must remain for the 'unexact' case *)
+ because they must remain for the 'inexact' case *)
let state =
if exact then Base.Hptset.fold Cvalue.Model.remove_base bases state
else state
@@ -538,7 +538,7 @@ let realloc_alloc_copy loc weak bases_to_realloc null_in_arg sizev state =
(* get bases to free and copy *)
let lbases = Base.Hptset.elements bases_to_realloc in
let dst_state =
- (* unitialized on all reallocated valid bits *)
+ (* uninitialized on all reallocated valid bits *)
let offsm = offsm_with_uninit (Base.validity base) max_valid in
let offsm =
if null_in_arg then offsm (* In this case, realloc may copy nothing *)
@@ -585,7 +585,7 @@ let realloc_multiple loc state size bases null =
join res (realloc_alloc_copy loc Strong Base.Hptset.empty true size state)
else res
-(* Multiple indicates that existing bases are reallocateed into as many new
+(* Multiple indicates that existing bases are reallocated into as many new
bases. *)
let realloc ~multiple state args = match args with
| [ (eptr,ptr,_); (_,size,_) ] ->
diff --git a/src/plugins/value/domains/cvalue/builtins_nonfree.ml b/src/plugins/value/domains/cvalue/builtins_nonfree.ml
index 71186b33dc1a87b814ae13a7b7c677775c298037..e6086eb1dfd5ab1203af263eefbd0fbea6a1d0a6 100644
--- a/src/plugins/value/domains/cvalue/builtins_nonfree.ml
+++ b/src/plugins/value/domains/cvalue/builtins_nonfree.ml
@@ -94,7 +94,7 @@ exception Memcpy_result of (Cvalue.Model.t * Function_Froms.froms * Zone.t)
exception Indeterminate of V_Or_Uninitialized.t
(* Called by the [memcpy] builtin. Warns when the offsetmap contains
- an indterminate value, when the imprecision category is enabled *)
+ an indeterminate value, when the imprecision category is enabled *)
let memcpy_check_indeterminate_offsetmap offsm =
if Value_parameters.is_debug_key_enabled dkey then
try
@@ -663,7 +663,7 @@ let memset_typ_offsm_int full_typ i =
(* Type-aware memset on an entire type. Same as [memset_typ_offsm_int], but
with a [Cvalue.V] instead of an integer. We accept [-ilevel] different
possible values in [v] before falling back to the imprecise memset.
- May rais {!ImpreciseMemset}. *)
+ May raise {!ImpreciseMemset}. *)
let memset_typ_offsm typ v =
try
let i = V.project_ival v in
diff --git a/src/plugins/value/domains/cvalue/builtins_nonfree_print_c.mli b/src/plugins/value/domains/cvalue/builtins_nonfree_print_c.mli
index 9ed3ea213325ecb43eb164053eb7f3a29d1809e1..f0bc35faa513774ed80a60340cf6805680c6d7f1 100644
--- a/src/plugins/value/domains/cvalue/builtins_nonfree_print_c.mli
+++ b/src/plugins/value/domains/cvalue/builtins_nonfree_print_c.mli
@@ -14,7 +14,7 @@
(** Translate a Value state into a bunch of C assertions *)
(** This file is experimental, and partly tuned to Csmith programs. In
- particular, it might not follow your machedp, or fail to translate
+ particular, it might not follow your machdep, or fail to translate
some variables. Use at your own risk *)
val pretty_state_as_c_assert: Cvalue.Model.t Pretty_utils.formatter
diff --git a/src/plugins/value/domains/cvalue/builtins_string.ml b/src/plugins/value/domains/cvalue/builtins_string.ml
index 46c694600819793ccfa69421f0b81f900ece09a8..794e05dc6dbdf59125304e159e4e89caaed6f5c0 100644
--- a/src/plugins/value/domains/cvalue/builtins_string.ml
+++ b/src/plugins/value/domains/cvalue/builtins_string.ml
@@ -210,7 +210,7 @@ type imprecise_builtin =
let bytes_of_bits ?inexact i =
if I.(i % eight <> zero) &&
match inexact with | Some b -> not b | None -> true then
- (* message for debugging purposes motly, should not happen *)
+ (* message for debugging purposes mostly, should not happen *)
Value_parameters.warning "bytes_of_bits: inexact division (%a / 8)"
Int.pretty i;
I.(i / eight)
@@ -576,7 +576,7 @@ let ival_of_opt_int_pair = function
[maybe_found_stop] is used to indicate, in the case where [bounds] is [None],
whether the stopping character has possibly been found *before* the searched
character (which implies a valid "not found" result).
- [is] indicates the possibility of errors (initialization, dangligness,
+ [is] indicates the possibility of errors (initialization, danglingness,
invalid access).
[Never_ok(is)] indicates that no valid solution exists (the function always
fails). [is] contains the error(s) that occur (it should never be
@@ -680,7 +680,7 @@ module Search_single_offset = struct
let process_search_in_byte range_start range_end bs acc =
match bs.BS.search_st with
| FS.Bottom ->
- (* this Invalid can only be due to initialization/dangligness;
+ (* this Invalid can only be due to initialization/danglingness;
check if min_fuel has been reached (for strnlen), to find out
which exception to raise *)
begin
@@ -905,7 +905,7 @@ module Search_single_offset = struct
end
in
fpf "search_and_acc (offset: %a), n_len: {%a}, last_byte_to_look: %a, \
- ajusted last_byte_to_look: %a" Int.pretty offset
+ adjusted last_byte_to_look: %a" Int.pretty offset
(Pretty_utils.pp_opt Ival.pretty) n_len Int.pretty last_byte_to_look
Int.pretty actual_last_byte;
let res = search bytecharmap offset n_len actual_last_byte in
diff --git a/src/plugins/value/domains/cvalue/locals_scoping.mli b/src/plugins/value/domains/cvalue/locals_scoping.mli
index 22f11d66f906069dcfc7c99777ef5af56dd2c754..1486df947281b9f6fcb1df928195e4a6253ba039 100644
--- a/src/plugins/value/domains/cvalue/locals_scoping.mli
+++ b/src/plugins/value/domains/cvalue/locals_scoping.mli
@@ -72,7 +72,7 @@ val offsetmap_top_addresses_of_locals:
topify_offsetmap_approx
(** [offsetmap_top_addresses_of_locals is_local] returns a function that
topifies all the parts of an offsetmap that contains a pointer verifying
- [is_local]. For efficicent reasons, this function is meant to be partially
+ [is_local]. For efficiency reasons, this function is meant to be partially
applied to its first argument. *)
val state_top_addresses_of_locals:
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index cb9a805ba4fb50fc105735234406d716cdbef22e..ddd017d40a099ba4fa7835ccad23069c1659a4b1 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -307,7 +307,7 @@ module G = struct
(* A MV contains, for interesting variables, the coefficient that is
associated to one lambda, represented as an integer interval.
- Missign coefficients are 0. *)
+ Missing coefficients are 0. *)
module MC = struct
include Hptmap.Make(Base)(Bounds)(Hptmap.Comp_unused)
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index 625ee1675bd5e4e85ba52fb3bed48488d0204046..d28f879b220ebde264a6a8e8fc25e589f1e86676 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -57,7 +57,7 @@ end
During pretty-printing, we skip them altogether.
(In fact, it should be possible to prove inductively that everything
is initialized except Top, because no computation introduces initialized
- bits, and nothing is initially unitialized. *)
+ bits, and nothing is initially uninitialized. *)
module V_Or_Uninitialized = struct
include Cvalue.V_Or_Uninitialized
@@ -161,7 +161,7 @@ module Internal : Domain_builder.InputDomain
let v = Eval.value_assigned value in
let v = match v with
| `Value v -> v
- (* Copy of fully indeterminate bits. We could store an unitialized
+ (* Copy of fully indeterminate bits. We could store an uninitialized
bottom, or something like that. Since this would be redundant
with the legacy domain, we just drop the value. *)
| `Bottom -> Top
diff --git a/src/plugins/value/engine/abstractions.mli b/src/plugins/value/engine/abstractions.mli
index 2c883ecf25a811c06dde69fd248b7dda579a23a5..2d4a018f82ee65fc831667faecc6ce607b0160e4 100644
--- a/src/plugins/value/engine/abstractions.mli
+++ b/src/plugins/value/engine/abstractions.mli
@@ -67,7 +67,7 @@ end
val make : config -> (module S)
-(** Two abstractions are instanciated at compile time: default and legacy
+(** Two abstractions are instantiated at compile time: default and legacy
(which may be the same). *)
module Legacy : S
diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml
index ea10b4c4b38c733e3ff7f9fa9ffba540da681beb..f1f9eba6aaa26d4f0e9193554494b02609266069 100644
--- a/src/plugins/value/engine/evaluation.ml
+++ b/src/plugins/value/engine/evaluation.ml
@@ -26,9 +26,9 @@ open Cil_types
open Eval
-(* The forward evaluation of an expression [e] gives a value to each subterms
+(* The forward evaluation of an expression [e] gives a value to each subterm
of [e], from its variables to the root expression [e]. It also computes the
- set of alarms which may occur in the evaluaton of each subterm.
+ set of alarms which may occur in the evaluation of each subterm.
All these intermediate results of an evaluation are stored in a cache, whose
type is described in eval.mli. The cache is the complete result of the
evaluation. *)
@@ -62,7 +62,7 @@ open Eval
statement, where the condition may be reduced to zero or non-zero. *)
(* An expression is deemed volatile if it contains an access to a volatile
- location. The forward evaluation computes this synctatically, by checking
+ location. The forward evaluation computes this syntactically, by checking
for volatile qualifiers on sub-lvalues and intermediate types. A 'volatile'
flag is propagated through the expression. This flag prevents the update of
the value computed by the initial forward evaluation. *)
@@ -699,7 +699,7 @@ module Make
- the new value (if any) is more precise than the old one.
Then the latter is reduced by the former, and the reduction kind is set
to [Backward].
- - or the old value has been reduced during the forward évaluation.
+ - or the old value has been reduced during the forward evaluation.
Then, [report.reduced] is [Forward], and must be set to [Neither] as
the reduction is propagated but the value of the current expression is
unchanged. *)
@@ -1258,7 +1258,7 @@ module Make
in
(* For pointer calls, we retro-propagate which function is being called
in the abstract state. This may be useful:
- - inside the call for langages with OO (think 'self')
+ - inside the call for languages with OO (think 'self')
- everywhere, because we may remove invalid values for the pointer
- after if enough slevel is available, as states obtained in
different functions are not merged by default. *)
diff --git a/src/plugins/value/engine/evaluation.mli b/src/plugins/value/engine/evaluation.mli
index bc12624dabc45153ccf2dcdc6fc4f9d227504a7e..0792bf86dda395449a5a5d1936a4c4c1d250e4a1 100644
--- a/src/plugins/value/engine/evaluation.mli
+++ b/src/plugins/value/engine/evaluation.mli
@@ -74,7 +74,7 @@ module type S = sig
?valuation:Valuation.t -> for_writing:bool ->
state -> lval -> (Valuation.t * loc * typ) evaluated
- (** [reduce ~valuation state expr positive] evaluates the expresssion [expr]
+ (** [reduce ~valuation state expr positive] evaluates the expression [expr]
in the state [state], and then reduces the [valuation] such that
the expression [expr] evaluates to a zero or a non-zero value, according
to [positive]. By default, the empty valuation is used. *)
diff --git a/src/plugins/value/engine/non_linear_evaluation.ml b/src/plugins/value/engine/non_linear_evaluation.ml
index 372898fac1babe1256224162a9d83a0f5a213e54..1df0c77a4272d4e5f04fa783470a71fe3fe08b2a 100644
--- a/src/plugins/value/engine/non_linear_evaluation.ml
+++ b/src/plugins/value/engine/non_linear_evaluation.ml
@@ -100,7 +100,7 @@ let same lval expr = match expr.enode with
(* Converts a map from lvalues to expressions and depth into an association
list from expressions to list of lvalues, sorted by decreasing depth of
expressions.
- The lvalues bound to themself are ignored. *)
+ The lvalues bound to themselves are ignored. *)
let reverse_map map =
let fill lval (expr, depth) acc =
if same lval expr then acc else DepthMap.add depth expr lval acc
@@ -265,7 +265,7 @@ module Make
smallest element of [list] according to [has_better_bound], [split] its
value in two smaller values, and [compute] the result for each.
The process is repeated [subdivnb] times, or until we detect no more
- improvment is possible. *)
+ improvement is possible. *)
let subdiv subdivnb list has_better_bound split compute =
Cmp.cmp_subdiv := has_better_bound;
let working_list = ref (Subdiv.of_list list) in
diff --git a/src/plugins/value/engine/partitioned_dataflow.ml b/src/plugins/value/engine/partitioned_dataflow.ml
index ac161c939bdcb9e3167bc1a91eb80c8165713e50..a9f152a3c15b8a4b691e6723db929ee07a2af531 100644
--- a/src/plugins/value/engine/partitioned_dataflow.ml
+++ b/src/plugins/value/engine/partitioned_dataflow.ml
@@ -284,7 +284,7 @@ module Make_Dataflow
let old_counter = current_info.counter_unroll in
(* Check whether there is enough slevel available. If not, merge all
states together. However, do not perform merge on return
- instructions. This needelessly degrades precision for
+ instructions. This needlessly degrades precision for
postconditions and option -split-return. *)
let r =
if old_counter > slevel stmt && not (is_return stmt)
@@ -366,7 +366,7 @@ module Make_Dataflow
Value_util.pretty_current_cfunction_name;
d
| Skip _ -> d
- | Code_annot (_,_) -> d (* processed direcly in doStmt from the
+ | Code_annot (_,_) -> d (* processed directly in doStmt from the
annotation table *)
end
in
diff --git a/src/plugins/value/engine/transfer_logic.ml b/src/plugins/value/engine/transfer_logic.ml
index 538278417b20c5cfc98322ca4a38725076e3edeb..84cd4abe002d0de845d754769f15990422800414 100644
--- a/src/plugins/value/engine/transfer_logic.ml
+++ b/src/plugins/value/engine/transfer_logic.ml
@@ -92,7 +92,7 @@ let emit_message_and_status kind kf behavior active property named_pred status =
emit_status property (conv_status status);
| Postcondition (PostLeaf | PostUseSpec as postk) ->
(* Only emit a status if the function has a body. Otherwise, we would
- overwite the "considered valid" status of the kernel. *)
+ overwrite the "considered valid" status of the kernel. *)
if postk = PostUseSpec then
emit_status property (conv_status status)
| Assumes ->
diff --git a/src/plugins/value/eval.ml b/src/plugins/value/eval.ml
index 79dbbb97839c94b9ceb59cf9d7e76d623ddce316..635dcd1d793ef70075accd40fc312fb2322c5072 100644
--- a/src/plugins/value/eval.ml
+++ b/src/plugins/value/eval.ml
@@ -136,7 +136,7 @@ end
let compute_englobing_subexpr ~subexpr ~expr =
let merge = Extlib.merge_opt (fun _ -> (@)) () in
(* Returns [Some] of the list of subexpressions of [expr] that contain
- [subexpr], apart from [expr] and [subexpr] themself, or [None] if [subexpr]
+ [subexpr], apart from [expr] and [subexpr] themselves, or [None] if [subexpr]
does not appear in [expr]. *)
let rec compute expr =
if Cil_datatype.ExpStructEq.equal expr subexpr
diff --git a/src/plugins/value/eval.mli b/src/plugins/value/eval.mli
index f01ea87e3565716ea6ce7536f034db13bc2115ee..7404b61fd3e69ab1d02d6dff17f2a86d8f2373df 100644
--- a/src/plugins/value/eval.mli
+++ b/src/plugins/value/eval.mli
@@ -116,7 +116,7 @@ type binop_context = {
- Unreduced: the value provided by the domain could not be reduced;
- Reduced: the value provided by the domain has been reduced;
- Created: the domain has returned `Top for the given expression;
- - Dull: the domain was not queried for the given expresssion.
+ - Dull: the domain was not queried for the given expression.
*)
(** State of reduction of an abstract value. *)
diff --git a/src/plugins/value/gui_files/register_gui.ml b/src/plugins/value/gui_files/register_gui.ml
index f45ff944dd7fb543eb37ab3f454aea778850b638..d63c58f8cc76e77ab5dcfb7ac4a71e4bb6ad323e 100644
--- a/src/plugins/value/gui_files/register_gui.ml
+++ b/src/plugins/value/gui_files/register_gui.ml
@@ -536,7 +536,7 @@ module Callstacks_manager = struct
) model.rows;
if not !has_visible_row && not (GCallstackMap.is_empty model.rows) then
(* Add a special row to indicate that some things are hidden by
- filters. This row is intentionnaly only added to the view, but
+ filters. This row is intentionally only added to the view, but
not to the model *)
w#insert_row (gtk_model#add (row_unfocused ()));
GtkTree.TreeView.columns_autosize w#view#as_tree_view;
@@ -1011,7 +1011,7 @@ let gui_compute_values (main_ui:main_ui) =
if not (Db.Value.is_computed ())
then main_ui#launcher ()
-let cleant_outputs kf s =
+let cleaned_outputs kf s =
let outs = Db.Outputs.kinstr (Kstmt s) in
let accept =
Callgraph.Uses.accept_base ~with_formals:true ~with_locals:true kf
@@ -1164,7 +1164,7 @@ let pretty_stmt_info (main_ui:main_ui) kf stmt =
| _ -> ()
else
(* Out for this statement *)
- let outs = cleant_outputs kf stmt in
+ let outs = cleaned_outputs kf stmt in
match outs with
| Some outs ->
main_ui#pretty_information
@@ -1174,7 +1174,7 @@ let pretty_stmt_info (main_ui:main_ui) kf stmt =
else main_ui#pretty_information "This code is dead@."
(* Actions to perform when the user has left-clicked, and Value is computed.
- Maintain sychronized with [can_eval_acsl_expr_selector] later in this file.*)
+ Maintain synchronized with [can_eval_acsl_expr_selector] later in this file.*)
let left_click_values_computed main_ui cm localizable =
try
let open Property in
@@ -1238,7 +1238,7 @@ let right_click_values_computed main_ui menu (cm: Callstacks_manager.t) localiza
begin
(match lv with
| Var _,NoOffset when isFunctionType ty ->
- () (* direcl calls are handled by [Design]. *)
+ () (* direct calls are handled by [Design]. *)
| Mem _, NoOffset when isFunctionType ty -> begin
(* Function pointers *)
(* get the list of functions in the values *)
diff --git a/src/plugins/value/legacy/eval_annots.ml b/src/plugins/value/legacy/eval_annots.ml
index dc58de3cafc87d8046bfc6c716904e4d6219d79f..ce9493c6a0d535eb4df942a7bd199652a9479130 100644
--- a/src/plugins/value/legacy/eval_annots.ml
+++ b/src/plugins/value/legacy/eval_annots.ml
@@ -25,7 +25,7 @@ open Eval_terms
(* Statuses for code annotations and function contracts *)
-(* Emits a status, possibly mutiple times. *)
+(* Emits a status, possibly multiple times. *)
let emit_status ppt status =
Property_status.emit ~distinct:true Value_util.emitter ~hyps:[] ppt status
@@ -191,7 +191,7 @@ let emit_message_and_status kf bhv behav_active ip pre_post pred_status pred nam
(if behav_active then (fun _ -> ()) else pp_behavior_inactive)
Value_util.pp_callstack;
(* Only emit a status if the function has a body. Otherwise, we would
- overwite the "considered valid" status of the kernel. *)
+ overwrite the "considered valid" status of the kernel. *)
if postk = PostUseSpec then
emit_status ip (conv_status pred_status);
| Assumes ->
@@ -684,7 +684,7 @@ let mark_unreachable () =
(* Do not put "unreachable" statuses on preconditions of
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
+ gives very bad results when reachable and unreachable calls
coexist (untried+dead -> unknown). *)
if Builtins.find_builtin_override kf = None
then begin
diff --git a/src/plugins/value/legacy/eval_op.mli b/src/plugins/value/legacy/eval_op.mli
index 8a0cbecdad782ed8ff323865337e4ba1d7231d4f..0573189845a5c8c1d8a33dfe55f265b5438fc6d8 100644
--- a/src/plugins/value/legacy/eval_op.mli
+++ b/src/plugins/value/legacy/eval_op.mli
@@ -108,7 +108,7 @@ val backward_comp_left_from_type:
val find:
with_alarms:CilE.warn_mode ->
?conflate_bottom:bool -> Model.t -> Locations.location -> V.t
-(** Tempory. Re-export of [Cvalue.Model.find] with a [~with_alarms] argument *)
+(** Temporary. Re-export of [Cvalue.Model.find] with a [~with_alarms] argument *)
val add_binding :
with_alarms:CilE.warn_mode ->
@@ -136,7 +136,7 @@ val copy_offsetmap :
with_alarms:CilE.warn_mode ->
Locations.Location_Bits.t -> Integer.t -> Model.t ->
V_Offsetmap.t Bottom.or_bottom
-(** Tempory. Re-export of [Cvalue.Model.copy_offsetmap] with a [with_alarms]
+(** Temporary. Re-export of [Cvalue.Model.copy_offsetmap] with a [with_alarms]
argument *)
val paste_offsetmap:
diff --git a/src/plugins/value/legacy/eval_slevel.ml b/src/plugins/value/legacy/eval_slevel.ml
index 455908a959be1a29a20a04f479de413a8020c3af..74f5def0c1e94ae4431f0d3392303447e77b1887 100644
--- a/src/plugins/value/legacy/eval_slevel.ml
+++ b/src/plugins/value/legacy/eval_slevel.ml
@@ -368,7 +368,7 @@ struct
let old_counter = current_info.counter_unroll in
(* Check whether there is enough slevel available. If not, merge all
states together. However, do not perform merge on return
- instructions. This needelessly degrades precision for
+ instructions. This needlessly degrades precision for
postconditions and option -split-return. *)
let r =
if old_counter > slevel s && not (is_return s)
@@ -493,7 +493,7 @@ struct
pretty_current_cfunction_name;
d
| Skip _ -> d
- | Code_annot (_,_) -> d (* processed direcly in doStmt from the
+ | Code_annot (_,_) -> d (* processed directly in doStmt from the
annotation table *)
end
in
diff --git a/src/plugins/value/legacy/eval_stmt.ml b/src/plugins/value/legacy/eval_stmt.ml
index e197c6022e3d3d13b8d66a6b0172a2e3407bbc5c..ea5f1e870830549c0441b58b066803f480cf7946 100644
--- a/src/plugins/value/legacy/eval_stmt.ml
+++ b/src/plugins/value/legacy/eval_stmt.ml
@@ -105,7 +105,7 @@ let compute_call_ref = ref (fun _ -> assert false)
in
if not (Eval_typ.offsetmap_matches_type typ_lv o) then
raise Do_assign_imprecise_copy;
- (* Warn for unitialized/escaping addresses. May return bottom
+ (* Warn for uninitialized/escaping addresses. May return bottom
when a part of the offsetmap contains no value. *)
if warn_indeterminate then
Warn.warn_reduce_indeterminate_offsetmap
@@ -152,7 +152,7 @@ let compute_call_ref = ref (fun _ -> assert false)
if Eval_typ.is_bitfield typ_lv
then default ()
else
- (* An lval assignement might be hidden by a dummy cast *)
+ (* An lval assignment might be hidden by a dummy cast *)
let exp_lv = find_lv state exp in
right_is_lval exp_lv
with Cannot_find_lv | Do_assign_imprecise_copy -> default ()
@@ -337,7 +337,7 @@ let compute_call_ref = ref (fun _ -> assert false)
in
(* For pointer calls, we retro-propagate which function is being called
in the abstract state. This may be useful:
- - inside the call for langages with OO (think 'self')
+ - inside the call for languages with OO (think 'self')
- everywhere, because we may remove invalid values for the pointer
- after if enough slevel is available, as states obtained in
different functions are not merged by default. *)
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 45a8b5cedfe1467ef4dd6cbce0947e1a44223d8c..64cb0561e3d02b2678cc0c81e210f5bdec1d8f91 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -143,7 +143,7 @@ let warn_reduce_mode () =
L:
x = 1;
\assert \at(x == 1, L);
- A naïve implementation of assertions involving C labels is likely to miss
+ A naive implementation of assertions involving C labels is likely to miss
the fact that the assertion is false after the else branch. A good
solution is to use a dummy edge that flows from L to the assertion,
to force its re-evaluation.
@@ -305,7 +305,7 @@ let rec infer_type = function
unsupported (Pretty_utils.to_string Cil_datatype.Logic_type.pretty t)
else Logic_const.plain_or_set infer_type t
-(* Best effort for compring the types currently understood by Value: ignore
+(* Best effort for comparing the types currently understood by Value: ignore
differences in integer and floating-point sizes, that are meaningless
in the logic *)
let same_etype t1 t2 =
@@ -1596,7 +1596,7 @@ let eval_predicate env pred =
| Cvalue.V_Or_Uninitialized.C_init_noesc v -> v, true
in
if Cvalue.V.is_bottom v && not ok then raise Stop;
- valid ~over:v ~under:V.bottom (*No precise under-approxition*);
+ valid ~over:v ~under:V.bottom (*No precise under-approximation*);
if not ok then raise DoNotReduce
| _ ->
let v = eval_term ~with_alarms env tsets in
diff --git a/src/plugins/value/legacy/mem_exec.ml b/src/plugins/value/legacy/mem_exec.ml
index 73480cad4b4e9a034cb03ae9e30092e1c9b9a1de..0fc8505a9cb7daf7a7e1c63db202bb404c2ed217 100644
--- a/src/plugins/value/legacy/mem_exec.ml
+++ b/src/plugins/value/legacy/mem_exec.ml
@@ -39,7 +39,7 @@ module ValueOutputs = Datatype.Pair
Datatype.Pair
(Datatype.Option(Cvalue.V_Offsetmap)) (* Return *)
(Cvalue.Model) (* Memory state *)))
- (Base.SetLattice) (* cloberred set for local variables *)
+ (Base.SetLattice) (* clobbered set for local variables *)
(* let pretty fmt (((bin, stin), (_, stout, _), _i) : PreviousState.t) =
Format.fprintf fmt
diff --git a/src/plugins/value/legacy/mem_exec.mli b/src/plugins/value/legacy/mem_exec.mli
index db21589465e0dcfd2d567e2a3a5f9ca0fba9f4f4..9d2637332c564114886e977d00e91876c30444be 100644
--- a/src/plugins/value/legacy/mem_exec.mli
+++ b/src/plugins/value/legacy/mem_exec.mli
@@ -30,7 +30,7 @@ val new_counter : unit -> int
(** Subtype of {!Value_types.call_res} *)
module ValueOutputs: Datatype.S with type t =
(Cvalue.V_Offsetmap.t option * Cvalue.Model.t) list (** states *) *
- Base.SetLattice.t (** cloberred set for local variables *)
+ Base.SetLattice.t (** clobbered set for local variables *)
(** [store_computed_call (kf, ki) init_state actuals outputs] memoizes the fact
diff --git a/src/plugins/value/legacy/valarms.mli b/src/plugins/value/legacy/valarms.mli
index 8593d35f19ed99434ecc8132f7a2207e9eb1bfb5..0689a7ad77ebdf773e12c3ef4f52e97afff2dbb1 100644
--- a/src/plugins/value/legacy/valarms.mli
+++ b/src/plugins/value/legacy/valarms.mli
@@ -46,7 +46,7 @@ val warn_div : warn_mode -> addresses:bool -> unit
not being comparable to \null. *)
val warn_shift : warn_mode -> int option -> unit
-(** Warn that the RHS of a shift operator must be positive, and optionnally
+(** Warn that the RHS of a shift operator must be positive, and optionally
less than the given size. *)
val warn_shift_left_positive : warn_mode -> unit
diff --git a/src/plugins/value/legacy/warn.mli b/src/plugins/value/legacy/warn.mli
index 79ad3f1217dfa563e600ac282e1c4a0607cc7b97..89d24e2e7791cb0e72de62b902a570a17a042f19 100644
--- a/src/plugins/value/legacy/warn.mli
+++ b/src/plugins/value/legacy/warn.mli
@@ -90,7 +90,7 @@ val maybe_warn_div: with_alarms:CilE.warn_mode -> Cvalue.V.t -> unit
val maybe_warn_indeterminate:
with_alarms:CilE.warn_mode -> Cvalue.V_Or_Uninitialized.t -> bool
-(** Warn for unitialized or escaping bits in the value passed
+(** Warn for uninitialized or escaping bits in the value passed
as argument. Returns [true] when an alarm has been raised *)
val maybe_warn_completely_indeterminate:
diff --git a/src/plugins/value/utils/value_perf.ml b/src/plugins/value/utils/value_perf.ml
index a0213cec72c75a1f922306da02e36194e7fd9b61..3e570d9f81a87219d9dda82f92caa4a6fa9d4be2 100644
--- a/src/plugins/value/utils/value_perf.ml
+++ b/src/plugins/value/utils/value_perf.ml
@@ -468,12 +468,12 @@ let reset () =
(* TODO: Output files with more graphical outputs, such as
- Gprof2dot-like output: (directoly output the dot)
+ Gprof2dot-like output: (directory output the dot)
http://code.google.com/p/jrfonseca/wiki/Gprof2Dot
The latter would be useful to see when imbricated loops multiply
the number of calls to leaf functions.
TODO: Also account for the memexec hit rate; and for the individual
- execution time of derivated plugins.
+ execution time of derived plugins.
*)
diff --git a/src/plugins/value/utils/value_util.mli b/src/plugins/value/utils/value_util.mli
index 1ec1cb7a19264328345392d41ebcee382a5df59b..e1d3bc04778e00287cefc7a1cb66632720ab1b30 100644
--- a/src/plugins/value/utils/value_util.mli
+++ b/src/plugins/value/utils/value_util.mli
@@ -109,13 +109,13 @@ val compatible_functions:
with_alarms:CilE.warn_mode -> varinfo -> typ -> typ -> bool
val zero: exp -> exp
-(** Retun a zero constant compatible with the type of the argument *)
+(** Return a zero constant compatible with the type of the argument *)
val is_value_zero: exp -> bool
(** Return [true] iff the argument has been created by {!zero} *)
val dump_garbled_mix: unit -> unit
-(** print information on the garblex mix created during evaluation *)
+(** print information on the garbled mix created during evaluation *)
(** Dependences of expressions and lvalues. *)
diff --git a/src/plugins/value/utils/widen.ml b/src/plugins/value/utils/widen.ml
index 950859d1eaf12ad8b06f2f953b0aedb1483cb9f4..71e2360ac5a26c0e6aa50913751e2d64e290c19a 100644
--- a/src/plugins/value/utils/widen.ml
+++ b/src/plugins/value/utils/widen.ml
@@ -87,7 +87,7 @@ class pragma_widen_visitor init_widen_hints init_enclosing_loops = object(self)
match s.skind with
| Loop (_, bl, _, _, _) -> begin
(* ZZZ: this code does not handle loops that are created using gotos. We
- could improve this by finding the relevants statements using a
+ could improve this by finding the relevant statements using a
traversal of the CFG. *)
let annot = Annotations.code_annot s in
let pragmas = Logic_utils.extract_loop_pragma annot in
@@ -187,7 +187,7 @@ class pragma_widen_visitor init_widen_hints init_enclosing_loops = object(self)
let thresholds = Ival.Widen_Hints.of_list [bound1; bound2] in
self#add_thresholds ~base:(Base.of_varinfo vidx) thresholds
in
- (* Find insided [idx] a variable on which we will add hints. [shift] is an
+ (* Find inside [idx] a variable on which we will add hints. [shift] is an
integer that indicates that we access to [idx+shift], instead of to
[idx] directly *)
let rec aux_idx idx shift =
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 149da154881ba01095ad446990d73db9e7b1e8d8..bf0031759ed7734cca4448dc74102ec99471e420 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -657,7 +657,7 @@ module SplitReturn =
module SplitGlobalStrategy = State_builder.Ref (Split_strategy)
(struct
let default () = Split_strategy.NoSplit
- let name = "Value_parameters.SplitGlobalStategy"
+ let name = "Value_parameters.SplitGlobalStrategy"
let dependencies = [SplitReturn.self]
end)
let () =
diff --git a/src/plugins/value/values/abstract_location.mli b/src/plugins/value/values/abstract_location.mli
index 8aefc4fd98cfa83834e05c1b5af7e1b437b5281a..53bf993a47da8681418fcd8dc6188fbf041041c4 100644
--- a/src/plugins/value/values/abstract_location.mli
+++ b/src/plugins/value/values/abstract_location.mli
@@ -65,7 +65,7 @@ module type S = sig
val forward_index : typ -> value -> offset -> offset
(** [reduce_index_by_array_size ~size_expr ~index_expr size index] reduces
- the value [index] to fit into the inverval [0..(size-1)]. It also returns
+ the value [index] to fit into the interval [0..(size-1)]. It also returns
out-of-bound alarms if it was not already the case. [size_expr] and
[index_expr] are the Cil expressions of the array size and the index,
needed to create the alarms. *)
@@ -88,7 +88,7 @@ module type S = sig
(** [reduce_loc_by_validity for_writing bitfield lval loc] reduce the location
[loc] by its valid part for a read or write operation, according to the
- [for_writing] boolean. It also returns the alarms enusuring this validity.
+ [for_writing] boolean. It also returns the alarms ensuring this validity.
[bitfield] indicates whether the location may be the one of a bitfield;
if it does not hold, the location is assumed to be byte aligned.
[lval] is only used to create the alarms. *)
@@ -97,7 +97,7 @@ module type S = sig
(** {3 Backward Operations } *)
- (** For an unary forward operation F, the inverse backward opereror B tries to
+ (** For an unary forward operation F, the inverse backward operator B tries to
reduce the argument values of the operation, given its result.
It must satisfy:
diff --git a/src/plugins/value/values/abstract_value.mli b/src/plugins/value/values/abstract_value.mli
index 4eeae11615e7c06979c54a251da5a611f398373f..04658f22df67fb3b6d1decb54455fa51b70fc35d 100644
--- a/src/plugins/value/values/abstract_value.mli
+++ b/src/plugins/value/values/abstract_value.mli
@@ -48,7 +48,7 @@ module type S = sig
(** {3 Forward Operations } *)
- (** Returns the abstract value of a litteral constants, and potentially some
+ (** Returns the abstract value of a literal constant, and potentially some
alarms in case of floating point constants overflow. *)
val constant : exp -> constant -> t evaluated
@@ -66,7 +66,7 @@ module type S = sig
(** {3 Backward Operations } *)
- (** For an unary forward operation F, the inverse backward opereror B tries to
+ (** For an unary forward operation F, the inverse backward operator B tries to
reduce the argument values of the operation, given its result.
It must satisfy:
diff --git a/src/plugins/value_types/cvalue.mli b/src/plugins/value_types/cvalue.mli
index ca1f6948c8c0195a959946d689175f8bdfd8668f..b60fff409214556b5ad692c8f7e094ec655febc3 100644
--- a/src/plugins/value_types/cvalue.mli
+++ b/src/plugins/value_types/cvalue.mli
@@ -225,7 +225,7 @@ module V_Or_Uninitialized : sig
[!\dangling(r)] otherwise. *)
val remove_indeterminateness: t -> t
- (** Remove 'unitialized' and 'escaping addresses' flags from the argument *)
+ (** Remove 'uninitialized' and 'escaping addresses' flags from the argument *)
val unspecify_escaping_locals :
exact:bool -> (V.M.key -> bool) -> t -> Base.SetLattice.t * t
diff --git a/src/plugins/value_types/function_Froms.ml b/src/plugins/value_types/function_Froms.ml
index 8631bac1a91e4da5f281ee1487f46153fcfbd9c6..206f13db72dada0ba5f90c71ff39453206f7a796 100644
--- a/src/plugins/value_types/function_Froms.ml
+++ b/src/plugins/value_types/function_Froms.ml
@@ -429,7 +429,7 @@ module Memory = struct
let substitute_data_deps =
(* Nothing left to substitute, return z unchanged *)
let empty_right z = Deps.from_data_deps z in
- (* Zone to subtitute is empty *)
+ (* Zone to substitute is empty *)
let empty_left _ = Deps.bottom in
(* [b] is in the zone and substituted. Rewrite appropriately *)
let both b itvs offsm =
@@ -457,7 +457,7 @@ module Memory = struct
let substitute_indirect_deps =
(* Nothing left to substitute, z is directly an indirect dependency *)
let empty_right z = z in
- (* Zone to subtitute is empty *)
+ (* Zone to substitute is empty *)
let empty_left _ = Zone.bottom in
let both b itvs offsm =
(* Both the found data and indirect dependencies are computed for indirect
diff --git a/src/plugins/value_types/function_Froms.mli b/src/plugins/value_types/function_Froms.mli
index 977c1d8bd81a5f2120abb7a43e119c1cf069e1ad..e5f21cbff98c1474ba4c35eb62e19fa7f9a943bf 100644
--- a/src/plugins/value_types/function_Froms.mli
+++ b/src/plugins/value_types/function_Froms.mli
@@ -128,10 +128,10 @@ module Memory : sig
(** Default value to use for storing the dependencies of [\result] *)
val default_return: return
- (** Completly imprecise return *)
+ (** Completely imprecise return *)
val top_return: return
- (** Completly imprecise return of the given size *)
+ (** Completely imprecise return of the given size *)
val top_return_size: Int_Base.t -> return
(** Add some dependencies to [\result], between bits [start] and
diff --git a/src/plugins/variadic/classify.ml b/src/plugins/variadic/classify.ml
index e0aeb72157713e2bcd1613cc19956359e9aeeb8c..d6430a3fbe8cd078a323e32bfe4245472a27b76c 100644
--- a/src/plugins/variadic/classify.ml
+++ b/src/plugins/variadic/classify.ml
@@ -84,7 +84,7 @@ let mk_aggregator env fun_name a_pos pname a_type =
let mk_format_fun ~buffer ?(additional=[]) ~format f_kind =
FormatFun { f_kind; f_buffer = buffer ; f_format_pos = format ;
- f_additionnal_args = additional; }
+ f_additional_args = additional; }
(* ************************************************************************ *)
diff --git a/src/plugins/variadic/generic.ml b/src/plugins/variadic/generic.ml
index 756eb763dec9cec9d071110663e68af96a4a681b..da7c593b6d4f726408e594f30ef1cddf9fdf4e8e 100644
--- a/src/plugins/variadic/generic.ml
+++ b/src/plugins/variadic/generic.ml
@@ -165,7 +165,7 @@ let translate_call ~fundec stmt =
(* Assign parameters to these *)
block.bstmts <- List.map2 (Build.vi_assign ~loc) vis v_exps;
- (* Build an array with to store adresses *)
+ (* Build an array with to store addresses *)
let addrs = List.map Cil.mkAddrOfVi vis in
let vargs, assigns = Build.array_init ~loc fundec block
"__va_args" Cil.voidPtrType addrs
diff --git a/src/plugins/variadic/standard.ml b/src/plugins/variadic/standard.ml
index 067c06ecccef775419319247ec0de487cc0cca68..3ee0122c70c17b8a72221e50123ff8748db9be53 100644
--- a/src/plugins/variadic/standard.ml
+++ b/src/plugins/variadic/standard.ml
@@ -379,10 +379,10 @@ let build_fun_spec env loc vf format_fun tvparams formals =
let l = List.combine vformals dirs in
List.iter (add_var ~indirect:false) l;
- (* Add format source and additionnal parameters *)
+ (* Add format source and additional parameters *)
add_var ~indirect:true (List.nth sformals format_fun.f_format_pos, `ArgInArray);
List.iter (fun p -> add_var ~indirect:true (List.nth sformals p, `ArgIn))
- format_fun.f_additionnal_args;
+ format_fun.f_additional_args;
(* Add buffer source/dest *)
begin match format_fun.f_buffer, format_fun.f_kind with
diff --git a/src/plugins/variadic/tests/known/exec.c b/src/plugins/variadic/tests/known/exec.c
index 4011b122852cb26642885897ffc67b48234fb832..b8f3733090ff429fe8af50c8b3002f0fe3c743dd 100644
--- a/src/plugins/variadic/tests/known/exec.c
+++ b/src/plugins/variadic/tests/known/exec.c
@@ -11,7 +11,7 @@ int main()
execl("ls", "ls", "-l", "--color", NULL, 42);
execlp("ls", "ls", "-all", NULL, NULL);
execle("ls", "ls", NULL, env, 42, NULL);
- // Null present but not syntaxically
+ // Null present but not syntactically
execlp("ls", "ls", "--reverse", sentinel);
}
diff --git a/src/plugins/variadic/tests/known/open_wrong.c b/src/plugins/variadic/tests/known/open_wrong.c
index 0fdce9fb33a64749abedcf7a5d921c6fbe83096f..3a693eaf5e0160644d29398b61ebefe0b2976911 100644
--- a/src/plugins/variadic/tests/known/open_wrong.c
+++ b/src/plugins/variadic/tests/known/open_wrong.c
@@ -1,5 +1,5 @@
/* A note on this test.
- The mecanism chosing the version of open to use will conclude that, since
+ The mechanism choosing the version of open to use will conclude that, since
a string is not a possible argument, the function call has probably too
many parameters. The problem and the warning message issued by the
plug-in is not very intuitive.
diff --git a/src/plugins/variadic/translate.ml b/src/plugins/variadic/translate.ml
index 2babde48823f9f0ceb63c1856639e8588e8b617a..1bc898c25c0a9980c904b03fde6efc6cab300db1 100644
--- a/src/plugins/variadic/translate.ml
+++ b/src/plugins/variadic/translate.ml
@@ -25,7 +25,7 @@ open Va_types
open Extlib
module Typ = Extends.Typ
-(* List of builting function names to translate *)
+(* List of builtin function names to translate *)
let va_builtins = [
"__builtin_va_start";
diff --git a/src/plugins/variadic/va_types.mli b/src/plugins/variadic/va_types.mli
index 12104c4bdef83b4b4748143c7aea21dcfd15a0ec..d34cf6355924d706089cbe7f327c35b7fc714d45 100644
--- a/src/plugins/variadic/va_types.mli
+++ b/src/plugins/variadic/va_types.mli
@@ -55,7 +55,7 @@ and aggregator_type = EndedByNull
and format_fun = {
f_kind : Format_types.format_kind;
f_buffer : buffer;
- f_additionnal_args : int list;
+ f_additional_args : int list;
f_format_pos : int;
}
diff --git a/src/plugins/wp/Cfloat.ml b/src/plugins/wp/Cfloat.ml
index a6e524c185a116873712869fd960569759d50f4c..fec83a32018fdff193264aa579d4d0ba8e9100a0 100644
--- a/src/plugins/wp/Cfloat.ml
+++ b/src/plugins/wp/Cfloat.ml
@@ -91,7 +91,7 @@ type model = Real | Float
let model = Context.create ~default:Real "Cfloat.model"
(* -------------------------------------------------------------------------- *)
-(* --- Litterals --- *)
+(* --- Literals --- *)
(* -------------------------------------------------------------------------- *)
let code_lit f =
diff --git a/src/plugins/wp/Cfloat.mli b/src/plugins/wp/Cfloat.mli
index 92e9eae86235c798187d896138c2147b349938f0..fa12c25015d288b322fd0c762788ab199d84b57d 100644
--- a/src/plugins/wp/Cfloat.mli
+++ b/src/plugins/wp/Cfloat.mli
@@ -21,7 +21,7 @@
(**************************************************************************)
(* -------------------------------------------------------------------------- *)
-(** Floatting Arithmetic Model *)
+(** Floating Arithmetic Model *)
(* -------------------------------------------------------------------------- *)
open Ctypes
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 22dee44ab674dab1751380e2410d2e36d7fd6285..2d4c02df7fde586797b313e3eba3de72822cb50d 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -69,7 +69,7 @@ let ac = {
associative = true ;
commutative = true ;
idempotent = false ;
- inversible = false ;
+ invertible = false ;
neutral = E_none ;
absorbant = E_none ;
}
@@ -84,7 +84,7 @@ let result = Logic.Int
let library = "cbits"
let balance = Lang.Left
-let op_lxor = { ac with neutral = E_int 0 ; inversible = true }
+let op_lxor = { ac with neutral = E_int 0 ; invertible = true }
let op_lor = { ac with neutral = E_int 0 ; absorbant = E_int (-1); idempotent = true }
let op_land = { ac with neutral = E_int (-1); absorbant = E_int 0 ; idempotent = true }
@@ -754,7 +754,7 @@ let is_cint_simplifier = object (self)
Format.fprintf fmt "%a: %a,@ " Lang.F.pp_term k Ival.pretty v)
domain
- method name = "Remove redondant is_cint"
+ method name = "Remove redundant is_cint"
method copy = {< domain = domain >}
method private narrow_dom t v =
diff --git a/src/plugins/wp/Cint.mli b/src/plugins/wp/Cint.mli
index d8990e91fe8e8a30aebcfaf6af52a9863708f608..90a50a2466fd891dd6091717eb6c533efe9a4e5c 100644
--- a/src/plugins/wp/Cint.mli
+++ b/src/plugins/wp/Cint.mli
@@ -29,7 +29,7 @@ open Lang
open Lang.F
val of_real : c_int -> unop
-val convert : c_int -> unop (** Indenpendent from model *)
+val convert : c_int -> unop (** Independent from model *)
val to_cint : lfun -> c_int (** Raises [Not_found] if not. *)
val is_cint : lfun -> c_int (** Raises [Not_found] if not. *)
@@ -74,6 +74,6 @@ val f_bit : lfun
val is_cint_simplifier: Conditions.simplifier
(** Remove the [is_cint] in formulas that are
- redondant with other conditions. *)
+ redundant with other conditions. *)
val is_positive_or_null: term -> bool
diff --git a/src/plugins/wp/Cleaning.ml b/src/plugins/wp/Cleaning.ml
index 4a085639a73aa3a78af643e47e86beee8a8b9f1c..2627fa4a0d0454a6123c4c4cc9e9bb2547699c0c 100644
--- a/src/plugins/wp/Cleaning.ml
+++ b/src/plugins/wp/Cleaning.ml
@@ -29,7 +29,7 @@ open Lang
open Lang.F
(* -------------------------------------------------------------------------- *)
-(* --- Latice --- *)
+(* --- Lattice --- *)
(* -------------------------------------------------------------------------- *)
type 'a occur =
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index 3d4aafcb3df0439b3c2b47611698d498405f2ec3..f10250adbf60c048b0f2c9d945244a631d83808a 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -578,7 +578,7 @@ let rec flatten_sequence m = function
flat_cons step (flatten_sequence m seq)
(* -------------------------------------------------------------------------- *)
-(* --- Maping --- *)
+(* --- Mapping --- *)
(* -------------------------------------------------------------------------- *)
let lift f e = F.e_prop (f (F.p_bool e))
diff --git a/src/plugins/wp/Conditions.mli b/src/plugins/wp/Conditions.mli
index 6fd30db228cfacad398e2902d54b074214dc3b2a..b6193f2e7cb92c7d058ed85f49d39a563a150340 100644
--- a/src/plugins/wp/Conditions.mli
+++ b/src/plugins/wp/Conditions.mli
@@ -146,7 +146,7 @@ val at_closure : (sequent -> sequent ) -> unit (** register a transformation app
(** {2 Bundles}
Bundles are {i mergeable} pre-sequences.
- This the key structure for merging hypotheses with linerar complexity
+ This the key structure for merging hypotheses with linear complexity
during backward weakest pre-condition calculus.
*)
@@ -187,7 +187,7 @@ class type simplifier =
method fixpoint : unit
(** Called after assuming hypothesis and knowing the goal *)
method infer : F.pred list
- (** Add new hypotheses implyed by the original hypothesis. *)
+ (** Add new hypotheses implied by the original hypothesis. *)
method simplify_exp : F.term -> F.term
(** Currently simplify an expression. *)
diff --git a/src/plugins/wp/Cstring.ml b/src/plugins/wp/Cstring.ml
index 73b9136aaeb58267c37b3c7148b4c6186002bb1f..d743317918f1db6275deb9d15550ad322c12a00f 100644
--- a/src/plugins/wp/Cstring.ml
+++ b/src/plugins/wp/Cstring.ml
@@ -51,7 +51,7 @@ module LIT = Model.Generator(STR)
(struct
type key = cst
type data = int * F.term
- let name = "Cstring.Litterals"
+ let name = "Cstring.Literals"
let hid = Hashtbl.create 31
diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index fbb07d32de70171509163b468c37c21743044f8b..4bbf0549d45ff798b7ed0d3266a7602ecc530267 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -85,7 +85,7 @@ sig
val prefix : string
val natural : bool
(* natural: all types are constrained, but only with their natural values *)
- (* otherwize: only atomic types are constrained *)
+ (* otherwise: only atomic types are constrained *)
val is_int : c_int -> term -> pred
val is_float : c_float -> term -> pred
val is_pointer : term -> pred
@@ -323,7 +323,7 @@ let plain lt e =
Vexp e
(* -------------------------------------------------------------------------- *)
-(* --- Int-As-Boolans --- *)
+(* --- Int-As-Booleans --- *)
(* -------------------------------------------------------------------------- *)
let bool_eq a b = e_if (e_eq a b) e_one e_zero
diff --git a/src/plugins/wp/Cvalues.mli b/src/plugins/wp/Cvalues.mli
index 4cd9a752f6364706b8c5408f1b7213356c791ac2..8bc3b1e01304085857af6a166a6e9aba1e25e79c 100644
--- a/src/plugins/wp/Cvalues.mli
+++ b/src/plugins/wp/Cvalues.mli
@@ -29,7 +29,7 @@ open Ctypes
open Memory
open Lang.F
-(** {2 Int-As-Boolans} *)
+(** {2 Int-As-Booleans} *)
val bool_val : unop
val bool_eq : binop
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 4d802a2e21fe9e61972e80f5600b73b28cd32d76..99fc52196dba1f0ab11a85c005516008f2561517 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -335,7 +335,7 @@ struct
p_equal (val_of_term env a) (val_of_term env b)
| EQ_incomparable ->
- (* incomparrable terms *)
+ (* incomparable terms *)
Wp_parameters.warning ~current:true
"@[Incomparable terms (comparison is False):@ type %a with@ type %a@]"
Printer.pp_logic_type a.term_type
diff --git a/src/plugins/wp/LogicUsage.ml b/src/plugins/wp/LogicUsage.ml
index 947a12779b3eb340964bd4147c8c2b1c350ff58c..23965d520aff5720c26503abbbb56d7d972d9d05 100644
--- a/src/plugins/wp/LogicUsage.ml
+++ b/src/plugins/wp/LogicUsage.ml
@@ -156,7 +156,7 @@ let compute_logicname l =
let base = l.l_var_info.lv_name in
let over =
try SMap.find base d.clash
- with Not_found -> LSet.empty (*TODO: Undected usage -> overloading issue *)
+ with Not_found -> LSet.empty (*TODO: Undetected usage -> overloading issue *)
in
match LSet.elements over with
| [] | [_] -> d.names <- LMap.add l base d.names ; base
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 22c2d889f6fa8a33bf46214cf7b144d72cee0579..8c67f9ecb9a06ed5c7d280028b852d00cadc8718 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -489,7 +489,7 @@ struct
let compare = compare_ptr_conflated
end
-(* This is a model-indepent generator,
+(* This is a model-independent generator,
which will be inherited from the model-dependent clusters *)
module ShiftGen = Model.StaticGenerator(Cobj)
(struct
@@ -1016,7 +1016,7 @@ struct
if c.cstruct
then List.fold_left flayout w c.cfields
else
- (* TODO: can be the longuest common prefix *)
+ (* TODO: can be the longest common prefix *)
add_block Garbled w
| C_array { arr_flat = Some a } ->
let ly = rlayout [] (Ctypes.object_of a.arr_cell) in
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 91f427c418acf7acf8281aabdc5820416c090553..d7c500f9e8829dc74c997407aa9b599de9d244ec 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -698,7 +698,7 @@ struct
"Validity of unsized-array not implemented yet"
(* Append conditions to [cond] for [range=(elt,a,b)],
- consiting of [a..b] elements with type [elt] to fits inside the block,
+ consisting of [a..b] elements with type [elt] to fits inside the block,
provided [a<=b]. *)
let rec fits cond (block,size) ((elt,a,b) as range) =
if Ctypes.equal block elt then
@@ -724,7 +724,7 @@ struct
| _ -> offset_fits (fits cond (obj,1) (te,k,k)) te ofs
(* Append conditions to [cond] for [range=(elt,a,b)], starting at [offset],
- consiting of [a..b] elements with type [elt] to fits inside the block,
+ consisting of [a..b] elements with type [elt] to fits inside the block,
provided [a<=b]. *)
let rec range_fits cond alloc offset ((elt,a,b) as range) =
match offset with
@@ -862,7 +862,7 @@ struct
let global sigma p = M.global sigma.mem p
(* -------------------------------------------------------------------------- *)
- (* --- Havoc allong a ranged-path --- *)
+ (* --- Havoc along a ranged-path --- *)
(* -------------------------------------------------------------------------- *)
let rec assigned_path
@@ -902,7 +902,7 @@ struct
assigned_path hs xs (y::ys) ak bk ofs
else
(* index [e] is not covered by [xs]:
- any indice different from e is disjoint.
+ any index different from e is disjoint.
explore also deeply with index [e]. *)
let ae = e_get a e in
let be = e_get b e in
diff --git a/src/plugins/wp/Memory.ml b/src/plugins/wp/Memory.ml
index 0975c8d7ac3341890f03aa19b1b300e5b024235a..2c999da380727d4e7b4f326dfe30195081549826 100644
--- a/src/plugins/wp/Memory.ml
+++ b/src/plugins/wp/Memory.ml
@@ -60,7 +60,7 @@ type 'a logic =
(** Memory Variables
- The memory is partitionned into chunk, set of memory location.
+ The memory is partitioned into chunks, sets of memory locations.
*)
module type Chunk =
@@ -159,7 +159,7 @@ sig
(** Try to interpret a term as an in-memory operation
located at this program point. Only best-effort
- shall be performed, otherwize return [Mvalue].
+ shall be performed, otherwise return [Mvalue].
Recognized [Cil] patterns:
- [Mvar x,[Mindex 0]] is rendered as [*x] when [x] has a pointer type
@@ -171,7 +171,7 @@ sig
The result shall be exhaustive with respect to values that are printed as [Memory.mval]
values at [post] label {i via} the [lookup] function.
- Otherwize, those values would not be pretty-printed to the user. *)
+ Otherwise, those values would not be pretty-printed to the user. *)
val updates : state sequence -> Vars.t -> update Bag.t
(** Propagate a sequent substitution inside the memory state. *)
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index 9f8889bd5eafb67765874ac398d2051d1c686ed9..ec296b2176ce3d9c21c618ba895935850b259149 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -293,7 +293,7 @@ type local_ctx = {
mutable tlet : model LVmap.t; (* for \\let var bound to a term *)
mutable plet : value LVmap.t; (* for \\let var bound to a predicate *)
mutable spec : value; (* for formals and globals of of spec,
- before partionning the result *)
+ before partitioning the result *)
}
let mk_local_ctx () = { tlet=LVmap.empty ; plet=LVmap.empty ; spec=E.bot }
@@ -640,7 +640,7 @@ let cfun_spec env kf =
end in
let spec = Annotations.funspec kf in
ignore (Cil.visitCilFunspec (visitor:>Cil.cilVisitor) spec) ;
- (* Partionning the accesses of the spec for formals vs globals *)
+ (* Partitioning the accesses of the spec for formals vs globals *)
let formals,globals = E.partition_formals_vs_others env.local.spec in
env.global.spec_formals <- formals ;
env.global.spec_globals <- globals
diff --git a/src/plugins/wp/Region.ml b/src/plugins/wp/Region.ml
index e97a6b12c4164715d70b73d81b91df4d9a55b9f4..00f10b12febad17d39ef985a99e747131fb98b24 100644
--- a/src/plugins/wp/Region.ml
+++ b/src/plugins/wp/Region.ml
@@ -114,7 +114,7 @@ and merge_fields fxs gys =
(f,merge x y) :: merge_fields fxstail gystail
(* -------------------------------------------------------------------------- *)
-(* --- Disjonction --- *)
+(* --- Disjunction --- *)
(* -------------------------------------------------------------------------- *)
let rec disjoint a b =
diff --git a/src/plugins/wp/Repr.mli b/src/plugins/wp/Repr.mli
index d81efb4581ccca86dafbb7cc7226971cd32b7147..c6f1672d7474967fc60ae43eae86c3533f6002c3 100644
--- a/src/plugins/wp/Repr.mli
+++ b/src/plugins/wp/Repr.mli
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-(** {2 Term & Predicate Instrospection} *)
+(** {2 Term & Predicate Introspection} *)
(** Environment for binder resolution, see Forall & Exists *)
type env
diff --git a/src/plugins/wp/Vlist.ml b/src/plugins/wp/Vlist.ml
index 6af27adb74e69990f0364b526f5d3b0b174af876..6dbd47dda1eaff0da68cf16ac1cf40c32118532a 100644
--- a/src/plugins/wp/Vlist.ml
+++ b/src/plugins/wp/Vlist.ml
@@ -53,12 +53,12 @@ let l_repeat = Lang.(E.({
(*--- Qed Symbols ---*)
-let f_cons = Lang.extern_f ~library "cons" (* rewriten in concat(elt) *)
+let f_cons = Lang.extern_f ~library "cons" (* rewritten in concat(elt) *)
let f_nil = Lang.extern_f ~library ~category:L.Constructor "nil"
let f_elt = Lang.extern_f ~library ~category:L.Constructor ~link:l_elt "elt"
let concatenation = L.(Operator {
- inversible = true ;
+ invertible = true ;
associative = true ;
commutative = false ;
idempotent = false ;
diff --git a/src/plugins/wp/Vset.ml b/src/plugins/wp/Vset.ml
index 49421fb439dff5dec70230dae066954e35ff3eee..15310e42407bc90d3f44e32ee3f36b9363692fb1 100644
--- a/src/plugins/wp/Vset.ml
+++ b/src/plugins/wp/Vset.ml
@@ -290,7 +290,7 @@ let disjoint xs ys =
in p_conj ws
(* -------------------------------------------------------------------------- *)
-(* --- Lifting & Maping --- *)
+(* --- Lifting & Mapping --- *)
(* -------------------------------------------------------------------------- *)
let cartesian f xs ys =
diff --git a/src/plugins/wp/Vset.mli b/src/plugins/wp/Vset.mli
index 654abefe17cebec45a89d8554efce42fa9ec179b..a92606a7d08de1387a0c3db841e7ffa4dd28bdf8 100644
--- a/src/plugins/wp/Vset.mli
+++ b/src/plugins/wp/Vset.mli
@@ -66,8 +66,8 @@ val pp_bound : Format.formatter -> term option -> unit
val pp_vset : Format.formatter -> vset -> unit
val pretty : Format.formatter -> set -> unit
-(** {3 Maping}
- These operations computes different kinds of [{f x y with x in A, y in B}].
+(** {3 Mapping}
+ These operations compute different kinds of [{f x y with x in A, y in B}].
*)
val map : (term -> term) -> set -> set
diff --git a/src/plugins/wp/WpTac.ml b/src/plugins/wp/WpTac.ml
index ab80c7dd6e983aa761947ab1eabea368558b108e..c4bdd2154f07ec817088562687d3005ba32fc230 100644
--- a/src/plugins/wp/WpTac.ml
+++ b/src/plugins/wp/WpTac.ml
@@ -57,14 +57,14 @@ let is_disj0_literal_repr = function
| _ as repr -> is_cnf_dnf_literal_repr repr
let is_disj0_literal e = is_disj0_literal_repr (repr e)
-(* is it already into a Conjunctive Nomal Form *)
+(* is it already into a Conjunctive Normal Form *)
let is_cnf_repr =
function
| And xs -> List.for_all is_disj0_literal xs
| _ as repr -> is_disj0_literal_repr repr
let is_cnf e = is_cnf_repr (repr e)
-(* is it already into a Disjunctive Nomal Form *)
+(* is it already into a Disjunctive Normal Form *)
let is_dnf_repr = function
| Or xs -> List.for_all is_conj0_literal xs
| _ as repr -> is_conj0_literal_repr repr
@@ -369,7 +369,7 @@ let e_dnf = cnf_dnf ~pol:false
(** Register new available transformation at Conditions.closure **)
-(* feature at Conditions.closure and also for debuging purpose *)
+(* feature at Conditions.closure and also for debugging purposes *)
let () = Conditions.at_closure (fun ((step,goal) as sequent) ->
match Wp_parameters.SplitDepth.get () with
| 0 -> sequent
diff --git a/src/plugins/wp/calculus.ml b/src/plugins/wp/calculus.ml
index 772bc8febfeef1b564b2938c4c97d6a338fb98de..f359000e1da0c1c62678a7e1569f5fd4408661cd 100644
--- a/src/plugins/wp/calculus.ml
+++ b/src/plugins/wp/calculus.ml
@@ -284,7 +284,7 @@ module Cfg (W : Mcfg.S) = struct
obj
- (** We have found some assigns hypothesis in the stategy :
+ (** We have found some assigns hypothesis in the strategy :
* it means that we skip the corresponding bloc, ie. we directly compute
* the result before the block : (forall assigns. P),
* and continue with empty. *)
diff --git a/src/plugins/wp/cfgDump.ml b/src/plugins/wp/cfgDump.ml
index 811c2e2aab3fbbb8adf7841fbb4671a6c6d8fa27..1024210e08b0abd276540c9b49d15a4afeec07dc 100644
--- a/src/plugins/wp/cfgDump.ml
+++ b/src/plugins/wp/cfgDump.ml
@@ -218,7 +218,7 @@ end
module WP = Calculus.Cfg(VC)
(* ------------------------------------------------------------------------ *)
-(* --- Proof Obilgation Generation --- *)
+(* --- Proof Obligation Generation --- *)
(* ------------------------------------------------------------------------ *)
class computer () =
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 314ae5011dc55d7ea695c17ada32a998834b53d1..aed57385ef1b06b34e804777ce25bc12f1d9c95e 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -1489,7 +1489,7 @@ struct
end
-(* Cache because computer functors can not be instanciated twice *)
+(* Cache because computer functors can not be instantiated twice *)
module COMPUTERS = Model.S.Hashtbl
let computers = COMPUTERS.create 1
diff --git a/src/plugins/wp/cil2cfg.ml b/src/plugins/wp/cil2cfg.ml
index bb275d0f58e7db00756b887bbce63d1d0ae79d1e..ae0025dcf59a544561d22ae3ab51de9e3a752c58 100644
--- a/src/plugins/wp/cil2cfg.ml
+++ b/src/plugins/wp/cil2cfg.ml
@@ -772,7 +772,7 @@ let get_call_type fct =
(** In some cases (goto for instance) we have to create a node before having
* processed if through [cfg_stmt]. It is important that the created node
* is the same than while the 'normal' processing ! That is why
- * this pattern matching might seem redondant with the other one. *)
+ * this pattern matching might seem redundant with the other one. *)
let get_stmt_node env s = match s.skind with
| Instr (Call (res, fct, args, _)) ->
get_node env (Vcall (s, res, get_call_type fct, args))
@@ -933,7 +933,7 @@ let clean_graph cfg =
* Below, we use an algorithm from the paper :
* "A New Algorithm for Identifying Loops in Decompilation"
* of Tao Wei, Jian Mao, Wei Zou, and Yu Chen,
- * to gather information about the loops in the builted CFG.
+ * to gather information about the loops in the built CFG.
*)
module type WeiMaoZouChenInput = sig
diff --git a/src/plugins/wp/cil2cfg.mli b/src/plugins/wp/cil2cfg.mli
index ad99002599a8e5f7cef5536dba8de04f643de07e..6cbf2b795747723b17e8121dec449e5b7ef98482 100644
--- a/src/plugins/wp/cil2cfg.mli
+++ b/src/plugins/wp/cil2cfg.mli
@@ -126,7 +126,7 @@ val get_edge_labels : edge -> Clabels.c_label list
(** @return None when the edge leads to the end of the function. *)
val get_edge_next_stmt : t -> edge -> stmt option
-(** wether an exit edge exists or not *)
+(** whether an exit edge exists or not *)
val has_exit : t -> bool
(** Find the edges where the precondition of the node statement have to be
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index c0a47dde9cb3073a8118eee261ac7bcd70befe14..9f3e2669776b584390c582a7c1826261a6664a7d 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -498,7 +498,7 @@ let field_offset fd =
(* domain(signed) *)
(* then convert to signed *)
(* Otherwise: *)
-(* both are converted to unsiged *)
+(* both are converted to unsigned *)
(* *)
(* Case 2 is actually the negative *)
(* of Case 1, and both simplifies *)
diff --git a/src/plugins/wp/driver.mll b/src/plugins/wp/driver.mll
index 35ab96dfeb3bbfef8dd87cbd1be5cd4e58094b71..9023a07cc400510fd542bcc7f35fa7fb483273c5 100644
--- a/src/plugins/wp/driver.mll
+++ b/src/plugins/wp/driver.mll
@@ -309,7 +309,7 @@ and bal = parse
let op = {
- inversible = false ;
+ invertible = false ;
associative = false ;
commutative = false ;
idempotent = false ;
@@ -344,8 +344,8 @@ and bal = parse
op_link { op with commutative = true ; associative = true } input
| ID "idempotent" -> skip input ; skipkey input ":" ;
op_link { op with idempotent = true } input
- | ID "inversible" -> skip input ; skipkey input ":" ;
- op_link { op with inversible = true } input
+ | ID "invertible" -> skip input ; skipkey input ":" ;
+ op_link { op with invertible = true } input
| ID "neutral" ->
skip input ; let e = op_elt input in
op_link { op with neutral = e } input
diff --git a/src/plugins/wp/dyncall.mli b/src/plugins/wp/dyncall.mli
index 22080944a57ee24a28b60831521f646da3573e3f..1f7fc0fd61ae7e7e948469152079e955677746d7 100644
--- a/src/plugins/wp/dyncall.mli
+++ b/src/plugins/wp/dyncall.mli
@@ -33,5 +33,5 @@ val get : ?bhv:string -> stmt -> kernel_function list
val compute : unit -> unit
(** Forces computation of dynamic calls.
- Otherwize, they are computed lazily on [get].
+ Otherwise, they are computed lazily on [get].
Requires [-wp-dynamic]. *)
diff --git a/src/plugins/wp/mcfg.ml b/src/plugins/wp/mcfg.ml
index d5f5f4ce22b47cadae229f21cc76986b294283f4..9dca47d019a14e746e5ddb2185423784eb438f6f 100644
--- a/src/plugins/wp/mcfg.ml
+++ b/src/plugins/wp/mcfg.ml
@@ -51,7 +51,7 @@ end
* Usually, the propagated thing should be a predicate,
* but it can be more sophisticated like lists of predicates,
* or maybe a structure to keep hypotheses and goals separated.
- * Moreover, proof obligations may also need to be handeled.
+ * Moreover, proof obligations may also need to be handled.
**)
module type S = sig
diff --git a/src/plugins/wp/qed/old/assistant.ml b/src/plugins/wp/qed/old/assistant.ml
index 169d01c1e15e962f7b1424151b9e46b3211d74d3..09eb04b451d0c5318b404557872f5a42e2216d31 100644
--- a/src/plugins/wp/qed/old/assistant.ml
+++ b/src/plugins/wp/qed/old/assistant.ml
@@ -1,5 +1,5 @@
(* -------------------------------------------------------------------------- *)
-(* --- Proof Assistent --- *)
+(* --- Proof Assistant --- *)
(* -------------------------------------------------------------------------- *)
open Qed
diff --git a/src/plugins/wp/qed/old/equality.mli b/src/plugins/wp/qed/old/equality.mli
index 8681b37b32f6cf0902c0d6cd1c3d4df6d0a282a2..31245d0b6bbbc4eff25c982f65decc9d1111da81 100644
--- a/src/plugins/wp/qed/old/equality.mli
+++ b/src/plugins/wp/qed/old/equality.mli
@@ -29,7 +29,7 @@ sig
(** The class of [t] is the singleton [t]. *)
val compute : eqs -> term -> term
- (** Recursively replace sub-terms by their representent.
+ (** Recursively replace sub-terms by their representant.
@raise Contradiction if computation introduce inequalities. *)
val are_equal : eqs -> term -> term -> maybe
@@ -40,7 +40,7 @@ sig
val assume : eqs -> term -> eqs
(** Add a new hypothesis [h].
- If [h] is a [a=b], merges [a] and [b]. Otherwize,
+ If [h] is a [a=b], merges [a] and [b]. Otherwise,
merges [h] with [true] and [not h] with [false].
@raise Contradiction if the computations introduce non-equal terms. *)
diff --git a/src/plugins/wp/qed/old/grammar.mli b/src/plugins/wp/qed/old/grammar.mli
index 9755efc5b798fe79743c6d00dad62eb8362c7fbc..311feffbd22b9f0542f255898a9a8bb6af0d9552 100644
--- a/src/plugins/wp/qed/old/grammar.mli
+++ b/src/plugins/wp/qed/old/grammar.mli
@@ -17,7 +17,7 @@ open Syntax
{3 Strategy and Tactics}
Tactics can be used as strategy.
- - [ strategy := ("case" H: script)+ ("otherwize": script)? ]
+ - [ strategy := ("case" H: script)+ ("otherwise": script)? ]
- [ tactic := "straightforward" ]
- [ tactic := "by" theorem ]
diff --git a/src/plugins/wp/qed/old/proof.mli b/src/plugins/wp/qed/old/proof.mli
index b5fdb9c5f5efe38919f2757e26ebb430f151eb09..833ab0b10d26a35a1647dca5b6b4fa7c6094a95f 100644
--- a/src/plugins/wp/qed/old/proof.mli
+++ b/src/plugins/wp/qed/old/proof.mli
@@ -59,7 +59,7 @@ sig
- check goal is [Q1,..,Qn.P],
- when [Qi=forall xi], check [Li=Lvar y] and [y] is fresh,
- when [Qi=exists xi], check [Li=Lterm t],
- - finally prove [P[xi:=Li]] witrh [Pgoal]. *)
+ - finally prove [P[xi:=Li]] with [Pgoal]. *)
| Induction of T.term * proof * proof * T.var * proof
(** [Induction(a,Ppos,Pinit,n,Pind)]:
diff --git a/src/plugins/wp/qed/old/simplifier.mli b/src/plugins/wp/qed/old/simplifier.mli
index 0d138553af22f831852bcafae0337aece62e7fc7..d62bc249b0cdc174df22a19c6fdd66da957b05c7 100644
--- a/src/plugins/wp/qed/old/simplifier.mli
+++ b/src/plugins/wp/qed/old/simplifier.mli
@@ -45,8 +45,8 @@ sig
val simplify : T.term simplifier list -> T.term -> T.term
(** Might raises [NoSolution] from a plugin at initialization
- stage. Otherwize, [NoSolution] exceptions are likely to be
- catched during simplification, hence pruning any contradictory
+ stage. Otherwise, [NoSolution] exceptions are likely to be
+ caught during simplification, hence pruning any contradictory
hypothesis. *)
end
diff --git a/src/plugins/wp/qed/old/srange.mli b/src/plugins/wp/qed/old/srange.mli
index 517a681f898cfbfab8e946c7029cc1dc840f4013..77ec420b6db2afe7294150c952034a151ffd5aef 100644
--- a/src/plugins/wp/qed/old/srange.mli
+++ b/src/plugins/wp/qed/old/srange.mli
@@ -34,7 +34,7 @@ sig
end
-(** A Theory for arythmetics comparisons *)
+(** A Theory for arithmetic comparisons *)
module Make(T : Term)(D : Domain) :
sig
diff --git a/src/plugins/wp/qed/src/bvars.mli b/src/plugins/wp/qed/src/bvars.mli
index 57328a6d0086dde930c9ce0d4533131231f4c75a..8439712e5ec06c2c28a870d294d48adb28a500c6 100644
--- a/src/plugins/wp/qed/src/bvars.mli
+++ b/src/plugins/wp/qed/src/bvars.mli
@@ -45,7 +45,7 @@ val is_empty : t -> bool
(** No bound variables *)
val contains : int -> t -> bool
-(** if [may_constains k s] returns [false] then [k] does not belong to [s] *)
+(** if [contains k s] returns [false] then [k] does not belong to [s] *)
val overlap : int -> int -> t -> bool
(** if [may_overlap k n s] returns [false] then no variable [i] with
diff --git a/src/plugins/wp/qed/src/export_whycore.ml b/src/plugins/wp/qed/src/export_whycore.ml
index 2e13ea17ffb8ac477868b46b5949d9eae4d3702c..ecf415a04196880becd9deab9af1f65526cb7e56 100644
--- a/src/plugins/wp/qed/src/export_whycore.ml
+++ b/src/plugins/wp/qed/src/export_whycore.ml
@@ -182,7 +182,7 @@ struct
| Cterm -> fprintf fmt "function %s" name
method virtual pp_trigger : trigger printer
- method virtual pp_intros : tau -> string list printer (* forall with no separatyor *)
+ method virtual pp_intros : tau -> string list printer (* forall with no separator *)
method declare_prop ~kind fmt lemma xs tgs (p : term) =
self#global
diff --git a/src/plugins/wp/qed/src/logic.mli b/src/plugins/wp/qed/src/logic.mli
index 6ed25cd75c0b9a1d058d379238c802e23cec7b79..627e966fbcfefd390158de53e786cc385ee08ee1 100644
--- a/src/plugins/wp/qed/src/logic.mli
+++ b/src/plugins/wp/qed/src/logic.mli
@@ -34,7 +34,7 @@ type 'a element =
(** Algebraic properties for user operators. *)
type 'a operator = {
- inversible : bool ; (* x+y = x+z <-> y=z (on both side) *)
+ invertible : bool ; (* x+y = x+z <-> y=z (on both side) *)
associative : bool ; (* x+(y+z)=(x+y)+z *)
commutative : bool ; (* x+y=y+x *)
idempotent : bool ; (* x+x = x *)
@@ -283,7 +283,7 @@ sig
val e_subst : ?sigma:sigma -> (term -> term) -> term -> term
val e_subst_var : var -> term -> term -> term
- (** {3 Localy Nameless Representation} *)
+ (** {3 Locally Nameless Representation} *)
val lc_bind : var -> term -> bind (** Close [x] as a new bound variable *)
val lc_open : var -> bind -> term (** Instantiate top bound variable *)
@@ -359,7 +359,7 @@ sig
(** {3 Specific Patterns} *)
val consequence : term -> term -> term
- (** Kowning [h], [consequence h a] returns [b] such that [h -> (a<->b)] *)
+ (** Knowing [h], [consequence h a] returns [b] such that [h -> (a<->b)] *)
val literal : term -> bool * term
val congruence_eq : term -> term -> (term * term) list option
(** If [congruence_eq a b] returns [[ai,bi]], [a=b] is equivalent to [And{ai=bi}]. *)
diff --git a/src/plugins/wp/qed/src/plib.mli b/src/plugins/wp/qed/src/plib.mli
index 63fa35e84af3fcda914f769929b773064fd047d2..a918492e876a26aaa66e08beb44d9103b40cdc49 100644
--- a/src/plugins/wp/qed/src/plib.mli
+++ b/src/plugins/wp/qed/src/plib.mli
@@ -33,7 +33,7 @@ val sprintf : ('a,Format.formatter,unit,string) format4 -> 'a
val failure : ('a,Format.formatter,unit,'b) format4 -> 'a
val to_string : (Format.formatter -> 'a -> unit) -> 'a -> string
-(** Printy printers *)
+(** Pretty printers *)
type 'a printer = Format.formatter -> 'a -> unit
type 'a printer2 = Format.formatter -> 'a -> 'a -> unit
diff --git a/src/plugins/wp/qed/src/pool.mli b/src/plugins/wp/qed/src/pool.mli
index 0a66f40d06bdd2abb331c33de333ea7ec5074f27..111792a370ad2c1d6d3d4084a835fe1cdaaeff4c 100644
--- a/src/plugins/wp/qed/src/pool.mli
+++ b/src/plugins/wp/qed/src/pool.mli
@@ -21,7 +21,7 @@
(**************************************************************************)
(* -------------------------------------------------------------------------- *)
-(* --- Variable Manegement --- *)
+(* --- Variable Management --- *)
(* -------------------------------------------------------------------------- *)
open Hcons
diff --git a/src/plugins/wp/qed/src/pretty.ml b/src/plugins/wp/qed/src/pretty.ml
index bed88d3c68bf168881c9e498b55797cdfc08778e..5c3b31d7d66d0aa1619b99d6fed79e9a18a1ba38 100644
--- a/src/plugins/wp/qed/src/pretty.ml
+++ b/src/plugins/wp/qed/src/pretty.ml
@@ -353,7 +353,7 @@ struct
List.iter (fun e -> fprintf fmt "%s@,%a" op (pp_atom env) e) es
(* -------------------------------------------------------------------------- *)
- (* --- Horizonal Boxes --- *)
+ (* --- Horizontal Boxes --- *)
(* -------------------------------------------------------------------------- *)
and pp_hbox (env:env) (sep:string) (fmt:formatter) = function
diff --git a/src/plugins/wp/qed/src/term.ml b/src/plugins/wp/qed/src/term.ml
index 372e97df973e3d6213aa1797fd61ae56bc3047d8..dd0a0b80648f173b7706463ac7a92789cf262fb6 100644
--- a/src/plugins/wp/qed/src/term.ml
+++ b/src/plugins/wp/qed/src/term.ml
@@ -981,7 +981,7 @@ struct
| [_] as l -> l
| x::( (y::_) as w ) -> if x==y then op_idempotent w else x :: op_idempotent w
- let op_inversible xs ys =
+ let op_invertible xs ys =
let rec simpl modified turn xs ys = match xs , ys with
| x::xs , y::ys when x==y -> simpl true turn xs ys
| _ ->
@@ -1422,7 +1422,7 @@ struct
| S_equal (* equal constants or constructors *)
| S_disequal (* different constants or constructors *)
| S_injection (* same function, injective or constructor *)
- | S_inversible (* same function, inversible on both side *)
+ | S_invertible (* same function, invertible on both side *)
| S_disjunction (* both constructors, but different ones *)
| S_functions (* general functions *)
@@ -1430,7 +1430,7 @@ struct
if Fun.equal f g then
match Fun.category f with
| Logic.Injection -> S_injection
- | Logic.Operator { inversible=true } -> S_inversible
+ | Logic.Operator { invertible=true } -> S_invertible
| Logic.Constructor -> S_equal
| Logic.Function | Logic.Operator _ -> S_functions
else
@@ -1506,8 +1506,8 @@ struct
| S_injection -> eq_maybe x y (eq_all e_eq xs ys)
| S_disjunction -> e_false
| S_functions -> c_builtin_eq x y
- | S_inversible ->
- let modified,xs,ys = op_inversible xs ys in
+ | S_invertible ->
+ let modified,xs,ys = op_invertible xs ys in
if modified
then c_builtin_eq (e_fun f xs) (e_fun g ys)
else c_builtin_eq x y
@@ -1552,8 +1552,8 @@ struct
| S_injection -> neq_maybe x y (neq_any e_neq xs ys)
| S_disjunction -> e_true
| S_functions -> c_builtin_neq x y
- | S_inversible ->
- let modified,xs,ys = op_inversible xs ys in
+ | S_invertible ->
+ let modified,xs,ys = op_invertible xs ys in
if modified
then c_builtin_neq (e_fun f xs) (e_fun g ys)
else c_builtin_neq x y
@@ -1894,7 +1894,7 @@ struct
| Fun(f,xs) , Fun(g,ys) ->
begin
match structural f g with
- | S_equal | S_disequal | S_disjunction | S_inversible -> []
+ | S_equal | S_disequal | S_disjunction | S_invertible -> []
| S_injection -> concat2 congr_argeq xs ys
| S_functions -> raise NO_CONGRUENCE
end
@@ -1912,7 +1912,7 @@ struct
| Fun(f,xs) , Fun(g,ys) ->
begin
match structural f g with
- | S_equal | S_disequal | S_disjunction | S_inversible -> []
+ | S_equal | S_disequal | S_disjunction | S_invertible -> []
| S_injection -> concat2 congr_argneq xs ys
| S_functions -> raise NO_CONGRUENCE
end
@@ -1956,7 +1956,7 @@ struct
| S_disequal -> e_false
| S_injection -> e_all2 flat_eq xs ys
| S_disjunction -> e_false
- | S_functions | S_inversible -> e_eq a b
+ | S_functions | S_invertible -> e_eq a b
end
| Rdef fxs , Rdef gys ->
begin
@@ -1976,7 +1976,7 @@ struct
| S_disequal -> e_true
| S_injection -> e_any2 flat_neq xs ys
| S_disjunction -> e_true
- | S_functions | S_inversible -> e_neq a b
+ | S_functions | S_invertible -> e_neq a b
end
| Rdef fxs , Rdef gys ->
begin
diff --git a/src/plugins/wp/qed/tests/Intmapref.ml b/src/plugins/wp/qed/tests/Intmapref.ml
index edc652bdfa8613b746ef31e898d95812df773199..7f77298b2c5f3fe9dfe13921a5f60c129fee2a99 100644
--- a/src/plugins/wp/qed/tests/Intmapref.ml
+++ b/src/plugins/wp/qed/tests/Intmapref.ml
@@ -105,7 +105,7 @@ struct
let n = a.(x lsr 1)
in if x land 1 = 0 then n else f n
in
- let dkeys = (* extending dkeys array by replication on the hightest byte *)
+ let dkeys = (* extending dkeys array by replication on the highest byte *)
let bytes = match Sys.word_size with
| 32 -> 4
| 64 -> 8
@@ -137,7 +137,7 @@ struct
end
-module type Maping =
+module type Mapping =
sig
type 'a t
@@ -147,7 +147,7 @@ sig
end
-module Oracle(M1 : Maping)(M2 : Maping) =
+module Oracle(M1 : Mapping)(M2 : Mapping) =
struct
let timed = ref None
diff --git a/src/plugins/wp/share/coqwp/Bits.v b/src/plugins/wp/share/coqwp/Bits.v
index 61ac0c1a130d14dccb8fa5aa0eaf529b83c175ee..6ef9e065ba161bcef67bae64d85e263450fd36c0 100644
--- a/src/plugins/wp/share/coqwp/Bits.v
+++ b/src/plugins/wp/share/coqwp/Bits.v
@@ -173,7 +173,7 @@ Qed.
(** Function [f] has constant value [b] from rank [k]. *)
Definition trailing f (n:nat) (b:bool) := forall k, n <= k -> f k = b.
-(** Returns the lowest index such than [f n=b], and [n] otherwize. *)
+(** Returns the lowest index such than [f n=b], and [n] otherwise. *)
Fixpoint last f n b {struct n} :=
match n with
| O => O
diff --git a/src/plugins/wp/share/src/Bits.v b/src/plugins/wp/share/src/Bits.v
index 062ebd88ed97a4c93efd564e9048368e19b05e45..18bc1674b9ff194eaa582368ee4fb93ab7f928a9 100644
--- a/src/plugins/wp/share/src/Bits.v
+++ b/src/plugins/wp/share/src/Bits.v
@@ -173,7 +173,7 @@ Qed.
(** Function [f] has constant value [b] from rank [k]. *)
Definition trailing f (n:nat) (b:bool) := forall k, n <= k -> f k = b.
-(** Returns the lowest index such than [f n=b], and [n] otherwize. *)
+(** Returns the lowest index such than [f n=b], and [n] otherwise. *)
Fixpoint last f n b {struct n} :=
match n with
| O => O
diff --git a/src/plugins/wp/share/why3/Bits.v b/src/plugins/wp/share/why3/Bits.v
index 2b5f387aadf2d30b087f4a8b294d5e6e1ff9d638..0d7d4f445603182a1b62d3f5e29ec809f3c6a153 100644
--- a/src/plugins/wp/share/why3/Bits.v
+++ b/src/plugins/wp/share/why3/Bits.v
@@ -173,7 +173,7 @@ Qed.
(** Function [f] has constant value [b] from rank [k]. *)
Definition trailing f (n:nat) (b:bool) := forall k, n <= k -> f k = b.
-(** Returns the lowest index such than [f n=b], and [n] otherwize. *)
+(** Returns the lowest index such than [f n=b], and [n] otherwise. *)
Fixpoint last f n b {struct n} :=
match n with
| O => O
diff --git a/src/plugins/wp/tests/wp_acsl/axioms.i b/src/plugins/wp/tests/wp_acsl/axioms.i
index 8d0c79e79bb095d8eadcd201c7d710254b5d9378..1368722e6e1ca7b895d980b2216cc355480cba48 100644
--- a/src/plugins/wp/tests/wp_acsl/axioms.i
+++ b/src/plugins/wp/tests/wp_acsl/axioms.i
@@ -2,7 +2,7 @@
OPT: -wp -wp-model Typed -wp-par 1
*/
-// Test for the instanciation of axioms with labels.
+// Test for the instantiation of axioms with labels.
// The axiomatic A is equivalent (in spirit) to the definition of predicate Q.
/*@ axiomatic A {
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index dd3cf14a905e75e79381fa3d65f2658277dbc58c..e74eab5d5775cbdb844fb6b855a0093b09cfe4c4 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -243,7 +243,7 @@ type strategy_info = {
}
(*----------------------------------------------------------------------------*)
-(* Adding things in the stategy *)
+(* Adding things in the strategy *)
(*----------------------------------------------------------------------------*)
(* Select annotations to take as Hyp/Goal/... *)
@@ -1310,7 +1310,7 @@ let get_precond_strategies ~model p =
else []
in
let call_sites = Kernel_function.find_syntactic_callsites kf in
- let add_call_pre_stategy acc (kf_caller, stmt) =
+ let add_call_pre_strategy acc (kf_caller, stmt) =
let asked = CallPre (stmt, Some p) in
get_strategies NoAssigns kf_caller model [] None asked @ acc
in
@@ -1319,7 +1319,7 @@ let get_precond_strategies ~model p =
"No direct call sites for function '%a': cannot check pre-conditions"
Kernel_function.pretty kf;
strategies)
- else List.fold_left add_call_pre_stategy strategies call_sites
+ else List.fold_left add_call_pre_strategy strategies call_sites
| _ ->
invalid_arg "[get_precond_strategies] not a function precondition"
diff --git a/src/plugins/wp/wpAnnot.mli b/src/plugins/wp/wpAnnot.mli
index 3a9ec831e58bfb46d986ffe8db077e9a0f9d83d2..43171db27d4c5f630cd5b55217fd52594882f8c2 100644
--- a/src/plugins/wp/wpAnnot.mli
+++ b/src/plugins/wp/wpAnnot.mli
@@ -45,7 +45,7 @@ val is_composed : proof -> bool
(** whether a proof needs several lemma to be complete *)
val is_proved : proof -> bool
-(** wether all partial proofs have been accumulated or not *)
+(** whether all partial proofs have been accumulated or not *)
val target : proof -> Property.t
val dependencies : proof -> Property.t list
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index e2586250af0df8974d2ef4ca165d853962003cc2..3e0707605be3bc69813b00d7be5b069bd2627965 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -47,7 +47,7 @@ type prop_kind =
| PKPre of kernel_function * stmt * Property.t (** precondition for function
at stmt, property of the require. Many information that should come
from the p_prop part of the prop_id, but in the PKPre case,
- it seems that it is hiden in a IPBlob property ! *)
+ it seems that it is hidden in a IPBlob property ! *)
type prop_id = {
p_kind : prop_kind ;
@@ -272,7 +272,7 @@ end = struct
(Kernel_function.find_englobing_kf stmt)
in Printf.sprintf "%s_call_%s" kf_name_of_stmt (base_id_prop_txt pre)
- (** function used to normanize basename *)
+ (** function used to normalize basename *)
let normalize_basename s =
(* truncates basename in order to limit length of file name *)
let max_len = Wp_parameters.TruncPropIdFileName.get () in
diff --git a/src/plugins/wp/wpPropId.mli b/src/plugins/wp/wpPropId.mli
index 6120492db89bf2d4d4395ec68b3fab2de913eb23..9d3f47cbb6db2c68013d53c55691079a14c9df8c 100644
--- a/src/plugins/wp/wpPropId.mli
+++ b/src/plugins/wp/wpPropId.mli
@@ -84,7 +84,7 @@ type prop_kind =
| PKPre of kernel_function * stmt * Property.t (** precondition for function
at stmt, property of the require. Many information that should come
from the p_prop part of the prop_id, but in the PKPre case,
- it seems that it is hiden in a IPBlob property ! *)
+ it seems that it is hidden in a IPBlob property ! *)
val pretty : Format.formatter -> prop_id -> unit
val pretty_context : Description.kf -> Format.formatter -> prop_id -> unit
diff --git a/src/plugins/wp/wpRTE.ml b/src/plugins/wp/wpRTE.ml
index 5ab161b003b1f96b8922e84ca7cb7dd017651df3..2c39d6ca4b3aa71fd68f5f22c09f4b02b3659bd7 100644
--- a/src/plugins/wp/wpRTE.ml
+++ b/src/plugins/wp/wpRTE.ml
@@ -37,7 +37,7 @@ let option name =
let status db kf =
try
(* Absolutely forbidden to use 'set' from Db.RteGen :
- this disables the generation of the associed RTE. *)
+ this disables the generation of the associated RTE. *)
let (_,_,get) = (!db) () in get kf
with Failure _ ->
Wp_parameters.warning ~once:true
diff --git a/src/plugins/wp/wpStrategy.ml b/src/plugins/wp/wpStrategy.ml
index f28f1d5b3fd084ffb32236422919a690a26d4842..7160d5e230a4d7b4c20d7519c9721f1b21b9390b 100644
--- a/src/plugins/wp/wpStrategy.ml
+++ b/src/plugins/wp/wpStrategy.ml
@@ -35,7 +35,7 @@ type annot_kind =
but not an hypothesis (see Aboth): A /\ ...*)
| Aboth of bool
(* annotation can be used as both hypothesis and goal :
- - with true : considerer as both : A /\ A=>..
+ - with true : considered as both : A /\ A=>..
- with false : we just want to use it as hyp right now. *)
| AcutB of bool
(* annotation is use as a cut :
@@ -56,8 +56,8 @@ type annot_kind =
module ForCall = Kernel_function.Map
(** Some elements can be used as both Hyp and Goal : because of the selection
- * mecanism, we need to add a boolean [as_goal] to tell if the element is to be
- * considered as a goal. If [false], the element can still be used as hypthesis.
+ * mechanism, we need to add a boolean [as_goal] to tell if the element is to be
+ * considered as a goal. If [false], the element can still be used as hypothesis.
*)
type annots = {
p_hyp : WpPropId.pred_info list;
diff --git a/src/plugins/wp/wpStrategy.mli b/src/plugins/wp/wpStrategy.mli
index bfb137b9cecdf2ce6b806a7aa1d9ed0a5cd4bb54..cbacc607981882223c66f769255cc170e5efbcbf 100644
--- a/src/plugins/wp/wpStrategy.mli
+++ b/src/plugins/wp/wpStrategy.mli
@@ -23,7 +23,7 @@
open Cil_types
(* -------------------------------------------------------------------------- *)
-(** This file provide all the functions to build a stategy that can then
+(** This file provide all the functions to build a strategy that can then
* be used by the main generic calculus. *)
(* -------------------------------------------------------------------------- *)
@@ -45,7 +45,7 @@ type annot_kind =
| Agoal (** annotation is a goal,
but not an hypothesis (see Aboth): A /\ ...*)
| Aboth of bool (** annotation can be used as both hypothesis and goal :
- - with true : considerer as both : A /\ A=>..
+ - with true : considered as both : A /\ A=>..
- with false : we just want to use it as hyp right now. *)
| AcutB of bool (** annotation is use as a cut :
- with true (A is also a goal) -> A (+ proof obligation A => ...)
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index ca5b5191763254aad50a66c336b66de4de5cf8a5..972d9c13d130068ded4ee467b8a9de134cd4a12c 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -170,7 +170,7 @@ module Model =
* '+raw' no logic variable\n\
* '+ref' by-reference-style pointers detection\n\
* '+nat/+int' natural / machine-integers arithmetics\n\
- * '+real/+float' real / IEEE floatting point arithmetics"
+ * '+real/+float' real / IEEE floating point arithmetics"
end)
let () = Parameter_customize.set_group wp_model
@@ -360,7 +360,7 @@ let () = Parameter_customize.set_group wp_simplifier
module SimplifyIsCint =
True(struct
let option_name = "-wp-simplify-is-cint"
- let help = "Remove redondant machine integer range hypothesis."
+ let help = "Remove redundant machine integer range hypothesis."
end)
let () = Parameter_customize.set_group wp_simplifier
diff --git a/tests/slicing/loops.i b/tests/slicing/loops.i
index 1a21b4580570f3b70de62a19fdfb66141db4d327..d4a8e7179cd4e0385bc4e6d7f3f2f12853984ca7 100644
--- a/tests/slicing/loops.i
+++ b/tests/slicing/loops.i
@@ -103,14 +103,14 @@ void test_infinite_loop_3 (int ctrl1, int ctrl2,
if (no_ctrl) { /* Don't control an assignment of G
* which leads to the return */
G = no_data ; /* Don't affect the final value of G
- * because the assignement
+ * because the assignment
* does not lead to the return */
while (1)
G = no_data ; /* Don't affect the final value of G
- * because the assignement
+ * because the assignment
* does not lead to the return */
G = no_data ; /* Don't affect the final value of G
- * because the assignement
+ * because the assignment
* is dead code */
}
if (ctrl2)
@@ -127,14 +127,14 @@ void test_infinite_loop_4 (int ctrl1, int ctrl2, int no_ctrl,
if (no_ctrl) { /* Don't control an assignment of G
* which leads to the return */
G += no_data ; /* Don't affect the final value of G
- * because the assignement
+ * because the assignment
* does not lead to the return */
while (1)
G += no_data ; /* Don't affect the final value of G
- * because the assignement
+ * because the assignment
* does not lead to the return */
G += no_data ; /* Don't affect the final value of G
- * because the assignement
+ * because the assignment
* is dead code */
}
if (ctrl2)
@@ -157,7 +157,7 @@ void test_infinite_loop_5 (int ctrl1, int ctrl2, int no_ctrl,
G += no_data ; /* Don't affect ... dead code */
}
else /* <-- This is the difference with test_infinite_loop_4.
- * It is only a syntaxical difference,
+ * It is only a syntactical difference,
* and not a semantical difference
* since the previous statement "G += no_data" is dead.
*/
diff --git a/tests/slicing/slice_no_body.ml b/tests/slicing/slice_no_body.ml
index bb5d0143c9635321e682be7ded11067e19ba9b93..76a1b56dfe3fb5e8be4e5c61abb4f9bc1e801a14 100644
--- a/tests/slicing/slice_no_body.ml
+++ b/tests/slicing/slice_no_body.ml
@@ -8,7 +8,7 @@ let callers kf = !Db.Value.callers kf
(** simple implementation to select every calls to [kf] source function.
* The problem of this implementation is that it can generate several slice
-* for one fonction during propagation to the callers.
+* for one function during propagation to the callers.
* See [S.Request.select_fun_calls] for a better implementation.
* *)
let call_f project kf =
diff --git a/tests/value/volatile.c b/tests/value/volatile.c
index 21c15b3113cb0fd6c91bb64f8004d0914e8053f4..7b2aca52de562523ca1f53f656ed129de0ead937 100644
--- a/tests/value/volatile.c
+++ b/tests/value/volatile.c
@@ -62,7 +62,7 @@ int main1 () {
h = 1;
E = h;
- /* assignement via pointer */
+ /* assignment via pointer */
X = -1;
Y = -1;
pv = (int *) &X;