From 62caa4a430c707fe44430c264f7781e4c47d4691 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Wed, 8 Feb 2017 14:50:02 +0100
Subject: [PATCH] typos
---
Changelog | 8 +++---
Makefile | 6 ++--
configure.in | 4 +--
doc/developer/advance.tex | 14 +++++-----
doc/developer/architecture.tex | 4 +--
doc/developer/changes.tex | 4 +--
doc/developer/refman.tex | 2 +-
doc/developer/tutorial.tex | 10 +++----
doc/release/intro.tex | 6 ++--
doc/release/website.tex | 2 +-
doc/userman/user-changes.tex | 2 +-
doc/userman/user-start.tex | 2 +-
doc/value/slicing.tex | 8 +++---
headers/headache_config.txt | 2 +-
share/Makefile.plugin.template | 4 +--
share/machdep.c | 2 +-
src/kernel_internals/parsing/clexer.mll | 2 +-
src/kernel_internals/typing/alpha.ml | 2 +-
src/kernel_internals/typing/cabs2cil.ml | 16 +++++------
src/kernel_internals/typing/cfg.ml | 2 +-
.../typing/infer_annotations.ml | 2 +-
src/kernel_internals/typing/logic_builtin.ml | 2 +-
src/kernel_internals/typing/mergecil.ml | 4 +--
.../abstract_interp/abstract_interp.ml | 2 +-
.../abstract_interp/abstract_interp.mli | 2 +-
src/kernel_services/abstract_interp/base.ml | 2 +-
src/kernel_services/abstract_interp/base.mli | 2 +-
src/kernel_services/abstract_interp/fval.ml | 2 +-
src/kernel_services/abstract_interp/fval.mli | 12 ++++----
src/kernel_services/abstract_interp/ival.ml | 2 +-
src/kernel_services/abstract_interp/lmap.mli | 2 +-
.../abstract_interp/lmap_sig.mli | 4 +--
.../abstract_interp/offsetmap.ml | 6 ++--
.../abstract_interp/offsetmap_sig.mli | 4 +--
.../abstract_interp/origin.mli | 2 +-
src/kernel_services/analysis/bit_utils.ml | 4 +--
src/kernel_services/analysis/dataflow.ml | 2 +-
src/kernel_services/analysis/dataflow.mli | 2 +-
src/kernel_services/analysis/dataflow2.ml | 12 ++++----
src/kernel_services/analysis/dataflow2.mli | 2 +-
src/kernel_services/analysis/dataflows.mli | 6 ++--
src/kernel_services/analysis/loop.ml | 2 +-
src/kernel_services/analysis/ordered_stmt.mli | 2 +-
src/kernel_services/analysis/stmts_graph.mli | 2 +-
src/kernel_services/ast_data/alarms.ml | 2 +-
src/kernel_services/ast_data/annotations.ml | 2 +-
src/kernel_services/ast_data/cil_types.mli | 4 +--
src/kernel_services/ast_data/globals.ml | 2 +-
src/kernel_services/ast_data/property.ml | 2 +-
.../ast_data/property_status.mli | 4 +--
.../ast_printing/cil_printer.ml | 6 ++--
src/kernel_services/ast_printing/cprint.ml | 2 +-
.../ast_printing/description.mli | 2 +-
.../ast_printing/printer_api.mli | 2 +-
src/kernel_services/ast_queries/ast_info.ml | 14 +++++-----
src/kernel_services/ast_queries/ast_info.mli | 4 +--
src/kernel_services/ast_queries/cil.ml | 14 +++++-----
src/kernel_services/ast_queries/cil.mli | 14 +++++-----
.../ast_queries/logic_typing.ml | 6 ++--
.../ast_transformations/filter.mli | 2 +-
.../cmdline_parameters/cmdline.mli | 2 +-
.../cmdline_parameters/parameter_builder.ml | 2 +-
.../parameter_customize.mli | 2 +-
.../cmdline_parameters/parameter_sig.mli | 6 ++--
.../cmdline_parameters/typed_parameter.mli | 2 +-
src/kernel_services/parsetree/cabs.ml | 8 +++---
.../plugin_entry_points/db.mli | 28 +++++++++----------
.../plugin_entry_points/dynamic.ml | 2 +-
.../plugin_entry_points/emitter.ml | 4 +--
.../plugin_entry_points/journal.mli | 4 +--
.../plugin_entry_points/kernel.ml | 4 +--
.../plugin_entry_points/log.ml | 2 +-
.../plugin_entry_points/log.mli | 4 +--
src/kernel_services/visitors/cabsvisit.mli | 2 +-
src/kernel_services/visitors/visitor.ml | 2 +-
src/libraries/datatype/datatype.mli | 4 +--
src/libraries/datatype/descr.mli | 4 +--
src/libraries/datatype/type.ml | 2 +-
src/libraries/datatype/type.mli | 4 +--
src/libraries/project/state.mli | 2 +-
src/libraries/project/state_builder.mli | 2 +-
src/libraries/stdlib/extlib.ml | 2 +-
src/libraries/stdlib/extlib.mli | 2 +-
src/libraries/utils/c_bindings.c | 2 +-
src/libraries/utils/command.mli | 4 +--
src/libraries/utils/hptmap_sig.mli | 2 +-
src/libraries/utils/hptset.ml | 2 +-
src/libraries/utils/pretty_utils.mli | 4 +--
src/libraries/utils/rgmap.mli | 6 ++--
src/libraries/utils/task.mli | 4 +--
src/libraries/utils/wto.mli | 8 +++---
src/plugins/aorai/aorai_register.ml | 4 +--
src/plugins/aorai/aorai_utils.ml | 8 +++---
src/plugins/aorai/aorai_utils.mli | 4 +--
src/plugins/aorai/aorai_visitors.ml | 2 +-
src/plugins/aorai/data_for_aorai.mli | 4 +--
src/plugins/aorai/promelalexer.mll | 6 ++--
src/plugins/aorai/promelalexer_withexps.mll | 6 ++--
src/plugins/callgraph/cg.ml | 6 ++--
src/plugins/callgraph/cg_viewer.ml | 4 +--
src/plugins/constant_propagation/register.ml | 2 +-
src/plugins/from/callwise.ml | 2 +-
src/plugins/from/from_compute.ml | 6 ++--
src/plugins/from/from_compute.mli | 2 +-
src/plugins/gui/design.ml | 4 +--
src/plugins/gui/design.mli | 2 +-
src/plugins/gui/file_manager.ml | 2 +-
src/plugins/gui/filetree.ml | 2 +-
src/plugins/gui/filetree.mli | 2 +-
src/plugins/gui/gtk_helper.mli | 2 +-
src/plugins/gui/history.ml | 2 +-
src/plugins/gui/menu_manager.mli | 2 +-
src/plugins/gui/warning_manager.mli | 2 +-
src/plugins/gui/wbox.mli | 6 ++--
src/plugins/gui/wfile.mli | 2 +-
src/plugins/gui/widget.mli | 4 +--
src/plugins/gui/wpane.ml | 4 +--
src/plugins/gui/wpane.mli | 6 ++--
src/plugins/gui/wtext.mli | 4 +--
src/plugins/impact/compute_impact.ml | 4 +--
src/plugins/inout/cumulative_analysis.mli | 2 +-
src/plugins/inout/operational_inputs.ml | 8 +++---
src/plugins/loop_analysis/region_analysis.ml | 4 +--
src/plugins/loop_analysis/region_analysis.mli | 2 +-
src/plugins/metrics/metrics_base.mli | 4 +--
src/plugins/metrics/metrics_cilast.ml | 2 +-
src/plugins/metrics/metrics_cilast.mli | 2 +-
src/plugins/metrics/metrics_coverage.mli | 4 +--
src/plugins/metrics/metrics_gui.ml | 4 +--
src/plugins/metrics/metrics_gui.mli | 4 +--
src/plugins/metrics/metrics_parameters.mli | 2 +-
src/plugins/pdg/build.ml | 8 +++---
src/plugins/pdg/ctrlDpds.ml | 2 +-
src/plugins/pdg/pdg_state.ml | 2 +-
src/plugins/pdg/sets.ml | 2 +-
src/plugins/pdg_types/pdgIndex.ml | 4 +--
src/plugins/pdg_types/pdgMarks.mli | 6 ++--
src/plugins/pdg_types/pdgTypes.ml | 2 +-
src/plugins/pdg_types/pdgTypes.mli | 2 +-
.../report/tests/report/multi_emitters.ml | 4 +--
src/plugins/rte/options.ml | 2 +-
src/plugins/rte/rte.ml | 4 +--
src/plugins/rte/visit.ml | 8 +++---
src/plugins/scope/datascope.ml | 4 +--
src/plugins/scope/dpds_gui.ml | 2 +-
src/plugins/security_slicing/components.ml | 2 +-
src/plugins/slicing/fct_slice.ml | 2 +-
src/plugins/slicing/register_gui.ml | 2 +-
src/plugins/slicing/slicingActions.ml | 2 +-
src/plugins/slicing/slicingCmds.ml | 8 +++---
src/plugins/slicing/slicingMarks.ml | 4 +--
src/plugins/slicing/slicingProject.ml | 2 +-
src/plugins/slicing_types/slicingInternals.ml | 4 +--
src/plugins/slicing_types/slicingTypes.ml | 4 +--
src/plugins/sparecode/globs.ml | 2 +-
src/plugins/value/domains/abstract_domain.mli | 4 +--
.../value/domains/apron/apron_domain.ok.ml | 2 +-
.../value/domains/cvalue/builtins_malloc.ml | 10 +++----
.../value/domains/cvalue/builtins_nonfree.ml | 4 +--
.../cvalue/builtins_nonfree_print_c.mli | 2 +-
.../value/domains/cvalue/builtins_string.ml | 8 +++---
.../value/domains/cvalue/locals_scoping.mli | 2 +-
.../value/domains/gauges/gauges_domain.ml | 2 +-
src/plugins/value/domains/offsm_domain.ml | 4 +--
src/plugins/value/engine/abstractions.mli | 2 +-
src/plugins/value/engine/evaluation.ml | 10 +++----
src/plugins/value/engine/evaluation.mli | 2 +-
.../value/engine/non_linear_evaluation.ml | 4 +--
.../value/engine/partitioned_dataflow.ml | 4 +--
src/plugins/value/engine/transfer_logic.ml | 2 +-
src/plugins/value/eval.ml | 2 +-
src/plugins/value/eval.mli | 2 +-
src/plugins/value/gui_files/register_gui.ml | 10 +++----
src/plugins/value/legacy/eval_annots.ml | 6 ++--
src/plugins/value/legacy/eval_op.mli | 4 +--
src/plugins/value/legacy/eval_slevel.ml | 4 +--
src/plugins/value/legacy/eval_stmt.ml | 6 ++--
src/plugins/value/legacy/eval_terms.ml | 6 ++--
src/plugins/value/legacy/mem_exec.ml | 2 +-
src/plugins/value/legacy/mem_exec.mli | 2 +-
src/plugins/value/legacy/valarms.mli | 2 +-
src/plugins/value/legacy/warn.mli | 2 +-
src/plugins/value/utils/value_perf.ml | 4 +--
src/plugins/value/utils/value_util.mli | 4 +--
src/plugins/value/utils/widen.ml | 4 +--
src/plugins/value/value_parameters.ml | 2 +-
.../value/values/abstract_location.mli | 6 ++--
src/plugins/value/values/abstract_value.mli | 4 +--
src/plugins/value_types/cvalue.mli | 2 +-
src/plugins/value_types/function_Froms.ml | 4 +--
src/plugins/value_types/function_Froms.mli | 4 +--
src/plugins/variadic/classify.ml | 2 +-
src/plugins/variadic/generic.ml | 2 +-
src/plugins/variadic/standard.ml | 4 +--
src/plugins/variadic/tests/known/exec.c | 2 +-
src/plugins/variadic/tests/known/open_wrong.c | 2 +-
src/plugins/variadic/translate.ml | 2 +-
src/plugins/variadic/va_types.mli | 2 +-
src/plugins/wp/Cfloat.ml | 2 +-
src/plugins/wp/Cfloat.mli | 2 +-
src/plugins/wp/Cint.ml | 6 ++--
src/plugins/wp/Cint.mli | 4 +--
src/plugins/wp/Cleaning.ml | 2 +-
src/plugins/wp/Conditions.ml | 2 +-
src/plugins/wp/Conditions.mli | 4 +--
src/plugins/wp/Cstring.ml | 2 +-
src/plugins/wp/Cvalues.ml | 4 +--
src/plugins/wp/Cvalues.mli | 2 +-
src/plugins/wp/LogicSemantics.ml | 2 +-
src/plugins/wp/LogicUsage.ml | 2 +-
src/plugins/wp/MemTyped.ml | 4 +--
src/plugins/wp/MemVar.ml | 8 +++---
src/plugins/wp/Memory.ml | 6 ++--
src/plugins/wp/RefUsage.ml | 4 +--
src/plugins/wp/Region.ml | 2 +-
src/plugins/wp/Repr.mli | 2 +-
src/plugins/wp/Vlist.ml | 4 +--
src/plugins/wp/Vset.ml | 2 +-
src/plugins/wp/Vset.mli | 4 +--
src/plugins/wp/WpTac.ml | 6 ++--
src/plugins/wp/calculus.ml | 2 +-
src/plugins/wp/cfgDump.ml | 2 +-
src/plugins/wp/cfgWP.ml | 2 +-
src/plugins/wp/cil2cfg.ml | 4 +--
src/plugins/wp/cil2cfg.mli | 2 +-
src/plugins/wp/ctypes.ml | 2 +-
src/plugins/wp/driver.mll | 6 ++--
src/plugins/wp/dyncall.mli | 2 +-
src/plugins/wp/mcfg.ml | 2 +-
src/plugins/wp/qed/old/assistant.ml | 2 +-
src/plugins/wp/qed/old/equality.mli | 4 +--
src/plugins/wp/qed/old/grammar.mli | 2 +-
src/plugins/wp/qed/old/proof.mli | 2 +-
src/plugins/wp/qed/old/simplifier.mli | 4 +--
src/plugins/wp/qed/old/srange.mli | 2 +-
src/plugins/wp/qed/src/bvars.mli | 2 +-
src/plugins/wp/qed/src/export_whycore.ml | 2 +-
src/plugins/wp/qed/src/logic.mli | 6 ++--
src/plugins/wp/qed/src/plib.mli | 2 +-
src/plugins/wp/qed/src/pool.mli | 2 +-
src/plugins/wp/qed/src/pretty.ml | 2 +-
src/plugins/wp/qed/src/term.ml | 22 +++++++--------
src/plugins/wp/qed/tests/Intmapref.ml | 6 ++--
src/plugins/wp/share/coqwp/Bits.v | 2 +-
src/plugins/wp/share/src/Bits.v | 2 +-
src/plugins/wp/share/why3/Bits.v | 2 +-
src/plugins/wp/tests/wp_acsl/axioms.i | 2 +-
src/plugins/wp/wpAnnot.ml | 6 ++--
src/plugins/wp/wpAnnot.mli | 2 +-
src/plugins/wp/wpPropId.ml | 4 +--
src/plugins/wp/wpPropId.mli | 2 +-
src/plugins/wp/wpRTE.ml | 2 +-
src/plugins/wp/wpStrategy.ml | 6 ++--
src/plugins/wp/wpStrategy.mli | 4 +--
src/plugins/wp/wp_parameters.ml | 4 +--
tests/slicing/loops.i | 14 +++++-----
tests/slicing/slice_no_body.ml | 2 +-
tests/value/volatile.c | 2 +-
258 files changed, 500 insertions(+), 500 deletions(-)
diff --git a/Changelog b/Changelog
index efb27e56573..068aa475004 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 cf1e854254b..53ae95db952 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 c3705a3a592..2408602cc3d 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 108e62d1de9..1f6a0507dea 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 709a57c52a7..2df3d83a5dc 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 b2acdb7043a..5d081cc3ab8 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 9af475f8b62..3d2254979cb 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 17889df9339..e83f5e0175a 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 9ff6dbf54e4..64f267866d8 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 aa630b85543..3f6e75d34dc 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 b5402be1ba8..b6e51dbe006 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 e179a259575..fd924431fa3 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 80b392e234b..a02ac602fcb 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 f334be6c6eb..6582d030537 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 f9598c81b4b..c1517f8ff86 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 4aaf96666c0..43caa42a451 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 3b463ccf493..ebf9d3ab836 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 53ecb8d5bf2..7efe8438a3b 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 e126060d2f8..e8bf34710e1 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 09736aa2822..7bb00b18a2b 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 70bf32fe015..0cc78b649ac 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 05a8e16d231..b937d6b16ba 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 6dc74339d42..4a4e47782ce 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 3802bced80d..a2cac39ea15 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 910fb6a313c..212ee51ebd8 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 68784056543..7d6606e9951 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 d14c7b4f9fa..fed956fefd8 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 165cb80d8be..7123f40a4b2 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 9c54ba11aa3..abd1cbb4dba 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 68df66f7dff..f65fd0961af 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 53caae5a2e7..406c2cc5a0e 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 ce2d2440cc3..70e647bb95b 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 46cf3d735a9..24115a3dd7c 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 1eec8a7d952..12b9eece329 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 1549309d238..537bcbf8dd1 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 a175dffbd2b..a61a9d5b76f 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 0f32f243ea5..d65f32ff4c0 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 802f0605e28..94421fdc2a3 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 4286d8ec203..5fbca66581c 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 254c13ec36e..afe2a006914 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 a9c785b5f64..f3afd2f3d4b 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 1ea3490675c..5a774ef161c 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 a745f0beec0..cab45617cfe 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 5317836b7c0..0d2e5af1916 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 9743197b2e7..16c3e132261 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 8c8aae8c93a..78f1c02e4fe 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 6e1c769e6e2..42b0721eb66 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 a96082ded5f..ce9e69ee929 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 9e73d1630d1..6d4f25e3bad 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 36d6ede6ec6..8e8bb08ea3f 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 22596985ebd..2b9d94d4d77 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 22a9049ebbc..a104d412d42 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 36313bba3a9..c466144f9ad 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 3eba911e6dd..765b782f4da 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 54d5fb2bbc5..971bf4404e3 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 a1500650ff6..c68e4c0a8dc 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 f7401b5733b..77ae52aa0d0 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 37629dee94c..c494e12c6a7 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 29bb1b0327e..63bae4b6608 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 15a1a1db57e..f3099e23a02 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 95f0fb8ccd3..695210545de 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 042adcfedfd..2da9ef02340 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 6534b9ba715..933cf5214e6 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 cbbd63f5f31..7c5206c5ea6 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 35976b77720..48ba08f2b20 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 d17eb2af3eb..f0b7b94f54b 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 2ba894afcea..e7b0d6f04e8 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 7573b4e50f7..effc8d2cfbd 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 36872c05026..c4e473630a2 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 6d4836bb32c..dc0391c7b70 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 77900249ee9..079cdcea00c 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 08bf94274c2..b9f75d1a5be 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 da896ca36a2..d93f983026b 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 6091cf42ff4..4df5f481a41 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 e6cd12f3e30..f9da857ba9e 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 5bb81c6b20a..0c9e2da0560 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 b2cd632eceb..c420a202157 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 054ddf89876..7215f383564 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 2433dd2364a..42a2a17bbc7 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 ea98a6161db..b67cf7eb115 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 cd5ec62c5a8..7ae3c2ec42e 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 1d76856cac0..7e176edf36b 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 53e533497e0..6ed2a0a8fae 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 2760c0b57bd..4dbaa607890 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 f3b5e1dba4c..30f9dcb9176 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 33b238f2133..fa1ac37bce5 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 d96321d7fbd..dd5eabebd28 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 24332ed0f24..4829f39539d 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 e7a2c251a33..35a75229078 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 d00f39c2b55..eec28be5ca5 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 ca87e711ce9..a6313d69150 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 f27271f18ab..b8c9e090520 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 359d12f4f69..dfc4fa866b0 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 713e4e23353..5ccf05a9a78 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 e9350cde1eb..0f5b485abb5 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 ffca4f6477d..7179248f97e 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 a28414e90ba..68b97db0d63 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 7909d7e05a6..ce3a7c9e931 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 2a2b94156d4..1a7605b05d9 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 a5cfda94e0a..d58bbd570d1 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 ea4abeade42..d1055928d2a 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 17550dc355d..5c59508b7b5 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 2f5430b62e3..0cb7fe51fdb 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 e5c1785469b..8daa78f2989 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 5772ea04141..868a66fd4db 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 42036e30c6a..706249837d7 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 95082fa5a74..d4d0173ced6 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 3b36f8105c6..f32f90eb9c5 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 c066a1cdd9b..21f534cef98 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 13242edf0db..21ba828186b 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 8f33c4cc86c..badc51ebb05 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 bf0b1b6930b..54f6d65801a 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 65c5d3088b7..83d623f9051 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 357aada3dc6..7529975f046 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 b5758b144f9..b9e769747c0 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 afdbb981027..5090510f24a 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 160cdb2b692..b46b12942b9 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 c50c9466467..b23978d2321 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 222e391eac1..e432fd8332b 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 ff60e8be87a..bb4f81d0cdc 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 0d905d5dbd1..ddc7f5f6e39 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 8f3b5188e5c..5545a8ab13a 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 731cb7447d7..737b2f8bc15 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 dd692a28d18..de502a68232 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 ca6509b1fb5..e48d4864b2c 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 754c4e59219..261399b5f0f 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 db6eb4d0742..96e240ddffb 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 0227d3da610..5a9a387e178 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 cc2c0c388fa..ed160ff8b19 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 8b6d2d657ab..682d3edbbf9 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 fbb029f3b28..d5f1da0fc6d 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 70962e4421b..886b976570f 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 1485dad9c6c..2ce81a28ecf 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 2d7bd3c0b44..ee2560cec08 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 a039fab7d60..2ecfd16cb5a 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 22f7ebafcc2..975adc7bf52 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 41d190ed293..cec80924457 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 d4298f06f06..79856f8e41e 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 d9bd5d9f529..4a3d4a35ad9 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 43884570e53..055953df5d1 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 1d81cea21e8..772eab7ab70 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 6261cfd879f..c2c72c0fc70 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 682c55293e6..71134d7870d 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 194f39772b8..81e9e55e5d6 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 b0052bb9de9..ad052a26ef8 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 88e7c23c8ec..0e01b7962fc 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 5b85b043ed0..42124fa3651 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 8d3296a006d..bf6a38b55a3 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 2631b4dc299..70590fb5fd0 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 b74fe55619d..529f0446efa 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 e8c03f7edb3..ad00843722d 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 74b74a5d774..39ff546ca44 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 986a4ccca31..2f7b8263fb3 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 5ea4c68a4ba..d8639a98542 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 51046be16b7..d7935fb3720 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 227b1685412..37403ba5471 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 0957fcc10ca..aa450924e54 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 935bdbda827..5b3e7281e6f 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 71186b33dc1..e6086eb1dfd 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 9ed3ea21332..f0bc35faa51 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 46c69460081..794e05dc6db 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 22f11d66f90..1486df94728 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 cb9a805ba4f..ddd017d40a0 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 625ee1675bd..d28f879b220 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 2c883ecf25a..2d4a018f82e 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 ea10b4c4b38..f1f9eba6aaa 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 bc12624dabc..0792bf86dda 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 372898fac1b..1df0c77a427 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 ac161c939bd..a9f152a3c15 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 538278417b2..84cd4abe002 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 79dbbb97839..635dcd1d793 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 f01ea87e356..7404b61fd3e 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 f45ff944dd7..d63c58f8cc7 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 dc58de3cafc..ce9493c6a0d 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 8a0cbecdad7..0573189845a 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 455908a959b..74f5def0c1e 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 e197c6022e3..ea5f1e87083 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 45a8b5cedfe..64cb0561e3d 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 73480cad4b4..0fc8505a9cb 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 db21589465e..9d2637332c5 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 8593d35f19e..0689a7ad77e 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 79ad3f1217d..89d24e2e779 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 a0213cec72c..3e570d9f81a 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 1ec1cb7a192..e1d3bc04778 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 950859d1eaf..71e2360ac5a 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 149da154881..bf0031759ed 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 8aefc4fd98c..53bf993a47d 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 4eeae11615e..04658f22df6 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 ca1f6948c8c..b60fff40921 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 8631bac1a91..206f13db72d 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 977c1d8bd81..e5f21cbff98 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 e0aeb721577..d6430a3fbe8 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 756eb763dec..da7c593b6d4 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 067c06eccce..3ee0122c70c 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 4011b122852..b8f3733090f 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 0fdce9fb33a..3a693eaf5e0 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 2babde48823..1bc898c25c0 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 12104c4bdef..d34cf635592 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 a6e524c185a..fec83a32018 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 92e9eae8623..fa12c25015d 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 22dee44ab67..2d4c02df7fd 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 d8990e91fe8..90a50a2466f 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 4a085639a73..2627fa4a0d0 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 3d4aafcb3df..f10250adbf6 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 6fd30db228c..b6193f2e7cb 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 73b9136aaeb..d743317918f 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 fbb07d32de7..4bbf0549d45 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 4cd9a752f63..8bc3b1e0130 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 4d802a2e21f..99fc52196db 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 947a12779b3..23965d520af 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 22c2d889f6f..8c67f9ecb9a 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 91f427c418a..d7c500f9e88 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 0975c8d7ac3..2c999da3807 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 9f8889bd5ea..ec296b2176c 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 e97a6b12c41..00f10b12feb 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 d81efb4581c..c6f1672d747 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 6af27adb74e..6dbd47dda1e 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 49421fb439d..15310e42407 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 654abefe17c..a92606a7d08 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 ab80c7dd6e9..c4bdd2154f0 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 772bc8febfe..f359000e1da 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 811c2e2aab3..1024210e08b 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 314ae5011dc..aed57385ef1 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 bb275d0f58e..ae0025dcf59 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 ad99002599a..6cbf2b79574 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 c0a47dde9cb..9f3e2669776 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 35ab96dfeb3..9023a07cc40 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 22080944a57..1f7fc0fd61a 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 d5f5f4ce22b..9dca47d019a 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 169d01c1e15..09eb04b451d 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 8681b37b32f..31245d0b6bb 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 9755efc5b79..311feffbd22 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 b5fdb9c5f5e..833ab0b10d2 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 0d138553af2..d62bc249b0c 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 517a681f898..77ec420b6db 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 57328a6d008..8439712e5ec 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 2e13ea17ffb..ecf415a0419 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 6ed25cd75c0..627e966fbcf 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 63fa35e84af..a918492e876 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 0a66f40d06b..111792a370a 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 bed88d3c68b..5c3b31d7d66 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 372e97df973..dd0a0b80648 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 edc652bdfa8..7f77298b2c5 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 61ac0c1a130..6ef9e065ba1 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 062ebd88ed9..18bc1674b9f 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 2b5f387aadf..0d7d4f44560 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 8d0c79e79bb..1368722e6e1 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 dd3cf14a905..e74eab5d577 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 3a9ec831e58..43171db27d4 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 e2586250af0..3e0707605be 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 6120492db89..9d3f47cbb6d 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 5ab161b003b..2c39d6ca4b3 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 f28f1d5b3fd..7160d5e230a 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 bfb137b9cec..cbacc607981 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 ca5b5191763..972d9c13d13 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 1a21b458057..d4a8e7179cd 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 bb5d0143c96..76a1b56dfe3 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 21c15b3113c..7b2aca52de5 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;
--
GitLab