aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile23
-rw-r--r--arm/PrintAsm.ml6
-rw-r--r--checklink/Check.ml11
-rw-r--r--common/Sections.ml12
-rw-r--r--common/Sections.mli4
-rw-r--r--driver/Configuration.ml9
-rw-r--r--ia32/PrintAsm.ml58
-rw-r--r--powerpc/PrintDiab.ml8
-rw-r--r--powerpc/PrintLinux.ml13
-rw-r--r--test/regression/decl1.c2
10 files changed, 88 insertions, 58 deletions
diff --git a/Makefile b/Makefile
index 60342fa6..56c0cca4 100644
--- a/Makefile
+++ b/Makefile
@@ -31,6 +31,7 @@ COQDEP="$(COQBIN)coqdep" $(COQINCLUDES)
COQDOC="$(COQBIN)coqdoc"
COQEXEC="$(COQBIN)coqtop" $(COQINCLUDES) -batch -load-vernac-source
COQCHK="$(COQBIN)coqchk" $(COQINCLUDES)
+CP=cp
OCAMLBUILD=ocamlbuild
OCB_OPTIONS=\
@@ -130,14 +131,6 @@ DRIVER=Compopts.v Compiler.v Complements.v
FILES=$(LIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \
$(PARSERVALIDATOR) $(PARSER)
-# Symbolic links vs. copy
-
-ifneq (,$(findstring CYGWIN,$(shell uname -s)))
-SLN=cp
-else
-SLN=ln -s
-endif
-
all:
$(MAKE) proof
$(MAKE) extraction
@@ -160,34 +153,34 @@ extraction/STAMP: $(FILES:.v=.vo) extraction/extraction.v $(ARCH)/extractionMach
ccomp: extraction/STAMP compcert.ini
$(OCAMLBUILD) $(OCB_OPTIONS) Driver.native \
- && rm -f ccomp && $(SLN) _build/driver/Driver.native ccomp
+ && $(CP) _build/driver/Driver.native ccomp
ccomp.prof: extraction/STAMP compcert.ini
$(OCAMLBUILD) $(OCB_OPTIONS) Driver.p.native \
- && rm -f ccomp.prof && $(SLN) _build/driver/Driver.p.native ccomp.prof
+ && $(CP) _build/driver/Driver.p.native ccomp.prof
ccomp.byte: extraction/STAMP compcert.ini
$(OCAMLBUILD) $(OCB_OPTIONS) Driver.d.byte \
- && rm -f ccomp.byte && $(SLN) _build/driver/Driver.d.byte ccomp.byte
+ && $(CP) _build/driver/Driver.d.byte ccomp.byte
runtime:
$(MAKE) -C runtime
cchecklink: compcert.ini
$(OCAMLBUILD) $(OCB_OPTIONS_CHECKLINK) Validator.native \
- && rm -f cchecklink && $(SLN) _build/checklink/Validator.native cchecklink
+ && $(CP) _build/checklink/Validator.native cchecklink
cchecklink.byte: compcert.ini
$(OCAMLBUILD) $(OCB_OPTIONS_CHECKLINK) Validator.d.byte \
- && rm -f cchecklink.byte && $(SLN) _build/checklink/Validator.d.byte cchecklink.byte
+ && $(CP) _build/checklink/Validator.d.byte cchecklink.byte
clightgen: extraction/STAMP compcert.ini exportclight/Clightdefs.vo
$(OCAMLBUILD) $(OCB_OPTIONS_CLIGHTGEN) Clightgen.native \
- && rm -f clightgen && $(SLN) _build/exportclight/Clightgen.native clightgen
+ && $(CP) _build/exportclight/Clightgen.native clightgen
clightgen.byte: extraction/STAMP compcert.ini exportclight/Clightdefs.vo
$(OCAMLBUILD) $(OCB_OPTIONS_CLIGHTGEN) Clightgen.d.byte \
- && rm -f clightgen.byte && $(SLN) _build/exportclight/Clightgen.d.byte clightgen.byte
+ && $(CP) _build/exportclight/Clightgen.d.byte clightgen.byte
.PHONY: proof extraction ccomp ccomp.prof ccomp.byte runtime cchecklink cchecklink.byte clightgen clightgen.byte
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 7b9e2cc8..c7157aac 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -168,8 +168,10 @@ let thumbS oc =
let name_of_section = function
| Section_text -> ".text"
- | Section_data i | Section_small_data i -> if i then ".data" else "COMM"
- | Section_const | Section_small_const -> ".section .rodata"
+ | Section_data i | Section_small_data i ->
+ if i then ".data" else "COMM"
+ | Section_const i | Section_small_const i ->
+ if i then ".section .rodata" else "COMM"
| Section_string -> ".section .rodata"
| Section_literal -> ".text"
| Section_jumptable -> ".text"
diff --git a/checklink/Check.ml b/checklink/Check.ml
index 87910863..db0159c4 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -69,8 +69,8 @@ let name_of_section_Linux: section_name -> string = function
| Section_text -> ".text"
| Section_data i -> if i then ".data" else "COMM"
| Section_small_data i -> if i then ".sdata" else ".sbss"
-| Section_const -> ".rodata"
-| Section_small_const -> ".sdata2"
+| Section_const i -> if i then ".rodata" else "COMM"
+| Section_small_const i -> if i then ".sdata2" else "COMM"
| Section_string -> ".rodata"
| Section_literal -> ".rodata.cst8"
| Section_jumptable -> ".text"
@@ -79,10 +79,10 @@ let name_of_section_Linux: section_name -> string = function
(** Adapted from CompCert *)
let name_of_section_Diab: section_name -> string = function
| Section_text -> ".text"
-| Section_data i -> if i then ".data" else ".bss"
+| Section_data i -> if i then ".data" else "COMM"
| Section_small_data i -> if i then ".sdata" else ".sbss"
-| Section_const -> ".text"
-| Section_small_const -> ".sdata2"
+| Section_const _ -> ".text"
+| Section_small_const _ -> ".sdata2"
| Section_string -> ".text"
| Section_literal -> ".text"
| Section_jumptable -> ".text"
@@ -91,7 +91,6 @@ let name_of_section_Diab: section_name -> string = function
(** Taken from CompCert *)
let name_of_section: section_name -> string =
begin match Configuration.system with
- | "macosx" -> fatal "Unsupported CompCert configuration: macosx"
| "linux" -> name_of_section_Linux
| "diab" -> name_of_section_Diab
| _ -> fatal "Unsupported CompCert configuration"
diff --git a/common/Sections.ml b/common/Sections.ml
index d7ae8195..c6d4c4c2 100644
--- a/common/Sections.ml
+++ b/common/Sections.ml
@@ -21,8 +21,8 @@ type section_name =
| Section_text
| Section_data of bool (* true = init data, false = uninit data *)
| Section_small_data of bool
- | Section_const
- | Section_small_const
+ | Section_const of bool
+ | Section_small_const of bool
| Section_string
| Section_literal
| Section_jumptable
@@ -68,13 +68,13 @@ let builtin_sections = [
sec_writable = true; sec_executable = false;
sec_access = Access_near};
"CONST",
- {sec_name_init = Section_const;
- sec_name_uninit = Section_const;
+ {sec_name_init = Section_const true;
+ sec_name_uninit = Section_const false;
sec_writable = false; sec_executable = false;
sec_access = Access_default};
"SCONST",
- {sec_name_init = Section_small_const;
- sec_name_uninit = Section_small_const;
+ {sec_name_init = Section_small_const true;
+ sec_name_uninit = Section_small_const false;
sec_writable = false; sec_executable = false;
sec_access = Access_near};
"STRING",
diff --git a/common/Sections.mli b/common/Sections.mli
index ff6c8c95..38b99db0 100644
--- a/common/Sections.mli
+++ b/common/Sections.mli
@@ -20,8 +20,8 @@ type section_name =
| Section_text
| Section_data of bool (* true = init data, false = uninit data *)
| Section_small_data of bool
- | Section_const
- | Section_small_const
+ | Section_const of bool
+ | Section_small_const of bool
| Section_string
| Section_literal
| Section_jumptable
diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index aff638e7..e73125f7 100644
--- a/driver/Configuration.ml
+++ b/driver/Configuration.ml
@@ -58,8 +58,6 @@ let get_config key =
let bad_config key v =
Printf.eprintf "Invalid value `%s' for configuation option `%s'\n" v key; exit 2
-let stdlib_path = get_config "stdlib_path"
-
let prepro = get_config "prepro"
let asm = get_config "asm"
let linker = get_config "linker"
@@ -81,6 +79,13 @@ let has_runtime_lib =
| "false" -> false
| v -> bad_config "has_runtime_lib" v
+
+let stdlib_path =
+ if has_runtime_lib then
+ get_config "stdlib_path"
+ else
+ ""
+
let asm_supports_cfi =
match get_config "asm_supports_cfi" with
| "true" -> true
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 41002bac..649fd292 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -57,7 +57,7 @@ let preg oc = function
(* System dependend printer functions *)
-module type SYSTEM=
+module type SYSTEM =
sig
val raw_symbol: out_channel -> string -> unit
val symbol: out_channel -> P.t -> unit
@@ -69,6 +69,8 @@ module type SYSTEM=
val print_fun_info: out_channel -> P.t -> unit
val print_var_info: out_channel -> P.t -> unit
val print_epilogue: out_channel -> unit
+ val print_comm_decl: out_channel -> P.t -> Z.t -> int -> unit
+ val print_lcomm_decl: out_channel -> P.t -> Z.t -> int -> unit
end
(* Printer functions for cygwin *)
@@ -86,8 +88,10 @@ module Cygwin_System =
let name_of_section = function
| Section_text -> ".text"
- | Section_data _ | Section_small_data _ -> ".data"
- | Section_const | Section_small_const -> ".section .rdata,\"dr\""
+ | Section_data i | Section_small_data i ->
+ if i then ".data" else "COMM"
+ | Section_const i | Section_small_const i ->
+ if i then ".section .rdata,\"dr\"" else "COMM"
| Section_string -> ".section .rdata,\"dr\""
| Section_literal -> ".section .rdata,\"dr\""
| Section_jumptable -> ".text"
@@ -108,6 +112,14 @@ module Cygwin_System =
let print_var_info _ _ = ()
let print_epilogue _ = ()
+
+ let print_comm_decl oc name sz al =
+ fprintf oc " .comm %a, %s, %d\n" symbol name (Z.to_string sz) al
+
+ let print_lcomm_decl oc name sz al =
+ fprintf oc " .local %a\n" symbol name;
+ print_comm_decl oc name sz al
+
end:SYSTEM)
(* Printer functions for ELF *)
@@ -125,8 +137,10 @@ module ELF_System =
let name_of_section = function
| Section_text -> ".text"
- | Section_data i | Section_small_data i -> if i then ".data" else "COMM"
- | Section_const | Section_small_const -> ".section .rodata"
+ | Section_data i | Section_small_data i ->
+ if i then ".data" else "COMM"
+ | Section_const i | Section_small_const i ->
+ if i then ".section .rodata" else "COMM"
| Section_string -> ".section .rodata"
| Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8"
| Section_jumptable -> ".text"
@@ -151,6 +165,14 @@ module ELF_System =
fprintf oc " .size %a, . - %a\n" symbol name symbol name
let print_epilogue _ = ()
+
+ let print_comm_decl oc name sz al =
+ fprintf oc " .comm %a, %s, %d\n" symbol name (Z.to_string sz) al
+
+ let print_lcomm_decl oc name sz al =
+ fprintf oc " .local %a\n" symbol name;
+ print_comm_decl oc name sz al
+
end:SYSTEM)
(* Printer functions for MacOS *)
@@ -168,8 +190,10 @@ module MacOS_System =
let name_of_section = function
| Section_text -> ".text"
- | Section_data _ | Section_small_data _ -> ".data"
- | Section_const | Section_small_const -> ".const"
+ | Section_data i | Section_small_data i ->
+ if i then ".data" else "COMM"
+ | Section_const i | Section_small_const i ->
+ if i then ".const" else "COMM"
| Section_string -> ".const"
| Section_literal -> ".literal8"
| Section_jumptable -> ".const"
@@ -209,6 +233,14 @@ module MacOS_System =
!indirect_symbols;
indirect_symbols := StringSet.empty
+ let print_comm_decl oc name sz al =
+ fprintf oc " .comm %a, %s, %d\n"
+ symbol name (Z.to_string sz) (log2 al)
+
+ let print_lcomm_decl oc name sz al =
+ fprintf oc " .lcomm %a, %s, %d\n"
+ symbol name (Z.to_string sz) (log2 al)
+
end:SYSTEM)
@@ -996,12 +1028,9 @@ let print_var oc name v =
end else begin
let sz =
match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in
- if C2C.atom_is_static name then
- fprintf oc " .local %a\n" symbol name;
- fprintf oc " .comm %a, %s, %d\n"
- symbol name
- (Z.to_string sz)
- align
+ if C2C.atom_is_static name
+ then Target.print_lcomm_decl oc name sz align
+ else Target.print_comm_decl oc name sz align
end
let print_globdef oc (name, gdef) =
@@ -1032,7 +1061,8 @@ let print_program oc p =
Hashtbl.clear Printer.filename_num;
List.iter (Printer.print_globdef oc) p.prog_defs;
if !Printer.need_masks then begin
- Printer.section oc Section_const; (* not Section_literal because not 8-bytes *)
+ Printer.section oc (Section_const true);
+ (* not Section_literal because not 8-bytes *)
Target.print_align oc 16;
fprintf oc "%a: .quad 0x8000000000000000, 0\n"
Target.raw_symbol "__negd_mask";
diff --git a/powerpc/PrintDiab.ml b/powerpc/PrintDiab.ml
index 0d9f74e6..1aa27405 100644
--- a/powerpc/PrintDiab.ml
+++ b/powerpc/PrintDiab.ml
@@ -54,16 +54,16 @@ module Diab_System =
let name_of_section = function
| Section_text -> ".text"
- | Section_data i -> if i then ".data" else ".bss"
+ | Section_data i -> if i then ".data" else "COMM"
| Section_small_data i -> if i then ".sdata" else ".sbss"
- | Section_const -> ".text"
- | Section_small_const -> ".sdata2"
+ | Section_const _ -> ".text"
+ | Section_small_const _ -> ".sdata2"
| Section_string -> ".text"
| Section_literal -> ".text"
| Section_jumptable -> ".text"
| Section_user(s, wr, ex) ->
sprintf ".section \"%s\",,%c"
- s
+ s
(match wr, ex with
| true, true -> 'm' (* text+data *)
| true, false -> 'd' (* data *)
diff --git a/powerpc/PrintLinux.ml b/powerpc/PrintLinux.ml
index ed4ef19b..4e90308c 100644
--- a/powerpc/PrintLinux.ml
+++ b/powerpc/PrintLinux.ml
@@ -53,13 +53,14 @@ module Linux_System =
let name_of_section = function
| Section_text -> ".text"
- | Section_data i -> if i then ".data" else "COMM"
+ | Section_data i ->
+ if i then ".data" else "COMM"
| Section_small_data i ->
- if i
- then ".section .sdata,\"aw\",@progbits"
- else ".section .sbss,\"aw\",@progbits"
- | Section_const -> ".rodata"
- | Section_small_const -> ".section .sdata2,\"a\",@progbits"
+ if i then ".section .sdata,\"aw\",@progbits" else "COMM"
+ | Section_const i ->
+ if i then ".rodata" else "COMM"
+ | Section_small_const i ->
+ if i then ".section .sdata2,\"a\",@progbits" else "COMM"
| Section_string -> ".rodata"
| Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8"
| Section_jumptable -> ".text"
diff --git a/test/regression/decl1.c b/test/regression/decl1.c
index d2aedba7..6049b4af 100644
--- a/test/regression/decl1.c
+++ b/test/regression/decl1.c
@@ -10,7 +10,7 @@ int f (int p)
int main (int argc, char **argv)
{
- int (*p)();
+ int (*p)(int);
int f();
int i;
generated by cgit (git 2.34.1) at 2024-07-01 15:37:15 +0000