Skip to content

Commit

Permalink
Fix misspellings in messages, man pages, and comments
Browse files Browse the repository at this point in the history
This is a manual, partial merge of Github pull request AbsInt#296 by @Fourchaux.
flocq/, cparser/MenhirLib/ and parts of test/ have not been changed
because these are local copies and the fixes should be performed upstream.
  • Loading branch information
xavierleroy committed May 31, 2019
1 parent e105553 commit 8b0724f
Show file tree
Hide file tree
Showing 21 changed files with 31 additions and 31 deletions.
2 changes: 1 addition & 1 deletion backend/Allocation.v
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ Require Import Op Registers RTL Locations Conventions RTLtyping LTL.
- a [Lbranch s] instruction.
The [block_shape] type below describes all possible cases of structural
maching between an RTL instruction and an LTL basic block.
matching between an RTL instruction and an LTL basic block.
*)

Inductive move: Type :=
Expand Down
4 changes: 2 additions & 2 deletions backend/Asmexpandaux.mli
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ val emit: instruction -> unit
val new_label: unit -> label
(* Compute a fresh label *)
val is_current_function_variadic: unit -> bool
(* Test wether the current function is a variadic function *)
(* Test whether the current function is a variadic function *)
val get_current_function_args: unit -> typ list
(* Get the types of the current function arguments *)
val get_current_function_sig: unit -> signature
Expand All @@ -33,4 +33,4 @@ val get_current_function: unit -> coq_function
(* Get the current function *)
val expand: positive -> int -> (preg -> int) -> (instruction -> unit) -> instruction list -> unit
(* Expand the instruction sequence of a function. Takes the function id, the register number of the stackpointer, a
function to get the dwarf mapping of varibale names and for the expansion of simple instructions *)
function to get the dwarf mapping of variable names and for the expansion of simple instructions *)
2 changes: 1 addition & 1 deletion backend/Inliningproof.v
Original file line number Diff line number Diff line change
Expand Up @@ -1249,7 +1249,7 @@ Proof.
eapply external_call_nextblock; eauto.
auto. auto.

- (* return fron noninlined function *)
- (* return from noninlined function *)
inv MS0.
+ (* normal case *)
left; econstructor; split.
Expand Down
2 changes: 1 addition & 1 deletion backend/Unusedglob.v
Original file line number Diff line number Diff line change
Expand Up @@ -107,7 +107,7 @@ Definition used_globals (p: program) (pm: prog_map) : option IS.t :=

(** * Elimination of unreferenced global definitions *)

