From d487ba080c2c17c7d1bb3c8f853857fa59f31c32 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 22 Nov 2018 12:50:01 +0000
Subject: [PATCH] Merge branch 'fix/andre/typos' into 'master'
fix several typos in comments
See merge request frama-c/e-acsl!270
(cherry picked from commit d8f5df30cd3ad9b43f2e3dfd717ff202ce261af3)
e41fc4c0 fix several typos in comments
---
src/plugins/e-acsl/E_ACSL.mli | 2 +-
src/plugins/e-acsl/doc/refman/changes_modern.tex | 2 +-
src/plugins/e-acsl/dup_functions.ml | 4 ++--
src/plugins/e-acsl/env.ml | 2 +-
src/plugins/e-acsl/interval.mli | 2 +-
src/plugins/e-acsl/label.ml | 2 +-
src/plugins/e-acsl/loops.mli | 2 +-
src/plugins/e-acsl/misc.ml | 2 +-
src/plugins/e-acsl/mmodel_translate.ml | 8 ++++----
src/plugins/e-acsl/prepare_ast.mli | 2 +-
src/plugins/e-acsl/temporal.mli | 2 +-
src/plugins/e-acsl/typing.mli | 8 ++++----
12 files changed, 19 insertions(+), 19 deletions(-)
diff --git a/src/plugins/e-acsl/E_ACSL.mli b/src/plugins/e-acsl/E_ACSL.mli
index 29aea1b1ba1..b889109f461 100644
--- a/src/plugins/e-acsl/E_ACSL.mli
+++ b/src/plugins/e-acsl/E_ACSL.mli
@@ -33,7 +33,7 @@ module Translate: sig
exception No_simple_translation of term
val term_to_exp: typ option -> term -> exp
(** @raise New_typing_error when the given term cannot be typed (something wrong
- happends with this term)
+ happened with this term)
@raise Not_yet when the given term contains an unsupported construct.
@raise No_simple_translation when the given term cannot be translated into
a single expression. *)
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index bbcf78dedeb..b482e45965e 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -16,7 +16,7 @@
\item \changeinsection{statement_contract}{fix syntax rule for statement
contracts in allowing completeness clauses}
\item \changeinsection{memory}{add syntax for defining a set by giving
- explicitely its element}
+ explicitly its element}
\item \changeinsection{typedpointers}{new section}
\end{itemize}
\end{itemize}
diff --git a/src/plugins/e-acsl/dup_functions.ml b/src/plugins/e-acsl/dup_functions.ml
index 45e382a42f8..a4a7c550087 100644
--- a/src/plugins/e-acsl/dup_functions.ml
+++ b/src/plugins/e-acsl/dup_functions.ml
@@ -121,7 +121,7 @@ let dup_fundec loc spec bhv kf vi new_vi =
let mk_formal vi =
let name =
if vi.vname = "" then
- (* unamed formal parameter: must generate a fresh name since a fundec
+ (* unnamed formal parameter: must generate a fresh name since a fundec
cannot have unnamed formals (see bts #2303). *)
Env.Varname.get ~scope:Env.Function
(Functions.RTL.mk_gen_name "unamed_formal")
@@ -219,7 +219,7 @@ class dup_functions_visitor prj = object (self)
val mutable before_memory_model = Before_gmp
val mutable new_definitions: global list = []
(* new definitions of the annotated functions which will contain the
- translation of the E-ACSL constract *)
+ translation of the E-ACSL contract *)
method private before_memory_model = match before_memory_model with
| Before_gmp | Gmp | After_gmp -> true
diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index 9c604d2135e..c23b7089391 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -483,7 +483,7 @@ let pop_and_get ?(split=false) env stmt ~global_clear where =
else
b
in
- (* remove superflous brackets inside the generated block *)
+ (* remove superfluous brackets inside the generated block *)
let final_blk = Cil.flatten_transient_sub_blocks final_blk in
(* remove the non-scoping mark of the outermost block *)
let final_blk = Cil.block_of_transient final_blk in
diff --git a/src/plugins/e-acsl/interval.mli b/src/plugins/e-acsl/interval.mli
index 958f24409dd..0a1e07d7b78 100644
--- a/src/plugins/e-acsl/interval.mli
+++ b/src/plugins/e-acsl/interval.mli
@@ -23,7 +23,7 @@
(** Interval inference for terms.
Compute the smallest interval that contains all the possible values of a
- given integer term. The interval of C variables is directly infered from
+ given integer term. The interval of C variables is directly inferred from
their C type. The interval of logic variables must be registered from
outside before computing the interval of a term containing such variables
(see module {!Interval.Env}).
diff --git a/src/plugins/e-acsl/label.ml b/src/plugins/e-acsl/label.ml
index d8c90534dff..e3b74c7e0d8 100644
--- a/src/plugins/e-acsl/label.ml
+++ b/src/plugins/e-acsl/label.ml
@@ -58,7 +58,7 @@ let move (vis:Visitor.generic_frama_c_visitor) ~old new_stmt =
s_ref := new_stmt;
Cil.SkipChildren
| _ -> Cil.DoChildren
- (* improve efficiency: skip childrens which cannot contain any label *)
+ (* improve efficiency: skip children which cannot contain any label *)
method !vinst _ = Cil.SkipChildren
method !vexpr _ = Cil.SkipChildren
method !vlval _ = Cil.SkipChildren
diff --git a/src/plugins/e-acsl/loops.mli b/src/plugins/e-acsl/loops.mli
index 27a0596d6be..ed7dd9c4860 100644
--- a/src/plugins/e-acsl/loops.mli
+++ b/src/plugins/e-acsl/loops.mli
@@ -37,7 +37,7 @@ val mv_invariants: Env.t -> old:stmt -> stmt -> unit
val preserve_invariant:
Project.t -> Env.t -> Kernel_function.t -> stmt -> stmt * Env.t * bool
(** modify the given stmt loop to insert the code which preserves its loop
- invarariants. Also return the modify environment and a boolean which
+ invariants. Also return the modify environment and a boolean which
indicates whether the annotations corresponding to the loop invariant must
be moved from the new statement to the old one. *)
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index ee27e0f4521..e346f67efef 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -56,7 +56,7 @@ let get_lib_fun_vi fname =
with Not_found ->
try Builtins.find fname
with Not_found ->
- (* could not happen in normal mode, but coud be raised when E-ACSL is
+ (* could not happen in normal mode, but could be raised when E-ACSL is
used as a library *)
raise (Unregistered_library_function fname)
diff --git a/src/plugins/e-acsl/mmodel_translate.ml b/src/plugins/e-acsl/mmodel_translate.ml
index d4f5ff13979..5880b8b8024 100644
--- a/src/plugins/e-acsl/mmodel_translate.ml
+++ b/src/plugins/e-acsl/mmodel_translate.ml
@@ -45,7 +45,7 @@ let term_to_exp_ref
[\forall integer q1; n-1 <= q1 <= n+2 ==>
\forall integer q2; 0 <= q2 <= 1 ==>
\valid(&t[q1][1][q2])]
- However, the substition can be unsound,
+ However, the substitution can be unsound,
in which case [Range_elimination_exception] must be raised.
Example:
[\valid(&t[(0..2)==(0..2) ? 0 : 1])] is equivalent to [\valid(&t[0])]
@@ -134,7 +134,7 @@ let call ~loc kf name ctx env t =
(********************** \initialized, \valid, \valid_read ********************)
(*****************************************************************************)
-(* Take the term [size] thas has been typed into GMP
+(* Take the term [size] that has been typed into GMP
and return an expression of type [size_t].
The case where [!(0 <= size < SIZE_MAX)] is an UB ==> guard against it. *)
let gmp_to_sizet ~loc kf env size p =
@@ -256,7 +256,7 @@ let call_memory_block ~loc kf name ctx env ptr r p =
The generated code is a SET OF calls to the corresponding E-ACSL builtin
C: Any other use of ranges/No range
Call [call_default] which performs the translation for
- range free terms, and raises Not_yet if it ever encouters a range.
+ range free terms, and raises Not_yet if it ever encounters a range.
Example for case:
A: [\valid(&t[3..5])]
Contiguous locations -> a single call to [__e_acsl_valid]
@@ -393,4 +393,4 @@ let call_valid ~loc kf name ctx env t p =
env
t
p
- call_for_unsupported_constructs
\ No newline at end of file
+ call_for_unsupported_constructs
diff --git a/src/plugins/e-acsl/prepare_ast.mli b/src/plugins/e-acsl/prepare_ast.mli
index c2db62e1ea8..9ba5b76b9a9 100644
--- a/src/plugins/e-acsl/prepare_ast.mli
+++ b/src/plugins/e-acsl/prepare_ast.mli
@@ -22,7 +22,7 @@
(** Prepare AST for E-ACSL generation.
- So for this mudule performs two tasks:
+ So for this module performs two tasks:
- move declarations of variables declared in the bodies of switch
statements to upper scopes;
- store what is necessary to translate in [Keep_status]. *)
diff --git a/src/plugins/e-acsl/temporal.mli b/src/plugins/e-acsl/temporal.mli
index bd2e1606a1e..17b419e08d9 100644
--- a/src/plugins/e-acsl/temporal.mli
+++ b/src/plugins/e-acsl/temporal.mli
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-(** Transformations to detect temporal memory errors (e.g., derererence of
+(** Transformations to detect temporal memory errors (e.g., dereference of
stale pointers). *)
val enable: bool -> unit
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index 4195ec14f10..8182360e77e 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -50,7 +50,7 @@ open Cil_types
(** {2 Datatypes} *)
(******************************************************************************)
-(** Possible types infered by the system. *)
+(** Possible types inferred by the system. *)
type integer_ty = private
| Gmp
| C_type of ikind
@@ -105,15 +105,15 @@ val clear: unit -> unit
predicate. *)
val get_integer_ty: term -> integer_ty
-(** @return the infered type for the given term. *)
+(** @return the inferred type for the given term. *)
val get_integer_op: term -> integer_ty
-(** @return the infered type for the top operation of the given term.
+(** @return the inferred type for the top operation of the given term.
It is meaningless to call this function over a non-arithmetical/logical
operator. *)
val get_integer_op_of_predicate: predicate -> integer_ty
-(** @return the infered type for the top operation of the given predicate. *)
+(** @return the inferred type for the top operation of the given predicate. *)
val get_typ: term -> typ
(** Get the type which the given term must be generated to. *)
--
GitLab