diff options
| -rw-r--r-- | Changelog | 41 | ||||
| -rw-r--r-- | Makefile | 1 | ||||
| -rw-r--r-- | Makefile.extr | 17 | ||||
| -rw-r--r-- | cparser/Cerrors.ml | 69 | ||||
| -rw-r--r-- | cparser/Elab.mli | 9 | ||||
| -rw-r--r-- | debug/DebugInformation.ml | 1 | ||||
| -rw-r--r-- | debug/DebugTypes.mli | 1 | ||||
| -rw-r--r-- | debug/DwarfPrinter.ml | 4 | ||||
| -rw-r--r-- | debug/DwarfTypes.mli | 2 | ||||
| -rw-r--r-- | debug/Dwarfgen.ml | 2 | ||||
| -rw-r--r-- | doc/ccomp.1 | 24 | ||||
| -rw-r--r-- | driver/Commandline.ml | 17 | ||||
| -rw-r--r-- | driver/Commandline.mli | 5 | ||||
| -rwxr-xr-x | driver/Driver.ml | 7 |
14 files changed, 180 insertions, 20 deletions
@@ -1,5 +1,5 @@ -Working version -=============== +Release 3.0, 2017-02-xx +======================= Major improvements: @@ -18,6 +18,43 @@ Major improvements: above.) Support for x86-64 is currently available for Linux and MacOS X. (Run the configure script with 'x86_64-linux' or 'x86_64-macosx'.) +Language features: + +- Support for anonymous structures and unions as members of + structures or unions. (ISO C11, section 6.7.2.1, para 13 and 19.) +- New built-in functions for ARM and PowerPC: + __builtin_ctz, __builtin_ctzl, __builtin_ctzll + (count trailing zeros, 32 and 64 bits). + +Usability: + +- Added options -Wxxx and -Wno-xxx (for various values of "xxx") + to control which warnings are emitted. +- Support response files where additional command-line arguments can + be passed (syntax: @file). +- Improved wording of warning and error messages. + +Code generation: + +- Support for ARM target processors in big-endian mode. +- Optimize 64-bit integer division by constants. + +Bug fixing: + +- Issue #155: on ARM, assembly errors caused by large jump tables for + "switch" statements and overflow in accessing constant pools. +- Issue #151: large inductive definition causes a fatal error in + 32-bit versions of Coq. +- Issue #143: handle "%lf" printf() format in the reference interpreter +- Issue #138: struct declarations in K&R function parameters were ignored. +- Issues #110, #111, #113, #114, #115, #119, #120, #121, #122, #123, #124, + #125, #126, #127, #128, #129, #130, #133, #138, #144: various cases + of internal errors and failed assertions that should have been + proper errors instead. +- For __builtin_memcpy_aligned, size and alignment arguments of 64-bit + integer type were causing a fatal error on a 32-bit target. +- ARM and x86 ports: wrong register allocation for some calls to + function pointers. Release 2.7.1, 2016-07-18 @@ -255,6 +255,7 @@ endif clean: rm -f $(patsubst %, %/*.vo, $(DIRS)) + rm -f $(patsubst %, %/.*.aux, $(DIRS)) rm -rf doc/html doc/*.glob rm -f doc/coq2html.ml doc/coq2html doc/*.cm? doc/*.o rm -f driver/Version.ml diff --git a/Makefile.extr b/Makefile.extr index 8fdc9ffe..fb19dd00 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -17,10 +17,23 @@ include Makefile.config +# +# Variables from Makefile.config: +# -OCAML_OPT_COMP: can we use the native version +# -COMPFLAGS: compile options +# -LINK_OPT: additional linker flags for the native binary +# + # Menhir configuration. include Makefile.menhir +# +# Variables from Makefile.menhir: +# -MENHIR_INCLUDES: additional menhir include paths +# -MENHIR_LIBS: additional menhir libraries +# + # The pre-parser's error message database is compiled as follows. cparser/pre_parser_messages.ml: @@ -80,7 +93,7 @@ CCOMP_OBJS:=$(shell $(MODORDER) driver/Driver.cmx) ccomp: $(CCOMP_OBJS) @echo "Linking $@" - @$(OCAMLOPT) -o $@ $(LIBS) $+ + @$(OCAMLOPT) -o $@ $(LIBS) $(LINK_OPT) $+ ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo) @echo "Linking $@" @@ -90,7 +103,7 @@ CLIGHTGEN_OBJS:=$(shell $(MODORDER) exportclight/Clightgen.cmx) clightgen: $(CLIGHTGEN_OBJS) @echo "Linking $@" - @$(OCAMLOPT) -o $@ $(LIBS) $+ + @$(OCAMLOPT) -o $@ $(LIBS) $(LINK_OPT) $+ clightgen.byte: $(CLIGHTGEN_OBJS:.cmx=.cmo) @echo "Linking $@" diff --git a/cparser/Cerrors.ml b/cparser/Cerrors.ml index c7b791e0..dffd9c14 100644 --- a/cparser/Cerrors.ml +++ b/cparser/Cerrors.ml @@ -18,8 +18,15 @@ open Format open Commandline +(* Should errors be treated as fatal *) let error_fatal = ref false +(* Maximum number of errors, 0 means unlimited *) +let max_error = ref 0 + +(* Whether [-Woption] should be printed *) +let diagnostics_show_option = ref true + (* Test if color diagnostics are available by testing if stderr is a tty and if the environment varibale TERM is set *) @@ -33,6 +40,11 @@ let color_diagnostics = let num_errors = ref 0 let num_warnings = ref 0 + +let error_limit_reached () = + let max_err = !max_error in + max_err <> 0 && !num_errors >= max_err - 1 + let reset () = num_errors := 0; num_warnings := 0 exception Abort @@ -169,6 +181,9 @@ let wall () = Inline_asm_sdump; ] +let wnothing () = + active_warnings :=[] + (* Make all warnings an error *) let werror () = error_warnings:=[ @@ -198,12 +213,19 @@ let werror () = let key_of_warning w = match w with | Unnamed -> None - | _ -> Some ("-W"^(string_of_warning w)) + | _ -> if !diagnostics_show_option then + Some ("-W"^(string_of_warning w)) + else + None (* Add -Werror to the printed keys *) -let key_add_werror = function - | None -> Some ("-Werror") - | Some s -> Some ("-Werror,"^s) +let key_add_werror w = + if !diagnostics_show_option then + match w with + | None -> Some ("-Werror") + | Some s -> Some ("-Werror,"^s) + else + None (* Lookup how to print the warning *) let classify_warning w = @@ -250,10 +272,31 @@ let pp_key key fmt = | Some s -> " ["^s^"]" in fprintf fmt "%s%t@." key rsc +(* Different loc output formats *) +type loc_format = + | Default + | MSVC + | Vi + +let diagnostics_format : loc_format ref = ref Default + +(* Parse the option string *) +let parse_loc_format s = + let s = String.sub s 21 ((String.length s) - 21) in + let loc_fmt = match s with + | "ccomp" -> Default + | "msvc" -> MSVC + | "vi" -> Vi + | s -> Printf.eprintf "Invalid value '%s' in '-fdiagnostics-format=%s'\n" s s; exit 2 in + diagnostics_format := loc_fmt + (* Print the location or ccomp for the case of unknown loc *) let pp_loc fmt (filename,lineno) = if filename <> "" && lineno <> -10 && filename <> "cabs loc unknown" then - fprintf fmt "%t%s:%d:%t " bc filename lineno rsc + match !diagnostics_format with + | Default -> fprintf fmt "%t%s:%d:%t " bc filename lineno rsc + | MSVC -> fprintf fmt "%t%s(%d):%t " bc filename lineno rsc + | Vi -> fprintf fmt "%t%s +%d:%t " bc filename lineno rsc else fprintf fmt "%tccomp:%t " bc rsc @@ -282,7 +325,7 @@ let warning loc ty fmt = | SuppressedMsg -> ifprintf err_formatter fmt let error loc fmt = - if !error_fatal then + if !error_fatal || error_limit_reached ()then fatal_error None loc fmt else error None loc fmt @@ -301,7 +344,7 @@ let error_option w = let key = string_of_warning w in [Exact ("-W"^key), Unit (activate_warning w); Exact ("-Wno-"^key), Unit (deactivate_warning w); - Exact ("-Werror="^key), Unit ( warning_as_error w); + Exact ("-Werror="^key), Unit (warning_as_error w); Exact ("-Wno-error="^key), Unit ( warning_not_as_error w)] let warning_options = @@ -329,7 +372,13 @@ let warning_options = Exact ("-fdiagnostics-color"), Ignore; (* Either output supports it or no color *) Exact ("-fno-diagnostics-color"), Unset color_diagnostics; Exact ("-Werror"), Unit werror; - Exact ("-Wall"), Unit wall;] + Exact ("-Wall"), Unit wall; + Exact ("-w"), Unit wnothing; + longopt_int ("-fmax-errors") ((:=) max_error); + Exact("-fno-diagnostics-show-option"),Unset diagnostics_show_option; + Exact("-fdiagnostics-show-option"),Set diagnostics_show_option; + _Regexp("-fdiagnostics-format=\\(ccomp\\|msvc\\|vi\\)"),Self parse_loc_format; + ] let warning_help = {|Diagnostic options: -Wall Enable all warnings @@ -342,6 +391,10 @@ let warning_help = {|Diagnostic options: -Wfatal-errors Turn all errors into fatal errors aborting the compilation -fdiagnostics-color Turn on colored diagnostics -fno-diagnostics-color Turn of colored diagnostics + -fmax-errors=<n> Maximum number of errors to report + -fdiagnostics-show-option Print the option name with mappable diagnostics + -fno-diagnostics-show-option Turn of printing of options with mappable + diagnostics |} let raise_on_errors () = diff --git a/cparser/Elab.mli b/cparser/Elab.mli index 7eee4a08..f701e8c5 100644 --- a/cparser/Elab.mli +++ b/cparser/Elab.mli @@ -14,3 +14,12 @@ (* *********************************************************************) val elab_file : Cabs.definition list -> C.program + (* This is the main entry point. It transforms a list of toplevel + definitions as produced by the parser into a program in C abstract + syntax. *) + +val elab_int_constant : Cabs.cabsloc -> string -> int64 * C.ikind +val elab_float_constant : Cabs.floatInfo -> C.float_cst * C.fkind +val elab_char_constant : Cabs.cabsloc -> bool -> int64 list -> int64 + (* These auxiliary functions are exported so that they can be reused + in other projects that deal with C-style source languages. *) diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml index dfde9136..6f159743 100644 --- a/debug/DebugInformation.ml +++ b/debug/DebugInformation.ml @@ -395,6 +395,7 @@ let insert_global_declaration env dec = let fields = List.map (fun f -> { cfd_name = f.fld_name; + cfd_anon = f.fld_anonymous; cfd_typ = insert_type f.fld_typ; cfd_bit_size = f.fld_bitfield; cfd_bit_offset = None; diff --git a/debug/DebugTypes.mli b/debug/DebugTypes.mli index 25c7390f..c3df6066 100644 --- a/debug/DebugTypes.mli +++ b/debug/DebugTypes.mli @@ -19,6 +19,7 @@ open Camlcoq type composite_field = { cfd_name: string; + cfd_anon: bool; cfd_typ: int; cfd_bit_size: int option; cfd_bit_offset: int option; diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml index b81507a8..13e7765d 100644 --- a/debug/DwarfPrinter.ml +++ b/debug/DwarfPrinter.ml @@ -159,7 +159,7 @@ module DwarfPrinter(Target: DWARF_TARGET): add_attr_some e.member_bit_offset (add_abbr_entry (0xc,"DW_AT_bit_offset",DW_FORM_data1)); add_attr_some e.member_bit_size (add_abbr_entry (0xd,"DW_AT_bit_size",DW_FORM_data1)); add_attr_some e.member_declaration add_declaration; - add_name buf e.member_name; + add_name_opt buf e.member_name; add_type buf; (match e.member_data_member_location with | None -> () @@ -472,7 +472,7 @@ module DwarfPrinter(Target: DWARF_TARGET): print_opt_value oc "DW_AT_bit_offset" mb.member_bit_offset print_byte; print_opt_value oc "DW_AT_bit_size" mb.member_bit_size print_byte; print_opt_value oc "DW_AT_declaration" mb.member_declaration print_flag; - print_string oc "DW_AT_name" mb.member_name; + print_opt_value oc "DW_AT_name" mb.member_name print_string; print_ref oc "DW_AT_type" mb.member_type; print_opt_value oc "DW_AT_data_member_location" mb.member_data_member_location print_data_location diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli index 48da4509..23aba448 100644 --- a/debug/DwarfTypes.mli +++ b/debug/DwarfTypes.mli @@ -159,7 +159,7 @@ type dw_tag_member = member_bit_size: constant option; member_data_member_location: data_location_value option; member_declaration: flag option; - member_name: string_const; + member_name: string_const option; member_type: reference; } diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml index 30e44e52..ee568042 100644 --- a/debug/Dwarfgen.ml +++ b/debug/Dwarfgen.ml @@ -232,7 +232,7 @@ module Dwarfgenaux (Target: TARGET) = | None -> None | Some s -> Some (DataLocBlock (DW_OP_plus_uconst s))); member_declaration = None; - member_name = string_entry mem.cfd_name; + member_name = if mem.cfd_anon then None else Some (string_entry mem.cfd_name); member_type = mem.cfd_typ; } in new_entry (next_id ()) (DW_TAG_member mem) diff --git a/doc/ccomp.1 b/doc/ccomp.1 index c02d3571..d84adc7f 100644 --- a/doc/ccomp.1 +++ b/doc/ccomp.1 @@ -16,8 +16,7 @@ In other words, the executable code it produces is proved to behave exactly as s 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 +.SH RECOGNIZED SOURCE FILES . .TP .B .c @@ -48,6 +47,18 @@ Object file. Library file. . .SH OPTIONS +.SS General Options +.INDENT 0.0 +. +.TP +.B \-conf <file> +Read CompCert configuration from <file>. This takes precedence over any other specification. +. +.TP +.B \-target <triple> +Read CompCert configuration from <triple>.ini instead of using the default of compcert.ini. +The configuration file is searched for in the share directory of the CompCert installation. +. .SS Processing Options .INDENT 0.0 . @@ -537,5 +548,14 @@ Randomize execution order. .TP .B \-all Simulate all possible execution orders. +. +.SH ENVIRONMENT +. +.TP +.B COMPCERT_CONFIG +If this environment variable is present, it denotes the path to the CompCert configuration file to be used. +The variable takes precedence over default search paths or the \fB\-target\fP option, but has a lower priority than the \fB\-conf\fP option. +. .SH BUGS +. To report bugs, please visit <https://github.com/AbsInt/CompCert/issues>. diff --git a/driver/Commandline.ml b/driver/Commandline.ml index c0dd6257..b544c37b 100644 --- a/driver/Commandline.ml +++ b/driver/Commandline.ml @@ -115,3 +115,20 @@ let parse_cmdline spec = with Responsefile.Error s -> eprintf "%s" s; exit 2 + +let long_int_action key s = + let ls = String.length s + and lkey = String.length key in + assert (ls > lkey); + let s = String.sub s (lkey + 1) (ls - lkey - 1) in + try + int_of_string s + with Failure _ -> + eprintf "Argument to option `%s' must be an integer\n" key; + exit 2 + +let longopt_int key f = + let act s = + let n = long_int_action key s in + f n in + Prefix (key ^ "="),Self act diff --git a/driver/Commandline.mli b/driver/Commandline.mli index 197d0b04..65253749 100644 --- a/driver/Commandline.mli +++ b/driver/Commandline.mli @@ -40,3 +40,8 @@ val parse_cmdline: (pattern * action) list -> unit (* Note on precedence: [Exact] patterns are tried first, then the other patterns are tried in the order in which they appear in the list. *) + +val longopt_int: string -> (int -> unit) -> pattern * action +(** [longopt_int key fn] generates a pattern and an action for + options of the form [key=<n>] and calls [fn] with the integer argument +*) diff --git a/driver/Driver.ml b/driver/Driver.ml index d154c95b..3219b7b7 100755 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -271,7 +271,7 @@ Recognized source files: .i or .p C source file that should not be preprocessed .cm Cminor source file .s Assembly file - .S Assembly file that must be preprocessed + .S or .sx Assembly file that must be preprocessed .o Object file .a Library file Processing options: @@ -312,7 +312,8 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>) -fsmall-const <n> Set maximal size <n> for allocation in small constant area -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|} ^ + -falign-cond-branches <n> Set alignment (in bytes) of conditional branches +|} ^ target_help ^ assembler_help ^ linker_help ^ @@ -503,6 +504,8 @@ let cmdline_actions = push_action process_s_file s; incr num_source_files; incr num_input_files); Suffix ".S", Self (fun s -> push_action process_S_file s; incr num_source_files; incr num_input_files); + Suffix ".sx", Self (fun s -> + push_action process_S_file s; incr num_source_files; incr num_input_files); Suffix ".o", Self (fun s -> push_linker_arg s; incr num_input_files); Suffix ".a", Self (fun s -> push_linker_arg s; incr num_input_files); (* GCC compatibility: .o.ext files and .so files are also object files *) |