From c58233b2820e6341a8077cf4bf6e3e5b15d1cbf5 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 19 Aug 2014 13:47:39 +0000 Subject: Rename "-fthumb" option into "-mthumb" for GCC compatibility. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2572 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/PrintAsm.ml | 16 ++++++++-------- configure | 8 ++++---- driver/Clflags.ml | 2 +- driver/Driver.ml | 12 ++++++++---- extraction/extraction.v | 2 +- 5 files changed, 22 insertions(+), 18 deletions(-) diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index e1988cc..530a8f7 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -26,7 +26,7 @@ let vfpv3 = Configuration.model >= "armv7" let hardware_idiv () = match Configuration.model with - | "armv7r" | "armv7m" -> !Clflags.option_fthumb + | "armv7r" | "armv7m" -> !Clflags.option_mthumb | _ -> false let literals_in_code = ref true (* to be turned into a proper option *) @@ -147,7 +147,7 @@ let neg_condition_name = function mode. *) let thumbS oc = - if !Clflags.option_fthumb then output_char oc 's' + if !Clflags.option_mthumb then output_char oc 's' (* Names of sections *) @@ -245,7 +245,7 @@ let emit_constants oc = (* Generate code to load the address of id + ofs in register r *) let loadsymbol oc r id ofs = - if !Clflags.option_fthumb then begin + if !Clflags.option_mthumb then begin fprintf oc " movw %a, #:lower16:%a\n" ireg r print_symb_ofs (id, ofs); fprintf oc " movt %a, #:upper16:%a\n" @@ -560,7 +560,7 @@ let print_builtin_inline oc name args res = (* No "rsc" instruction in Thumb2. Emulate based on rsc a, b, #0 == a <- AddWithCarry(~b, 0, carry) == mvn a, b; adc a, a, #0 *) - if !Clflags.option_fthumb then begin + if !Clflags.option_mthumb then begin fprintf oc " mvn %a, %a\n" ireg rh ireg ah; fprintf oc " adc %a, %a, #0\n" ireg rh ireg rh; 3 end else begin @@ -754,7 +754,7 @@ let print_instruction oc = function (* Core instructions *) | Padd(r1, r2, so) -> fprintf oc " add%s %a, %a, %a\n" - (if !Clflags.option_fthumb && r2 <> IR14 then "s" else "") + (if !Clflags.option_mthumb && r2 <> IR14 then "s" else "") ireg r1 ireg r2 shift_op so; 1 | Pand(r1, r2, so) -> fprintf oc " and%t %a, %a, %a\n" @@ -1003,7 +1003,7 @@ let print_instruction oc = function fprintf oc " mov%s %a, %a\n" (neg_condition_name cond) ireg r1 shift_op ifnot; 2 | Pbtbl(r, tbl) -> - if !Clflags.option_fthumb then begin + if !Clflags.option_mthumb then begin let lbl = new_label() in fprintf oc " adr r14, .L%d\n" lbl; fprintf oc " add r14, r14, %a, lsl #2\n" ireg r; @@ -1092,7 +1092,7 @@ let print_function oc name fn = fprintf oc " .balign %d\n" alignment; if not (C2C.atom_is_static name) then fprintf oc " .global %a\n" print_symb name; - if !Clflags.option_fthumb then + if !Clflags.option_mthumb then fprintf oc " .thumb_func\n"; fprintf oc "%a:\n" print_symb name; print_location oc (C2C.atom_location name); @@ -1193,7 +1193,7 @@ let print_program oc p = | _ -> "armv7"); fprintf oc " .fpu %s\n" (if vfpv3 then "vfpv3-d16" else "vfpv2"); - fprintf oc " .%s\n" (if !Clflags.option_fthumb then "thumb" else "arm"); + fprintf oc " .%s\n" (if !Clflags.option_mthumb then "thumb" else "arm"); List.iter (print_globdef oc) p.prog_defs diff --git a/configure b/configure index 603b30a..a47b59d 100755 --- a/configure +++ b/configure @@ -36,10 +36,10 @@ Supported targets: manual (edit configuration file by hand) For ARM targets, the "arm-" prefix can be refined into: - armv6- ARMv6 + VFPv2 - armv7a- ARMv7a + VFPv3-d16 (default) - armv7r- ARMv7r + VFPv3-d16 - armv7m- ARMv7m + VFPv3-d16 + armv6- ARMv6 + VFPv2 + armv7a- ARMv7-A + VFPv3-d16 (default) + armv7r- ARMv7-R + VFPv3-d16 + armv7m- ARMv7-M + VFPv3-d16 Options: -prefix Install in /bin and /lib/compcert diff --git a/driver/Clflags.ml b/driver/Clflags.ml index d3d4067..76c9892 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -28,7 +28,7 @@ let option_falignfunctions = ref (None: int option) let option_falignbranchtargets = ref 0 let option_faligncondbranchs = ref 0 let option_finline_asm = ref false -let option_fthumb = ref (Configuration.model = "armv7m") +let option_mthumb = ref (Configuration.model = "armv7m") let option_Osize = ref false let option_dparse = ref false let option_dcmedium = ref false diff --git a/driver/Driver.ml b/driver/Driver.ml index da2fa7c..ae39783 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -426,11 +426,12 @@ Language support options (use -fno- to turn off -f) : -finline-asm Support inline 'asm' statements [off] -fall Activate all language support options above -fnone Turn off all language support options above +Debugging options: + -g Generate debugging information Code generation options: (use -fno- to turn off -f) : -O Optimize for speed [on by default] -Os Optimize for code size -ffpu Use FP registers for some integer operations [on] - -fthumb (ARM only) Use Thumb2 instruction encoding -fsmall-data Set maximal size for allocation in small data area -fsmall-const Set maximal size for allocation in small constant area -ffloat-const-prop Control constant propagation of floats @@ -439,9 +440,11 @@ Code generation options: (use -fno- to turn off -f) : -falign-functions Set alignment (in bytes) of function entry points -falign-branch-targets Set alignment (in bytes) of branch targets -falign-cond-branches Set alignment (in bytes) of conditional branches +Target processor options: + -mthumb (ARM only) Use Thumb2 instruction encoding + -marm (ARM only) Use classic ARM instruction encoding +Assembling options: -Wa, Pass option to the assembler -Debugging options: - -g Generate debugging information Linking options: -l Link library -L Add to search path for libraries @@ -533,6 +536,8 @@ let cmdline_actions = "-Os$", Set option_Osize; "-O$", Unset option_Osize; "-timings$", Set option_timings; + "-mthumb$", Set option_mthumb; + "-marm$", Unset option_mthumb; "-fsmall-data$", Integer(fun n -> option_small_data := n); "-fsmall-const$", Integer(fun n -> option_small_const := n); "-ffloat-const-prop$", Integer(fun n -> option_ffloatconstprop := n); @@ -554,7 +559,6 @@ let cmdline_actions = @ f_opt "inline-asm" option_finline_asm @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) - @ f_opt "thumb" option_fthumb let _ = try diff --git a/extraction/extraction.v b/extraction/extraction.v index a097bdb..f5556fd 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -95,7 +95,7 @@ Extract Constant Compopts.generate_float_constants => Extract Constant Compopts.eliminate_tailcalls => "fun _ -> !Clflags.option_ftailcalls". Extract Constant Compopts.thumb => - "fun _ -> !Clflags.option_fthumb". + "fun _ -> !Clflags.option_mthumb". (* Compiler *) Extract Constant Compiler.print_Clight => "PrintClight.print_if". -- cgit v1.2.3