diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | Makefile.menhir | 37 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 9 | ||||
| -rwxr-xr-x | configure | 40 | ||||
| -rw-r--r-- | cparser/Cerrors.ml | 7 | ||||
| -rw-r--r-- | cparser/Parse.ml | 2 | ||||
| -rw-r--r-- | cparser/Rename.ml | 29 | ||||
| -rw-r--r-- | cparser/Rename.mli | 2 | ||||
| -rw-r--r-- | debug/DebugInit.ml | 38 | ||||
| -rw-r--r-- | debug/Dwarfgen.ml | 6 | ||||
| -rw-r--r-- | doc/ccomp.1 | 533 | ||||
| -rw-r--r-- | driver/Clflags.ml | 3 | ||||
| -rw-r--r-- | driver/Driver.ml | 41 | ||||
| -rw-r--r-- | driver/Optionsprinter.ml | 1 |
14 files changed, 642 insertions, 108 deletions
@@ -246,6 +246,8 @@ install: install -m 0755 ./ccomp $(BINDIR) install -d $(SHAREDIR) install -m 0644 ./compcert.ini $(SHAREDIR) + install -d $(MANDIR)/man1 + install -m 0644 ./doc/ccomp.1 $(MANDIR)/man1 $(MAKE) -C runtime install ifeq ($(CLIGHTGEN),true) install -m 0755 ./clightgen $(BINDIR) diff --git a/Makefile.menhir b/Makefile.menhir index b72c52f3..1530536f 100644 --- a/Makefile.menhir +++ b/Makefile.menhir @@ -47,40 +47,3 @@ endif %.ml %.mli: %.mly $(MENHIR) $(MENHIR_MODE) $(MENHIR_FLAGS) $< - -# Note 1: finding where MenhirLib has been installed would be easier if we -# could depend on ocamlfind, but as far as I understand and as of today, -# CompCert can be compiled and linked even in the absence of ocamlfind. -# So, we should not require ocamlfind. - -# Note 2: Menhir has options --suggest-comp-flags and --suggest-link-flags -# which we are supposed to help solve this difficulty. However, they don't -# work for us out of the box, because if Menhir has been installed using -# ocamlfind, then Menhir will suggest using ocamlfind (i.e. it will suggest -# -package and -linkpkg options), which we don't want to do. - -# Solution: Ask Menhir first. If Menhir answers "-package menhirLib", then -# Menhir was installed with ocamlfind, so we should not ask Menhir, but we -# can instead ask ocamlfind where Menhir's library was installed. Otherwise, -# Menhir answers directly with a "-I ..." directive, which we use. - -ifndef MENHIR_INCLUDES - -ifeq ($(MENHIR_TABLE),true) - - MENHIR_SUGGESTION = $(MENHIR) $(MENHIR_MODE) --suggest-comp-flags - - MENHIR_INCLUDES := $(shell \ - if $(MENHIR_SUGGESTION) | grep -e "-package" >/dev/null ; then \ - echo "-I `ocamlfind query menhirLib`" ; \ - else \ - $(MENHIR_SUGGESTION) ; \ - fi) - -else - - MENHIR_INCLUDES = - -endif - -endif diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 38ef45e7..a1ca48d1 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -365,12 +365,15 @@ let make_builtin_memcpy args = let sz1 = match Initializers.constval !comp_env sz with | Errors.OK(Vint n) -> n - | _ -> error "argument 3 of '__builtin_memcpy_aligned' must be a constant"; Integers.Int.zero in + | _ -> error "size argument of '__builtin_memcpy_aligned' must be a constant"; Integers.Int.zero in let al1 = match Initializers.constval !comp_env al with | Errors.OK(Vint n) -> n - | _ -> error "argument 4 of '__builtin_memcpy_aligned' must be a constant"; Integers.Int.one in - (* to check: sz1 > 0, al1 divides sz1, al1 = 1|2|4|8 *) + | _ -> error "alignment argument of '__builtin_memcpy_aligned' must be a constant"; Integers.Int.one in + if Integers.Int.is_power2 al1 = None then + error "alignment argument of '__builtin_memcpy_aligned' must be a power of 2"; + if Integers.Int.modu sz1 al1 <> Integers.Int.zero then + error "alignment argument of '__builtin_memcpy_aligned' must be a divisor of the size"; (* Issue #28: must decay array types to pointer types *) Ebuiltin(EF_memcpy(sz1, al1), Tcons(typeconv(typeof dst), @@ -21,6 +21,7 @@ has_runtime_lib=true has_standard_headers=true clightgen=false responsefile="gnu" +merlin=false usage='Usage: ./configure [options] target @@ -69,6 +70,7 @@ Options: -no-runtime-lib Do not compile nor install the runtime support library -no-standard-headers Do not install nor use the standard .h headers -clightgen Also compile the clightgen tool + -merlin Generate .merlin file ' @@ -93,6 +95,8 @@ while : ; do has_standard_headers=false;; -clightgen) clightgen=true;; + -merlin) + merlin=true;; *) if test -n "$target"; then echo "$usage" 1>&2; exit 2; fi target="$1";; @@ -449,8 +453,9 @@ echo "Testing Menhir... " | tr -d '\n' menhir_ver=`menhir --version 2>/dev/null | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p'` case "$menhir_ver" in 20[0-9][0-9][0-9][0-9][0-9][0-9]) - if test "$menhir_ver" -ge $MENHIR_REQUIRED; then + if test "$menhir_ver" -ge $MENHIR_REQUIRED; then echo "version $menhir_ver -- good!" + menhir_includes="-I `menhir --suggest-menhirLib`" else echo "version $menhir_ver -- UNSUPPORTED" echo "Error: CompCert requires Menhir version $MENHIR_REQUIRED or later." @@ -484,6 +489,32 @@ if $missingtools; then exit 2 fi +if $merlin; then + cat > .merlin <<EOF +S lib +S common +S $arch +S backend +S cfrontend +S driver +S debug +S exportclight +S cparser +S extraction + +B lib +B common +B $arch +B backend +B cfrontend +B driver +B debug +B exportclight +B cparser +B extraction + +EOF +fi # # Generate Makefile.config @@ -495,9 +526,16 @@ cat > Makefile.config <<EOF PREFIX=$prefix BINDIR=$bindir LIBDIR=$libdir +MANDIR=$sharedir/man SHAREDIR=$sharedir OCAML_OPT_COMP=$ocaml_opt_comp +MENHIR_INCLUDES=$menhir_includes EOF +if $merlin; then + cat >> Makefile.config <<EOF +COMPFLAGS=-bin-annot +EOF +fi if test "$target" != "manual"; then cat >> Makefile.config <<EOF diff --git a/cparser/Cerrors.ml b/cparser/Cerrors.ml index c50e12d9..a38cceee 100644 --- a/cparser/Cerrors.ml +++ b/cparser/Cerrors.ml @@ -21,7 +21,10 @@ open Commandline let error_fatal = ref false let color_diagnostics = let term = try Sys.getenv "TERM" with Not_found -> "" in - ref (Unix.isatty Unix.stderr && term <> "dumb" && term <>"") + let activate = try + (Unix.isatty Unix.stderr && term <> "dumb" && term <>"") + with _ -> false in + ref activate let num_errors = ref 0 let num_warnings = ref 0 @@ -197,7 +200,7 @@ let classify_warning w = SuppressedMsg,None let cprintf fmt c = - if Unix.isatty Unix.stderr && !color_diagnostics then + if !color_diagnostics then fprintf fmt c else ifprintf fmt c diff --git a/cparser/Parse.ml b/cparser/Parse.ml index 507aea36..dceb9b11 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -24,7 +24,7 @@ let transform_program t p name = (run_pass Unblock.program 'b' (run_pass Bitfields.program 'f' p)))) in - (Rename.program p1 (Filename.chop_suffix name ".c")) + (Rename.program p1) let parse_transformations s = let t = ref CharSet.empty in diff --git a/cparser/Rename.ml b/cparser/Rename.ml index c62c6763..c1f31977 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -43,17 +43,6 @@ let enter_public env id = re_public = StringMap.add id.name id env.re_public; re_used = StringSet.add id.name env.re_used } -let enter_static env id file = - try - let id' = StringMap.find id.name env.re_public in - { env with re_id = IdentMap.add id id' env.re_id } - with Not_found -> - let file = String.map (fun a -> match a with 'a'..'z' | 'A'..'Z' | '0'..'9' -> a | _ -> '_') file in - let id' = {id with name = Printf.sprintf "_%s_%s" file id.name} in - { re_id = IdentMap.add id id' env.re_id; - re_public = env.re_public; - re_used = StringSet.add id'.name env.re_used } - (* For static or local identifiers, we make up a new name if needed *) (* If the same identifier has already been declared, don't rename a second time *) @@ -260,7 +249,7 @@ let reserve_builtins () = (* Reserve global declarations with public visibility *) -let rec reserve_public env file = function +let rec reserve_public env = function | [] -> env | dcl :: rem -> let env' = @@ -268,27 +257,21 @@ let rec reserve_public env file = function | Gdecl(sto, id, _, _) -> begin match sto with | Storage_default | Storage_extern -> enter_public env id - | Storage_static -> if !Clflags.option_rename_static then - enter_static env id file - else - env + | Storage_static -> env | _ -> assert false end | Gfundef f -> begin match f.fd_storage with | Storage_default | Storage_extern -> enter_public env f.fd_name - | Storage_static -> if !Clflags.option_rename_static then - enter_static env f.fd_name file - else - env + | Storage_static -> env | _ -> assert false end | _ -> env in - reserve_public env' file rem + reserve_public env' rem (* Rename the program *) -let program p file = +let program p = globdecls - (reserve_public (reserve_builtins()) file p) + (reserve_public (reserve_builtins()) p) [] p diff --git a/cparser/Rename.mli b/cparser/Rename.mli index c4ef2228..818a51bc 100644 --- a/cparser/Rename.mli +++ b/cparser/Rename.mli @@ -13,4 +13,4 @@ (* *) (* *********************************************************************) -val program : C.program -> string -> C.program +val program : C.program -> C.program diff --git a/debug/DebugInit.ml b/debug/DebugInit.ml index b3fedb00..ed22f7c2 100644 --- a/debug/DebugInit.ml +++ b/debug/DebugInit.ml @@ -10,7 +10,10 @@ (* *) (* *********************************************************************) +open Clflags +open Commandline open Debug +open Driveraux let default_debug = { @@ -48,7 +51,6 @@ let init_debug () = implem := if Configuration.system = "diab" then let gen = (fun a b -> Some (Dwarfgen.gen_diab_debug_info a b)) in - Clflags.option_gdwarf := 2; (* Dwarf 2 is the only supported target *) {default_debug with generate_debug_info = gen; add_diab_info = DebugInformation.add_diab_info; add_fun_addr = DebugInformation.diab_add_fun_addr;} @@ -60,7 +62,39 @@ let init_none () = implem := default_implem let init () = - if !Clflags.option_g then + if !option_g then init_debug () else init_none () + +let gnu_debugging_help = +" -gdwarf- Generate debug information in DWARF v2 or DWARF v3\n" + +let debugging_help = +"Debugging options:\n\ +\ -g Generate debugging information\n\ +\ -g<n> Control generation of debugging information\n\ +\ (<n>=0: none, <n>=1: only-globals, <n>=2: globals + locals \n\ +\ without locations, <n>=3: full;)\n" +^ (if gnu_system then gnu_debugging_help else "") + +let gnu_debugging_actions = + let version version () = + option_g:=true; + option_gdwarf:=version + in + [Exact "-gdwarf-2", Unit (version 2); + Exact "-gdwarf-3", Unit (version 3);] + +let debugging_actions = + let depth depth () = + option_g:=true; + option_gdepth := depth + in + [Exact "-g", Unit (depth 3); + Exact "-g0", Unset option_g; + Exact "-g1", Unit (depth 1); + Exact "-g2", Unit (depth 2); + Exact "-g3", Unit (depth 3);] + @ + (if gnu_system then gnu_debugging_actions else []) diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml index 76e2d638..617c4570 100644 --- a/debug/Dwarfgen.ml +++ b/debug/Dwarfgen.ml @@ -470,9 +470,10 @@ module Dwarfgenaux (Target: TARGET) = let scope = { lexical_block_range = r; } in + let acc = (acc >>= dwr) in let vars,acc = mmap_opt (local_to_entry f_id) acc sc.scope_variables in let entry = new_entry id (DW_TAG_lexical_block scope) in - add_children entry vars,(acc >>= dwr) + add_children entry vars,acc and local_to_entry f_id acc id = match get_local_variable id with @@ -577,7 +578,8 @@ let gnu_file_loc (f,l) = let string_table: (string,int) Hashtbl.t = Hashtbl.create 7 let gnu_string_entry s = - if String.length s < 4 || Configuration.system = "cygwin" then (*Cygwin does not use the debug_str seciton *) + if (String.length s < 4 && Configuration.system <> "macosx") (* macosx needs debug_str *) + || Configuration.system = "cygwin" then (*Cygwin does not use the debug_str seciton*) Simple_string s else try diff --git a/doc/ccomp.1 b/doc/ccomp.1 new file mode 100644 index 00000000..9d15791e --- /dev/null +++ b/doc/ccomp.1 @@ -0,0 +1,533 @@ +.TH CCOMP 1 +.SH NAME +ccomp \- the CompCert C compiler +. +.SH SYNOPSIS +\fBccomp\fP [\fIoptions\fP] \fIfile ...\fP +. +.SH DESCRIPTION +\fBCompCert C\fP is a compiler for the C programming language. +Its intended use is the compilation of life-critical and mission-critical software written in C and meeting high levels of assurance. +It accepts most of the ISO C 99 language, with some exceptions and a few extensions. +It produces machine code for the PowerPC, ARM, and IA-32 architectures. +.PP +What sets CompCert C apart from any other production compiler, is that it is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation issues. +In other words, the executable code it produces is proved to behave exactly as specified by the semantics of the source C program. +This level of confidence in the correctness of the compilation process is unprecedented and contributes to meeting the highest levels of software assurance. +In particular, using the CompCert C compiler is a natural complement to applying formal verification techniques (static analysis, program proof, model checking) at the source code level: the correctness proof of CompCert C guarantees that all safety properties verified on the source code automatically hold as well for the generated executable. +. +.SH +RECOGNIZED SOURCE FILES +. +.TP +.B .c +C source file. +. +.TP +.BR .i ", " .p +C source file that should not be preprocessed. +. +.TP +.B .cm +Cminor source file. +. +.TP +.B .s +Assembly file. +. +.TP +.B .S +Assembly file that must be preprocessed. +. +.TP +.B .o +Object file. +. +.TP +.B .a +Library file. +. +.SH OPTIONS +.SS Processing Options +.INDENT 0.0 +. +.TP +.B \-c +Compile to object file only (no linking), result in <file>.o. +. +.TP +.B \-E +Preprocess only, send result to standard output. +. +.TP +.B \-S +Compile to assembler only, save result in <file>.s. +. +.TP +.B \-o <file> +Generate output to <file>. +. +.SS Preprocessing Options +.INDENT 0.0 +. +.TP +.B \-I<dir> +Add <dir> to search path for include files. +. +.TP +.B \-include <file> +Process <file> as if \fB#include "<file>"\fP appears at the first line of the primary source file. +. +.TP +.B \-D<symbol>=<value> +Define a preprocessor symbol. +. +.TP +.B \-U<symbol> +Undefine a preprocessor symbol. +. +.TP +.B \-Wp,<args> +Pass comma separated arguments in <args> to the preprocessor. +. +.TP +.B \-Xpreprocessor <arg> +Pass argument <arg> to the preprocessor. +. +.TP +.BR \-C ", " \-CC ", " \-idirafter ", " \-imacros ", " \-iquote ", " \-isystem ", " \-M ", " \-MF ", " \-MG ", " \-MM ", " \-MP ", " \-MQ ", " \-MT ", " \-nostdinc ", " \-P +For GNU backends these options are recognized by CompCert and passed through to the preprocessor. +. +.SS +Optimization Options +.INDENT 0.0 +. +.TP +.B \-O +Optimize the compiled code. +Enabled by default. +. +.TP +.B \-O0 +Turn off most optimizations. +Synonymous to \fB\-fno\-const\-prop\fP \fB\-fno\-cse\fP \fB\-fno\-redundancy\fP \fB\-fno\-tailcalls\fP. +. +.TP +.BR \-O1 ", " \-O2 ", " \-O3 +Synonymous for \fB\-O\fP. +. +.TP +.B \-Os +Optimize for code size in preference to code speed. +. +.TP +.BR \-fconst\-prop ", " \-fno\-const\-prop +Turn on/off global constant propagation. +Enabled by default. +. +.TP +.BR \-fcse ", " \-fno\-cse +Turn on/off common subexpression elimination. +Enabled by default. +. +.TP +.BR \-fredundancy ", " \-fno\-redundancy +Turn on/off redundancy elimination. +Enabled by default. +. +.TP +.BR \-ftailcalls ", " \-fno\-tailcalls +Turn on/off optimization of function calls in tail position. +Enabled by default. +. +.TP +.B \-ffloat\-const\-prop <n> +Control constant propagation of floats (<n>=0: none, <n>=1: limited, <n>=2: full). +Default is full constant propagation. +. +.SS +Code Generation Options +.INDENT 0.0 +. +.TP +.B \-falign\-functions <n> +Set alignment of function entry points to <n> bytes. +The default alignment is 16 bytes for IA-32 targets and 4 bytes for ARM and PowerPC. +. +.TP +.BR \-ffpu ", " \-fno\-fpu +Turn on/off use of FP registers for some integer operations. +Enabled by default. +. +.SS +Code Generation Options (PowerPC with Diab Backend) +.INDENT 0.0 +. +.TP +.B \-falign\-branch\-targets <n> +Set alignment of branch targets to <n> bytes. +The default alignment is 0 bytes, which deactivates alignment of branch targets. +. +.TP +.B \-falign\-cond\-branches <n> +Set alignment of conditional branches to <n> bytes. +The default alignment is 0 bytes, which deactivates alignment of conditional branch targets. +. +.TP +.B \-fsmall\-const <n> +Set maximal size for allocation in small data constant to <n> bytes. +The default is 8 bytes. +. +.TP +.B \-fsmall\-data <n> +Set maximal size for allocation in small data area to <n> bytes. +The default is 8 bytes. +. +.SS +Code Generation Options (ARM Targets) +.INDENT 0.0 +. +.TP +.B \-mthumb +Generate code using the Thumb 2 instruction encoding. +This is the default if CompCert is configured for the ARMv7R profile. +. +.TP +.B \-marm +Generate code using the ARM instruction encoding. +This is the default if CompCert is configured for a profile other than ARMv7R. +. +.SS +Assembling Options +.INDENT 0.0 +. +.TP +.B \-Wa,<args> +Pass comma separated arguments in <args> to the assembler. +. +.TP +.B \-Xassembler <arg> +Pass argument <arg> to the assembler. +. +.SS +Debugging Options +.INDENT 0.0 +. +.TP +.B \-g +Generate debugging information. +. +.TP +.BR \-g0 ", " \-g1 ", " \-g2 ", " \-g3 +Control generation of debugging information (0: none, 1: only globals, 2: globals and locals without locations, 3: full debug information). The default level is 3 for full debug information. +. +.SS +Debugging Options (GNU Backend) +.INDENT 0.0 +. +.TP +.B \-gdwarf-<n> +For GNU backends select debug information in DWARF format version 2 or 3. +The default format is DWARF v3. +. +.SS +Linking Options +.INDENT 0.0 +. +.TP +.B \-l<library> +Link library <library>. +. +.TP +.B \-L<dir> +Add <dir> to search path for libraries. +. +.TP +.B \-Wl,<args> +Pass comma separated arguments in <args> to the linker. +. +.TP +.B \-WUl,<args> +Pass comma separated arguments in <args> to the driver program used for linking. +. +.TP +.B \-Xlinker <arg> +Pass argument <arg> to the linker. +. +.TP +.B \-s +Remove all symbol table and relocation information from the executable. +. +.TP +.B \-static +Prevent linking with the shared libraries. +. +.TP +.B \-T <file> +Use <file> as linker command file. +. +.TP +.B \-u <symbol> +Pretend the symbol <symbol> is undefined to force linking of library modules to define it. +. +.TP +.BR \-nodefaultlibs ", " \-nostartfiles ", " \-nostdlib +For GNU backends these options are recognized by CompCert and passed through to the linker. +. +.SS +Language Support Options +.INDENT 0.0 +. +.TP +.BR \-fbitfields ", " \-fno\-bitfields +Turn on/off support for emulation bit fields in structs. +Disabled by default. +. +.TP +.BR \-flongdouble ", " \-fno\-longdouble +Turn on/off support for emulation of \fBlong double\fP as \fBdouble\fP. +Disabled by default. +. +.TP +.BR \-fpacked\-structs ", " \-fno\-packed\-structs +Turn on/off support for emulation of packed structs. +Disabled by default. +. +.TP +.BR \-fstruct\-passing ", " \-fno\-struct\-passing\fR +Turn on/off support for passing structs and unions by value as function results or function arguments. +Disabled by default. +. +.TP +.BR \-funprototyped ", " \-fno\-unprototyped +Turn on/off support calls to old-style functions without prototypes. +Enabled by default. +. +.TP +.BR \-fvararg\-calls ", " \-fno\-vararg\-calls +Turn on/off support for calls to variable-argument functions. +Enabled by default. +. +.TP +.BR \-finline-asm ", " \-fno\-inline-asm +Turn on/off support for inline \fBasm\fP statements. +Disabled by default. +. +.TP +.B \-fall +Activate all language support options above. +. +.TP +.B \-fnone +Deactivate all language support options above. +. +.SS +Diagnostic Options +.INDENT 0.0 +. +.TP +.B \-Wall +Enable all warnings. +. +.TP +.B \-W<warning> +Enable the specific warning <warning>. +CompCert supports the following warning classes: +.sp +\fIc11\-extensions\fP: +Feature specific to C11. +Enabled by default. +.sp +\fIcompare\-distinct\-pointer\-types\fP: +Comparison of different pointer types. +Enabled by default. +.sp +\fIcompcert\-conformance\fP: +Features that are not part of the CompCert C core language, e.g. K&R style functions. +Disabled by default. +.sp +\fIconstant\-conversion\fP: +Dangerous conversion of constants, e.g. literals that are too large for the given type. +Enabled by default. +.sp +\fIgnu\-empty\-struct\fP: +GNU extension for empty structs. +Enabled by default. +.sp +\fIimplicit\-function\-declaration\fP: +Deprecated implicit function declarations. +Enabled by default. +.sp +\fIimplicit\-int\fP: +Type of parameter or return type is implicitly assumed to be int. +Enabled by default. +.sp +\fIint\-conversion\fP: +Conversion between pointer and integer. +Enabled by default. +.sp +\fIinvalid\-noreturn\fP: +Functions declared as noreturn that actually contain a return statement. +Enabled by default. +.sp +\fIliteral\-range\fP: +Floating point literals with out-of-range magnitudes or values that convert to NaN. +Enabled by default. +.sp +\fImain\-return\-type\fP: +Wrong return type for main. +Enabled by default. +.sp +\fIpointer\-type\-mismatch\fP: +Use of incompatible pointer types in conditional expressions. +Enabled by default. +.sp +\fIreturn\-type\fP: +Void-return statement in non-void function. +Enabled by default. +.sp +\fIunknown\-attributes\fP: +Use of unsupported or unknown attributes. +Enabled by default. +.sp +\fIunknown\-pragmas\fP: +Use of unsupported or unknown pragmas. +Disabled by default. +.sp +\fIvarargs\fP: +Promotable vararg arguments. +Enabled by default. +.sp +\fIzero\-length\-array\fP: +GNU extension for zero length arrays. +Disabled by default. +. +.TP +.B \-Wno-<warning> +Disable the specific warning <warning>. +. +.TP +.B \-Werror +Treat all warnings of CompCert as errors. +. +.TP +.B \-Werror=<warning> +Treat the specific warning <warning> as an error. +. +.TP +.B \-Wno-error=<warning> +Prevent the specific warning <warning> from being treated as error even if \fB\-Werror\fP is specified. +. +.TP +.B \-Wfatal-errors +Treat all errors of CompCert as fatal errors, so that the compilation is aborted immediately. +. +.TP +.B \-fdiagnostics-color +Turn on colored diagnostics. Default for TTY output devices. +. +.TP +.B \-fno-diagnostics-color +Turn of colored diagnostics. +. +.SS +Tracing Options +.INDENT 0.0 +. +.TP +.B \-dprepro +Save C file after preprocessing in <file>.i +. +.TP +.B \-dparse +Save C file after parsing and elaboration in <file>.parsed.c. +. +.TP +.B \-dc +Save generated CompCert C in <file>.compcert.c. +. +.TP +.B \-dclight +Save generated Clight in <file>.light.c. +. +.TP +.B \-dcminor +Save generated Cminor in <file>.cm. +. +.TP +.B \-drtl +Save RTL at various optimization points in <file>.rtl.<n>. +. +.TP +.B \-dltl +Save LTL after register allocation in <file>.ltl. +. +.TP +.B \-dmach +Save generated Mach code in <file>.mach. +. +.TP +.B \-dasm +Save generated assembly in <file>.s. +. +.TP +.B \-dall +Save all generated intermediate files in <file>.<ext>. +. +.TP +.B \-doptions +Save the compiler configuration in <file>.opt.json. +. +.TP +.B \-sdump +Save abstract syntax tree of generated assembly for post-linking validation tool in <file>.json. +. +.SS +Miscellaneous Options +.INDENT 0.0 +. +.TP +.B \-stdlib <dir> +Set the path of the CompCert run-time library to <dir>. +. +.TP +.B \-v +Print external commands before invoking them. +. +.TP +.B \-timings +Print information about the time spent in various compiler passes. +. +.TP +.B \-version +Print the CompCert version information and exit. +. +.TP +.B @<file> +Read command line options from <file>. +. +.SS +Interpreter Mode +.INDENT 0.0 +. +.TP +.B \-interp +Execute the given .c files using the reference interpreter. +. +.TP +.B \-quiet +Suppress diagnostic messages for the interpreter. +. +.TP +.B \-trace +Have the interpreter produce a detailed trace of reductions. +. +.TP +.B \-random +Randomize execution order. +. +.TP +.B \-all +Simulate all possible execution orders. +.SH BUGS +To report bugs, please visit <https://github.com/AbsInt/CompCert/issues>. diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 6a695aa4..c7a5d3bf 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -45,7 +45,7 @@ let option_dmach = ref false let option_dasm = ref false let option_sdump = ref false let option_g = ref false -let option_gdwarf = ref 2 +let option_gdwarf = ref (if Configuration.system = "diab" then 2 else 3) let option_gdepth = ref 3 let option_o = ref (None: string option) let option_E = ref false @@ -60,6 +60,5 @@ let option_small_data = then 8 else 0) let option_small_const = ref (!option_small_data) let option_timings = ref false -let option_rename_static = ref false let stdlib_path = ref Configuration.stdlib_path let use_standard_headers = ref Configuration.has_standard_headers diff --git a/driver/Driver.ml b/driver/Driver.ml index 3cc1bcad..145de6c5 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -255,20 +255,6 @@ let version_string = else "The CompCert C verified compiler, version "^ Version.version ^ "\n" -let gnu_system = Configuration.system <> "diab" - -let gnu_debugging_help = -" -gdwarf- Generate debug information in DWARF v2 or DWARF v3\n" - -let debugging_help = -"Debugging options:\n\ -\ -g Generate debugging information\n\ -\ -gdepth <n> Control generation of debugging information\n\ -\ (<n>=0: none, <n>=1: only-globals, <n>=2: globals + locals\n\ -\ without locations, <n>=3: full;)\n" -^ (if gnu_system then gnu_debugging_help else "")^ -" -frename-static Rename static functions and declarations\n" - let target_help = if Configuration.arch = "arm" then "Target processor options:\n\ \ -mthumb Use Thumb2 instruction encoding\n\ @@ -305,7 +291,7 @@ Processing options:\n\ \ -finline-asm Support inline 'asm' statements [off]\n\ \ -fall Activate all language support options above\n\ \ -fnone Turn off all language support options above\n" ^ - debugging_help ^ + DebugInit.debugging_help ^ "Optimization options: (use -fno-<opt> to turn off -f<opt>)\n\ \ -O Optimize the compiled code [on by default]\n\ \ -O0 Do not optimize the compiled code\n\ @@ -337,7 +323,7 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>)\n\ \ -dltl Save LTL after register allocation in <file>.ltl\n\ \ -dmach Save generated Mach code in <file>.mach\n\ \ -dasm Save generated assembly in <file>.s\n\ -\ -dall Save all generated intermidate files in <file>.<ext>\n\ +\ -dall Save all generated intermediate files in <file>.<ext>\n\ \ -sdump Save info for post-linking validation in <file>.json\n\ \ -doptions Save the compiler configurations in <file>.opt.json\n\ General options:\n\ @@ -345,6 +331,8 @@ General options:\n\ \ -v Print external commands before invoking them\n\ \ -timings Show the time spent in various compiler passes\n\ \ -version Print the version string and exit\n\ +\ -target <value> Generate code for the given target\n\ +\ -conf <file> Read configuration from file\n\ \ @<file> Read command line options from <file>\n" ^ Cerrors.warning_help ^ "Interpreter mode:\n\ @@ -380,9 +368,6 @@ 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 - let dwarf_version version () = - option_g:=true; - option_gdwarf := version in [ (* Getting help *) Exact "-help", Unit print_usage_and_exit; @@ -401,21 +386,11 @@ let cmdline_actions = @ prepro_actions @ (* Language support options -- more below *) [ Exact "-fall", Unit (set_all language_support_options); - Exact "-fnone", Unit (unset_all language_support_options); -(* Debugging options *) - Exact "-g", Unit (dwarf_version 3);] @ - (if gnu_system then - [ Exact "-gdwarf-2", Unit (dwarf_version 2); - Exact "-gdwarf-3", Unit (dwarf_version 3);] - else []) @ - [ Exact "-frename-static", Set option_rename_static; - Exact "-gdepth", Integer (fun n -> if n = 0 || n <0 then begin - option_g := false - end else begin - option_g := true; - option_gdepth := if n > 3 then 3 else n - end); + Exact "-fnone", Unit (unset_all language_support_options);] + (* Debugging options *) + @ DebugInit.debugging_actions @ (* Code generation options -- more below *) + [ Exact "-O0", Unit (unset_all optimization_options); Exact "-O", Unit (set_all optimization_options); _Regexp "-O[123]$", Unit (set_all optimization_options); diff --git a/driver/Optionsprinter.ml b/driver/Optionsprinter.ml index 9dce8592..00b5f5ec 100644 --- a/driver/Optionsprinter.ml +++ b/driver/Optionsprinter.ml @@ -64,7 +64,6 @@ let print_clflags oc = p_jmember oc "small_data" p_jint !option_small_data; p_jmember oc "small_data" p_jint !option_small_const; p_jmember oc "timings" p_jbool !option_timings; - p_jmember oc "rename_static" p_jbool !option_rename_static; fprintf oc "\n}" let print_struct_passing_style oc = function |