File tree 13 files changed +98
-99
lines changed
13 files changed +98
-99
lines changed Original file line number Diff line number Diff line change @@ -644,7 +644,7 @@ let add_interfs_instr g instr live =
644
644
(* Reloads from incoming slots can occur when some 64-bit
645
645
parameters are split and passed as two 32-bit stack locations. *)
646
646
begin match src with
647
- | L (Locations. S(Incoming, _ , _ )) ->
647
+ | L (Locations. S(Incoming, _ , _ )) ->
648
648
add_interfs_def g (vmreg temp_for_parent_frame) live
649
649
| _ -> ()
650
650
end
@@ -1210,9 +1210,9 @@ let regalloc f =
1210
1210
Errors. OK (first_round f3 liveness)
1211
1211
with
1212
1212
| Timeout ->
1213
- Errors. Error (Errors. msg (coqstring_of_camlstring " Spilling fails to converge" ))
1213
+ Errors. Error (Errors. msg (coqstring_of_camlstring " spilling fails to converge" ))
1214
1214
| Type_error_at pc ->
1215
- Errors. Error [Errors. MSG (coqstring_of_camlstring " Ill -typed XTL code at PC " );
1215
+ Errors. Error [Errors. MSG (coqstring_of_camlstring " ill -typed XTL code at PC " );
1216
1216
Errors. POS pc]
1217
1217
| Bad_LTL ->
1218
- Errors. Error (Errors. msg (coqstring_of_camlstring " Bad LTL after spilling" ))
1218
+ Errors. Error (Errors. msg (coqstring_of_camlstring " bad LTL after spilling" ))
Load Diff Large diffs are not rendered by default.
Original file line number Diff line number Diff line change @@ -21,7 +21,7 @@ open Pre_parser_aux
21
21
module SSet = Set. Make (String )
22
22
23
23
let lexicon : (string, Cabs.cabsloc -> token) Hashtbl.t = Hashtbl. create 17
24
- let ignored_keyworkds : SSet.t ref = ref SSet. empty
24
+ let ignored_keywords : SSet.t ref = ref SSet. empty
25
25
26
26
let () =
27
27
List. iter (fun (key , builder ) -> Hashtbl. add lexicon key builder)
@@ -85,7 +85,7 @@ let () =
85
85
(" while" , fun loc -> WHILE loc)];
86
86
if Configuration. system <> " diab" then
87
87
(* We can ignore the __extension__ GCC keyword. *)
88
- ignored_keyworkds := SSet. add " __extension__" ! ignored_keyworkds
88
+ ignored_keywords := SSet. add " __extension__" ! ignored_keywords
89
89
90
90
let init_ctx = SSet. singleton " __builtin_va_list"
91
91
let types_context : SSet.t ref = ref init_ctx
@@ -329,7 +329,7 @@ rule initial = parse
329
329
| " ," { COMMA (currentLoc lexbuf) }
330
330
| " ." { DOT (currentLoc lexbuf) }
331
331
| identifier as id {
332
- if SSet. mem id ! ignored_keyworkds then
332
+ if SSet. mem id ! ignored_keywords then
333
333
initial lexbuf
334
334
else
335
335
try Hashtbl. find lexicon id (currentLoc lexbuf)
Original file line number Diff line number Diff line change @@ -69,7 +69,7 @@ let preprocessed_file transfs name sourcefile =
69
69
| Parser.Parser.Inter. Fail_pr ->
70
70
(* Theoretically impossible : implies inconsistencies
71
71
between grammars. *)
72
- Diagnostics. fatal_error Diagnostics. no_loc " Internal error while parsing"
72
+ Diagnostics. fatal_error Diagnostics. no_loc " internal error while parsing"
73
73
| Parser.Parser.Inter. Timeout_pr -> assert false
74
74
| Parser.Parser.Inter. Parsed_pr (ast , _ ) -> ast) in
75
75
let p1 = Timing. time " Elaboration" Elab. elab_file ast in
Original file line number Diff line number Diff line change @@ -31,7 +31,7 @@ let rec local_initializer env path init k =
31
31
let (ty_elt, sz) =
32
32
match unroll env path.etyp with
33
33
| TArray (ty_elt , Some sz , _ ) -> (ty_elt, sz)
34
- | _ -> Diagnostics. fatal_error Diagnostics. no_loc " Wrong type for array initializer" in
34
+ | _ -> Diagnostics. fatal_error Diagnostics. no_loc " wrong type for array initializer" in
35
35
let rec array_init pos il =
36
36
if pos > = sz then k else begin
37
37
let (i1, il') =
Original file line number Diff line number Diff line change @@ -241,7 +241,7 @@ module DwarfPrinter(Target: DWARF_TARGET):
241
241
let abbrev = ! curr_abbrev in
242
242
incr curr_abbrev;abbrev
243
243
244
- (* Mapping from abbreviation string to abbrevaiton id *)
244
+ (* Mapping from abbreviation string to abbreviaton id *)
245
245
let abbrev_mapping: (string ,int ) Hashtbl. t = Hashtbl. create 7
246
246
247
247
(* Look up the id of the abbreviation and add it if it is missing *)
Original file line number Diff line number Diff line change @@ -15,7 +15,7 @@ val assemble: string -> string -> unit
15
15
(* * From asm to object file *)
16
16
17
17
val assembler_actions : (Commandline .pattern * Commandline .action ) list
18
- (* * Commandline optins affecting the assembler *)
18
+ (* * Commandline options affecting the assembler *)
19
19
20
20
val assembler_help : string
21
21
(* * Commandline help description *)
Original file line number Diff line number Diff line change @@ -74,7 +74,7 @@ let parse_array spec argv first last =
74
74
with Not_found -> find_action s inexact_cases in
75
75
match optact with
76
76
| None ->
77
- let msg = sprintf " Unknown argument `%s'" s in
77
+ let msg = sprintf " unknown argument `%s'" s in
78
78
raise (CmdError msg)
79
79
| Some (Set r ) ->
80
80
r := true ; parse (i+ 1 )
@@ -86,7 +86,7 @@ let parse_array spec argv first last =
86
86
if i + 1 < = last then begin
87
87
fn argv.(i+ 1 ); parse (i+ 2 )
88
88
end else begin
89
- let msg = sprintf " Option `%s' expects an argument" s in
89
+ let msg = sprintf " option `%s' expects an argument" s in
90
90
raise (CmdError msg)
91
91
end
92
92
| Some (Integer fn ) ->
@@ -95,19 +95,19 @@ let parse_array spec argv first last =
95
95
try
96
96
int_of_string argv.(i+ 1 )
97
97
with Failure _ ->
98
- let msg = sprintf " Argument to option `%s' must be an integer" s in
98
+ let msg = sprintf " argument to option `%s' must be an integer" s in
99
99
raise (CmdError msg)
100
100
in
101
101
fn n; parse (i+ 2 )
102
102
end else begin
103
- let msg = sprintf " Option `%s' expects an argument" s in
103
+ let msg = sprintf " option `%s' expects an argument" s in
104
104
raise (CmdError msg)
105
105
end
106
106
| Some (Ignore) ->
107
107
if i + 1 < = last then begin
108
108
parse (i+ 2 )
109
109
end else begin
110
- let msg = sprintf " Option `%s' expects an argument" s in
110
+ let msg = sprintf " option `%s' expects an argument" s in
111
111
raise (CmdError msg)
112
112
end
113
113
| Some (Unit f ) -> f () ; parse (i+ 1 )
@@ -131,7 +131,7 @@ let long_int_action key s =
131
131
try
132
132
int_of_string s
133
133
with Failure _ ->
134
- let msg = sprintf " Argument to option `%s' must be an integer" key in
134
+ let msg = sprintf " argument to option `%s' must be an integer" key in
135
135
raise (CmdError msg)
136
136
137
137
let longopt_int key f =
Original file line number Diff line number Diff line change @@ -404,7 +404,7 @@ let _ =
404
404
parse_cmdline cmdline_actions;
405
405
DebugInit. init () ; (* Initialize the debug functions *)
406
406
if nolink () && ! option_o <> None && ! num_source_files > = 2 then
407
- fatal_error no_loc " Ambiguous '-o' option (multiple source files)" ;
407
+ fatal_error no_loc " ambiguous '-o' option (multiple source files)" ;
408
408
if ! num_input_files = 0 then
409
409
fatal_error no_loc " no input file" ;
410
410
let linker_args = time " Total compilation time" perform_actions () in
Original file line number Diff line number Diff line change @@ -47,7 +47,7 @@ let command stdout args =
47
47
match status with
48
48
| Unix. WEXITED rc -> rc
49
49
| Unix. WSIGNALED n | Unix. WSTOPPED n ->
50
- error no_loc " Command '%s' killed on a signal." argv.(0 ); - 1
50
+ error no_loc " command '%s' killed on a signal." argv.(0 ); - 1
51
51
with Unix. Unix_error (err , fn , param ) ->
52
52
error no_loc " executing '%s': %s: %s %s"
53
53
argv.(0 ) fn (Unix. error_message err) param;
Original file line number Diff line number Diff line change @@ -18,7 +18,7 @@ val parse_c_file: string -> string -> Csyntax.coq_function Ctypes.program
18
18
(* * From preprocessed C to Csyntax *)
19
19
20
20
val prepro_actions : (Commandline .pattern * Commandline .action ) list
21
- (* * Commandline optins affecting the frontend *)
21
+ (* * Commandline options affecting the frontend *)
22
22
23
23
val prepro_help : string
24
24
(* * Commandline help description *)
Original file line number Diff line number Diff line change 12
12
(* *********************************************************************)
13
13
14
14
val linker : string -> string list -> unit
15
- (* * Link files into executbale *)
15
+ (* * Link files into executable *)
16
16
17
17
val linker_actions : (Commandline .pattern * Commandline .action ) list
18
- (* * Commandline optins affecting the assembler *)
18
+ (* * Commandline options affecting the assembler *)
19
19
20
20
val linker_help : string
21
21
(* * Commandline help description *)
Original file line number Diff line number Diff line change @@ -43,9 +43,9 @@ let error msg lexbuf =
43
43
lexbuf.lex_curr_p.pos_lnum,
44
44
msg)))
45
45
46
- let ill_formed_line lexbuf = error " Ill -formed line" lexbuf
47
- let unterminated_quote lexbuf = error " Unterminated quote" lexbuf
48
- let lone_backslash lexbuf = error " Lone \\ (backslash) at end of file" lexbuf
46
+ let ill_formed_line lexbuf = error " ill -formed line" lexbuf
47
+ let unterminated_quote lexbuf = error " unterminated quote" lexbuf
48
+ let lone_backslash lexbuf = error " lone \\ (backslash) at end of file" lexbuf
49
49
50
50
}
51
51
You can’t perform that action at this time.
0 commit comments