aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2022-12-08 16:05:16 +0100
committerXavier Leroy <xavier.leroy@college-de-france.fr>2022-12-08 16:05:16 +0100
commit8d21a7fa245637b684ddb4c12f4bfa6295569fb6 (patch)
treeb1dc2549f9c9dc8e12a5c3679d584a1e5d8dfc10
parente5d132537bd2dbbf9c3d4b313c6b312b62ac133e (diff)
downloadcompcert-8d21a7fa245637b684ddb4c12f4bfa6295569fb6.tar.gz
compcert-8d21a7fa245637b684ddb4c12f4bfa6295569fb6.zip
Remove support for 32-bit Cygwin
Cygwin 32 bits has reached end of life, and Cygwin >= 3.4 will be 64-bit only. (https://cygwin.com/pipermail/cygwin-announce/2022-November/010777.html)
-rwxr-xr-xconfigure9
-rw-r--r--x86/TargetPrinter.ml21
2 files changed, 7 insertions, 23 deletions
diff --git a/configure b/configure
index df132dcf..0081b770 100755
--- a/configure
+++ b/configure
@@ -52,7 +52,6 @@ Supported targets:
armeb-hardfloat (ARM, EABI using hardware FP registers, big endian)
x86_32-linux (x86 32 bits, Linux)
x86_32-bsd (x86 32 bits, BSD)
- x86_32-cygwin (x86 32 bits, Cygwin environment under Windows)
x86_64-linux (x86 64 bits, Linux)
x86_64-bsd (x86 64 bits, BSD)
x86_64-macos (x86 64 bits, MacOS X)
@@ -318,14 +317,6 @@ if test "$arch" = "x86" -a "$bitsize" = "32"; then
cprepro_options="-m32 -U__GNUC__ -E"
system="bsd"
;;
- cygwin)
- abi="standard"
- cc_options="-m32"
- casm_options="-m32 -c"
- clinker_options="-m32"
- cprepro_options="-m32 -U__GNUC__ '-D__attribute__(x)=' -E"
- system="cygwin"
- ;;
linux)
abi="standard"
cc_options="-m32"
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index f529a89d..a289127a 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -254,8 +254,7 @@ module Cygwin_System : SYSTEM =
(* The comment delimiter *)
let comment = "#"
- let symbol_prefix =
- if Archi.ptr64 then "" else "_"
+ let symbol_prefix = ""
let raw_symbol oc s =
fprintf oc "%s%s" symbol_prefix s
@@ -287,7 +286,6 @@ module Cygwin_System : SYSTEM =
| Section_ais_annotation -> assert false (* Not supported for coff binaries *)
let stack_alignment = 8
- (* minimum is 4 for 32 bits, 8 for 64 bits; 8 is better for perfs *)
let print_align oc n =
fprintf oc " .balign %d\n" n
@@ -295,13 +293,10 @@ module Cygwin_System : SYSTEM =
let indirect_symbols : StringSet.t ref = ref StringSet.empty
let print_mov_rs oc rd id =
- if Archi.ptr64 then begin
- let s = extern_atom id in
- indirect_symbols := StringSet.add s !indirect_symbols;
- fprintf oc " movq .refptr.%s(%%rip), %a\n" s ireg rd
- end else begin
- fprintf oc " movl $%a, %a\n" symbol id ireg rd
- end
+ assert Archi.ptr64;
+ let s = extern_atom id in
+ indirect_symbols := StringSet.add s !indirect_symbols;
+ fprintf oc " movq .refptr.%s(%%rip), %a\n" s ireg rd
let print_fun_info _ _ = ()
@@ -315,10 +310,8 @@ module Cygwin_System : SYSTEM =
fprintf oc " .quad %s\n" s
let print_epilogue oc =
- if Archi.ptr64 then begin
- StringSet.iter (declare_indirect_symbol oc) !indirect_symbols;
- indirect_symbols := StringSet.empty
- end
+ StringSet.iter (declare_indirect_symbol oc) !indirect_symbols;
+ indirect_symbols := StringSet.empty
let print_comm_decl oc name sz al =
fprintf oc " .comm %a, %s, %d\n"