(** We also eliminate multiple definitions of the same global name, keeping ony
(** We also eliminate multiple definitions of the same global name, keeping only
the last definition (in program definition order). *)

Fixpoint filter_globdefs (used: IS.t) (accu defs: list (ident * globdef fundef unit)) :=
Expand Down
2 changes: 1 addition & 1 deletion cfrontend/C2C.ml
Original file line number Diff line number Diff line change
Expand Up @@ -109,7 +109,7 @@ let atom_location a =

let comp_env : composite_env ref = ref Maps.PTree.empty

(** Hooks -- overriden in machine-dependent CPragmas module *)
(** Hooks -- overridden in machine-dependent CPragmas module *)

let process_pragma_hook = ref (fun (_: string) -> false)

Expand Down
2 changes: 1 addition & 1 deletion cfrontend/Clight.v
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ Definition typeof (e: expr) : type :=
(** ** Statements *)

(** Clight statements are similar to those of Compcert C, with the addition
of assigment (of a rvalue to a lvalue), assignment to a temporary,
of assignment (of a rvalue to a lvalue), assignment to a temporary,
and function call (with assignment of the result to a temporary).
The three C loops are replaced by a single infinite loop [Sloop s1
s2] that executes [s1] then [s2] repeatedly. A [continue] in [s1]
Expand Down
4 changes: 2 additions & 2 deletions common/AST.v
Original file line number Diff line number Diff line change
Expand Up @@ -432,12 +432,12 @@ Inductive external_function : Type :=
(** A function from the run-time library. Behaves like an
external, but must not be redefined. *)
| EF_vload (chunk: memory_chunk)
(** A volatile read operation. If the adress given as first argument
(** A volatile read operation. If the address given as first argument
points within a volatile global variable, generate an
event and return the value found in this event. Otherwise,
produce no event and behave like a regular memory load. *)
| EF_vstore (chunk: memory_chunk)
(** A volatile store operation. If the adress given as first argument
(** A volatile store operation. If the address given as first argument
points within a volatile global variable, generate an event.
Otherwise, produce no event and behave like a regular memory store. *)
| EF_malloc
Expand Down
2 changes: 1 addition & 1 deletion cparser/Cutil.ml
Original file line number Diff line number Diff line change
Expand Up @@ -947,7 +947,7 @@ let binary_conversion env t1 t2 =
end
| _, _ -> assert false

(* Conversion on function arguments (with protoypes) *)
(* Conversion on function arguments (with prototypes) *)

let argument_conversion env t =
(* Arrays and functions degrade automatically to pointers *)
Expand Down
2 changes: 1 addition & 1 deletion cparser/Diagnostics.ml
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ let max_error = ref 0
let diagnostics_show_option = ref true

(* Test if color diagnostics are available by testing if stderr is a tty
and if the environment varibale TERM is set
and if the environment variable TERM is set
*)
let color_diagnostics =
let term = try Sys.getenv "TERM" with Not_found -> "" in
Expand Down
8 changes: 4 additions & 4 deletions cparser/Diagnostics.mli
Original file line number Diff line number Diff line change
Expand Up @@ -22,22 +22,22 @@ exception Abort
(** Exception raised upon fatal errors *)

val check_errors : unit -> unit
(** Check whether errors occured and raise abort if an error occured *)
(** Check whether errors occurred and raise abort if an error occurred *)

type warning_type =
| Unnamed (** warnings which cannot be turned off *)
| Unknown_attribute (** usage of unsupported/unknown attributes *)
| Zero_length_array (** gnu extension for zero lenght arrays *)
| Zero_length_array (** gnu extension for zero length arrays *)
| Celeven_extension (** C11 features *)
| Gnu_empty_struct (** gnu extension for empty struct *)
| Missing_declarations (** declation which do not declare anything *)
| Missing_declarations (** declaration which do not declare anything *)
| Constant_conversion (** dangerous constant conversions *)
| Int_conversion (** pointer <-> int conversions *)
| Varargs (** promotable vararg argument *)
| Implicit_function_declaration (** deprecated implicit function declaration *)
| Pointer_type_mismatch (** pointer type mismatch in ?: operator *)
| Compare_distinct_pointer_types (** comparison between different pointer types *)
| Implicit_int (** implict int parameter or return type *)
| Implicit_int (** implicit int parameter or return type *)
| Main_return_type (** wrong return type for main *)
| Invalid_noreturn (** noreturn function containing return *)
| Return_type (** void return in non-void function *)
Expand Down
2 changes: 1 addition & 1 deletion cparser/Elab.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2632,7 +2632,7 @@ let elab_fundef genv spec name defs body loc =
For prototyped functions this has been done by [elab_fundef_name]
already, but some parameter may have been shadowed by the
function name, while it should be the other way around, e.g.
[int f(int f) { return f+1; }], with [f] refering to the
[int f(int f) { return f+1; }], with [f] referring to the
parameter [f] and not to the function [f] within the body of the
function. *)
let lenv =
Expand Down
4 changes: 2 additions & 2 deletions cparser/handcrafted.messages
Original file line number Diff line number Diff line change
Expand Up @@ -4477,7 +4477,7 @@ translation_unit_file: VOID PRE_NAME TYPEDEF_NAME PACKED LPAREN CONSTANT RPAREN
##

# We have just parsed a list of attribute specifiers, but we cannot
# print it because it is not available. We do not know wether it is
# print it because it is not available. We do not know whether it is
# part of the declaration or whether it is part of the first K&R parameter
# declaration.

Expand Down Expand Up @@ -4599,7 +4599,7 @@ translation_unit_file: PACKED LPAREN BUILTIN_OFFSETOF XOR_ASSIGN
##

Ill-formed __builtin_offsetof.
At this point, an opening paranthesis '(' is expected.
At this point, an opening parenthesis '(' is expected.

#------------------------------------------------------------------------------

Expand Down
4 changes: 2 additions & 2 deletions debug/DebugInformation.ml
Original file line number Diff line number Diff line change
Expand Up @@ -223,7 +223,7 @@ let name_to_definition: (string,int) Hashtbl.t = Hashtbl.create 7
(* Mapping from atom to debug id *)
let atom_to_definition: (atom, int) Hashtbl.t = Hashtbl.create 7

(* Various lookup functions for defintions *)
(* Various lookup functions for definitions *)
let find_gvar_stamp id =
let id = (Hashtbl.find stamp_to_definition id) in
let var = Hashtbl.find definitions id in
Expand Down Expand Up @@ -342,7 +342,7 @@ let insert_global_declaration env dec =
replace_var id ({var with gvar_declaration = false;})
end
end else begin
(* Implict declarations need special handling *)
(* Implicit declarations need special handling *)
let id' = try Hashtbl.find name_to_definition id.name with Not_found ->
let id' = next_id () in
Hashtbl.add name_to_definition id.name id';id' in
Expand Down
2 changes: 1 addition & 1 deletion debug/DwarfPrinter.ml
Original file line number Diff line number Diff line change
Expand Up @@ -241,7 +241,7 @@ module DwarfPrinter(Target: DWARF_TARGET):
let abbrev = !curr_abbrev in
incr curr_abbrev;abbrev

(* Mapping from abbreviation string to abbreviaton id *)
(* Mapping from abbreviation string to abbreviation id *)
let abbrev_mapping: (string,int) Hashtbl.t = Hashtbl.create 7

(* Mapping from abbreviation range id to label *)
Expand Down
2 changes: 1 addition & 1 deletion debug/Dwarfgen.ml
Original file line number Diff line number Diff line change
Expand Up @@ -595,7 +595,7 @@ let string_table: (string,int) Hashtbl.t = Hashtbl.create 7

let gnu_string_entry s =
if (String.length s < 4 && Configuration.system <> "macosx") (* macosx needs debug_str *)
|| Configuration.system = "cygwin" then (*Cygwin does not use the debug_str seciton*)
|| Configuration.system = "cygwin" then (*Cygwin does not use the debug_str section*)
Simple_string s
else
try
Expand Down
2 changes: 1 addition & 1 deletion doc/ccomp.1
Original file line number Diff line number Diff line change
Expand Up @@ -430,7 +430,7 @@ Wrong return type for main.
Enabled by default.
.sp
\fImissing\-declarations\fP:
Declations which do not declare anything.
Declarations which do not declare anything.
Enabled by default.
.sp
\fIpointer\-type\-mismatch\fP:
Expand Down
2 changes: 1 addition & 1 deletion driver/Commandline.mli
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ type action =
patterns are tried in the order in which they appear in the list. *)

exception CmdError of string
(** Raise by [parse_cmdline] when an error occured *)
(** Raise by [parse_cmdline] when an error occurred *)

val parse_cmdline: (pattern * action) list -> unit
(** [parse_cmdline actions] parses the command line (after @-file expansion)
Expand Down
4 changes: 2 additions & 2 deletions driver/Frontend.ml
Original file line number Diff line number Diff line change
Expand Up @@ -131,7 +131,7 @@ let gnu_prepro_opt_key key s =
let gnu_prepro_opt s =
prepro_options := s::!prepro_options

(* Add gnu preprocessor option s and the implict -E *)
(* Add gnu preprocessor option s and the implicit -E *)
let gnu_prepro_opt_e s =
prepro_options := s :: !prepro_options;
option_E := true
Expand Down Expand Up @@ -171,7 +171,7 @@ let prepro_actions = [
@ (if Configuration.gnu_toolchain then gnu_prepro_actions else [])

let gnu_prepro_help =
{| -M Ouput a rule suitable for make describing the
{| -M Output a rule suitable for make describing the
dependencies of the main source file
-MM Like -M but do not mention system header files
-MF <file> Specifies file <file> as output file for -M or -MM
Expand Down
2 changes: 1 addition & 1 deletion riscV/Asm.v
Original file line number Diff line number Diff line change
Expand Up @@ -369,7 +369,7 @@ lbl:
- [Ploadfi rd fval]: similar to [Ploadli] but loads a double FP constant fval
into a float register rd.
- [Ploadsi rd fval]: similar to [Ploadli] but loads a singe FP constant fval
- [Ploadsi rd fval]: similar to [Ploadli] but loads a single FP constant fval
into a float register rd.
- [Pallocframe sz pos]: in the formal semantics, this
Expand Down
6 changes: 3 additions & 3 deletions test/c/chomp.c
Original file line number Diff line number Diff line change
Expand Up @@ -106,7 +106,7 @@ void dump_play(struct _play *play) /* and for the entire game tree */
int get_value(int *data) /* get the value (0 or 1) for a specific _data */
{
struct _play *search;
search = game_tree; /* start at the begginig */
search = game_tree; /* start at the beginning */
while (! equal_data(search -> state,data)) /* until you find a match */
search = search -> next; /* take next element */
return search -> value; /* return its value */
Expand Down Expand Up @@ -138,7 +138,7 @@ void show_list(struct _list *list) /* show the entire list of moves */
}
}

void show_play(struct _play *play) /* to diplay the whole tree */
void show_play(struct _play *play) /* to display the whole tree */
{
while (play != NULL)
{
Expand All @@ -154,7 +154,7 @@ void show_play(struct _play *play) /* to diplay the whole tree */
int in_wanted(int *data) /* checks if the current _data is in the wanted list */
{
struct _list *current;
current = wanted; /* start at the begginig */
current = wanted; /* start at the beginning */
while (current != NULL) /* unitl the last one */
{
if (equal_data(current -> data,data)) break; /* break if found */
Expand Down
2 changes: 1 addition & 1 deletion x86/TargetPrinter.ml
Original file line number Diff line number Diff line change
Expand Up @@ -103,7 +103,7 @@ let rec log2 n =
assert (n > 0);
if n = 1 then 0 else 1 + log2 (n lsr 1)

(* System dependend printer functions *)
(* System dependent printer functions *)
module type SYSTEM =
sig
val raw_symbol: out_channel -> string -> unit
Expand Down

0 comments on commit 8b0724f

Please sign in to comment.