diff options
Diffstat (limited to 'driver')
-rw-r--r-- | driver/Clflags.ml | 2 | ||||
-rw-r--r-- | driver/Configuration.ml | 12 | ||||
-rw-r--r-- | driver/Configuration.mli | 2 | ||||
-rw-r--r-- | driver/Driver.ml | 8 | ||||
-rw-r--r-- | driver/Interp.ml | 12 |
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 |