Merge branch 'cherry-pick-d8f5df30' into 'stable/argon'

Merge branch 'fix/andre/typos' into 'master'

See merge request frama-c/e-acsl!272

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. *)

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}

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

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

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}).

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

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. *)
 

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)
 

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
+    call_for_unsupported_constructs
\ No newline at end of file

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]. *)

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

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. *)