Commit 887bddc5 authored by Andre Maroneze's avatar Andre Maroneze
Browse files

fix several typos in comments

parent 6aba973b
......@@ -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. *)
......
......@@ -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}
......
......@@ -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
......
......@@ -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
......
......@@ -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}).
......
......@@ -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
......
......@@ -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. *)
......
......@@ -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)
......
......@@ -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
......@@ -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]. *)
......
......@@ -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
......
......@@ -205,7 +205,7 @@ let coerce ~arith_operand ~ctx ~op ty =
end else
(* only add an explicit cast if the context is [Gmp] and [ty] is not;
or if the term corresponding to [ty] is an operand of an arithmetic
operation which must be explicitely coerced in order to force the
operation which must be explicitly coerced in order to force the
operation to be of the expected type. *)
if (ctx = Gmp && ty <> Gmp) || arith_operand
then { ty; op; cast = Some ctx }
......@@ -340,7 +340,7 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
with Interval.Not_an_integer ->
dup Other (* real *)
in
(* it is enough to explicitely coerce when required one operand to [ctx]
(* it is enough to explicitly coerce when required one operand to [ctx]
(through [arith_operand]) in order to force the type of the operation.
Heuristic: coerce the operand which is not a lval in order to lower
the number of explicit casts *)
......
......@@ -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. *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment