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

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 <dir>    Install in <dir>/bin and <dir>/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-<opt> to turn off -f<opt>) :
   -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-<opt> to turn off -f<opt>) :
   -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 <n>  Set maximal size <n> for allocation in small data area
   -fsmall-const <n>  Set maximal size <n> for allocation in small constant area
   -ffloat-const-prop <n>  Control constant propagation of floats
@@ -439,9 +440,11 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>) :
   -falign-functions <n>  Set alignment (in bytes) of function entry points
   -falign-branch-targets <n>  Set alignment (in bytes) of branch targets
   -falign-cond-branches <n>  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,<opt>      Pass option <opt> to the assembler
-Debugging options:
-  -g             Generate debugging information
 Linking options:
   -l<lib>        Link library <lib>
   -L<dir>        Add <dir> 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".