aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authorMichael Schmidt <github@mschmidt.me>2015-10-14 15:07:48 +0200
committerMichael Schmidt <github@mschmidt.me>2015-10-14 15:07:48 +0200
commit60ab550a952c3d9719b2a91ec90c9b58769f6717 (patch)
tree523cf4eb5a35594b16a297b4bd7e29157f42b0fc /driver
parenta479c280441b91007c379b0b63b907926d54f930 (diff)
downloadcompcert-60ab550a952c3d9719b2a91ec90c9b58769f6717.tar.gz
compcert-60ab550a952c3d9719b2a91ec90c9b58769f6717.zip
bug 17392: remove trailing whitespace in source files
Diffstat (limited to 'driver')
-rw-r--r--driver/Clflags.ml2
-rw-r--r--driver/Configuration.ml12
-rw-r--r--driver/Configuration.mli2
-rw-r--r--driver/Driver.ml8
-rw-r--r--driver/Interp.ml12
5 files changed, 18 insertions, 18 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index d9c21a9c..9d3697bd 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -52,7 +52,7 @@ let option_S = ref false
let option_c = ref false
let option_v = ref false
let option_interp = ref false
-let option_small_data =
+let option_small_data =
ref (if Configuration.arch = "powerpc"
&& Configuration.abi = "eabi"
&& Configuration.system = "diab"
diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index 41325368..1f05afd8 100644
--- a/driver/Configuration.ml
+++ b/driver/Configuration.ml
@@ -30,7 +30,7 @@ let ini_file_name =
try
List.find Sys.file_exists files
with Not_found ->
- begin
+ begin
eprintf "Cannot find compcert.ini configuration file.\n";
exit 2
end
@@ -73,19 +73,19 @@ let get_config_list key =
let prepro = get_config_list "prepro"
let asm = get_config_list "asm"
let linker = get_config_list "linker"
-let arch =
+let arch =
match get_config_string "arch" with
| "powerpc"|"arm"|"ia32" as a -> a
| v -> bad_config "arch" [v]
let model = get_config_string "model"
let abi = get_config_string "abi"
let system = get_config_string "system"
-let has_runtime_lib =
+let has_runtime_lib =
match get_config_string "has_runtime_lib" with
| "true" -> true
| "false" -> false
| v -> bad_config "has_runtime_lib" [v]
-let has_standard_headers =
+let has_standard_headers =
match get_config_string "has_standard_headers" with
| "true" -> true
| "false" -> false
@@ -95,7 +95,7 @@ let stdlib_path =
get_config_string "stdlib_path"
else
""
-let asm_supports_cfi =
+let asm_supports_cfi =
match get_config_string "asm_supports_cfi" with
| "true" -> true
| "false" -> false
@@ -117,7 +117,7 @@ type struct_return_style =
| SR_int1248 (* return by content if size is 1, 2, 4 or 8 bytes *)
| SR_int1to4 (* return by content if size is <= 4 *)
| SR_int1to8 (* return by content if size is <= 8 *)
- | SR_ref (* always return by assignment to a reference
+ | SR_ref (* always return by assignment to a reference
given as extra argument *)
let struct_passing_style =
diff --git a/driver/Configuration.mli b/driver/Configuration.mli
index f82ce213..1d048ac4 100644
--- a/driver/Configuration.mli
+++ b/driver/Configuration.mli
@@ -46,7 +46,7 @@ type struct_return_style =
| SR_int1248 (* return by content if size is 1, 2, 4 or 8 bytes *)
| SR_int1to4 (* return by content if size is <= 4 *)
| SR_int1to8 (* return by content if size is <= 8 *)
- | SR_ref (* always return by assignment to a reference
+ | SR_ref (* always return by assignment to a reference
given as extra argument *)
val struct_passing_style: struct_passing_style
diff --git a/driver/Driver.ml b/driver/Driver.ml
index c7d9984e..4b58fb4d 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -188,7 +188,7 @@ let compile_c_ast sourcename csyntax ofile debug =
| Errors.Error msg ->
eprintf "%s: %a" sourcename print_error msg;
exit 2 in
- (* Dump Asm in binary and JSON format *)
+ (* Dump Asm in binary and JSON format *)
if !option_sdump then
begin
dump_asm asm (output_filename sourcename ".c" ".sdump");
@@ -518,7 +518,7 @@ let unset_all opts = List.iter (fun r -> r := false) opts
let num_source_files = ref 0
let num_input_files = ref 0
-
+
let cmdline_actions =
let f_opt name ref =
[Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in
@@ -570,8 +570,8 @@ let cmdline_actions =
(* Linking options *)
Prefix "-l", Self push_linker_arg;
Prefix "-L", Self push_linker_arg;
- Exact "-T", String (fun s -> if Configuration.system = "diab" then
- push_linker_arg ("-Wm"^s)
+ Exact "-T", String (fun s -> if Configuration.system = "diab" then
+ push_linker_arg ("-Wm"^s)
else begin
push_linker_arg ("-T");
push_linker_arg(s)
diff --git a/driver/Interp.ml b/driver/Interp.ml
index f453af95..b3bdc883 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -98,7 +98,7 @@ let name_of_function prog fn =
in find_name prog.prog_defs
let invert_local_variable e b =
- Maps.PTree.fold
+ Maps.PTree.fold
(fun res id (b', _) -> if b = b' then Some id else res)
e None
@@ -176,7 +176,7 @@ let rec compare_cont k1 k2 =
match k1, k2 with
| Kstop, Kstop -> 0
| Kdo k1, Kdo k2 -> compare_cont k1 k2
- | Kseq(s1, k1), Kseq(s2, k2) ->
+ | Kseq(s1, k1), Kseq(s2, k2) ->
let c = compare s1 s2 in if c <> 0 then c else compare_cont k1 k2
| Kifthenelse(s1, s1', k1), Kifthenelse(s2, s2', k2) ->
let c = compare (s1,s1') (s2,s2') in
@@ -273,7 +273,7 @@ let extract_string m blk ofs =
if c = '\000' then begin
Some(Buffer.contents b)
end else begin
- Buffer.add_char b c;
+ Buffer.add_char b c;
extract blk (Z.succ ofs)
end
| _ ->
@@ -325,7 +325,7 @@ let format_value m flags length conv arg =
| 'p', "", _ ->
"<int or pointer argument expected>"
| _, _, _ ->
- "<unrecognized format>"
+ "<unrecognized format>"
let do_printf m fmt args =
@@ -374,7 +374,7 @@ let convert_external_arg ge v t =
| Vfloat f, AST.Tfloat -> Some (EVfloat f)
| Vsingle f, AST.Tsingle -> Some (EVsingle f)
| Vlong n, AST.Tlong -> Some (EVlong n)
- | Vptr(b, ofs), AST.Tint ->
+ | Vptr(b, ofs), AST.Tint ->
Senv.invert_symbol ge b >>= fun id -> Some (EVptr_global(id, ofs))
| _, _ -> None
@@ -565,7 +565,7 @@ let rec explore_all p prog ge time states =
if nextstates <> [] then explore_all p prog ge (time + 1) nextstates
(* The variant of the source program used to build the world for
- executing events.
+ executing events.
Volatile variables are turned into non-volatile ones, so that
reads and writes can be performed.
Other variables are turned into empty vars, so that